HCoop / bpt / coccinelle.git / blame
| Commit | Line | Data |
|---|---|---|
| 755320b0 C |
1 | /* |
| 2 | Given a file with data about the integer values that variables | |
| 3 | x can take at certain positions, this patch identifies some | |
| 4 | then-branches of if(x) ... statements. | |
| 5 | ||
| 6 | Run this example from the coccinelle main directory using: | |
| 7 | ||
| 8 | ./scripts/spatch --sp-file demos/external_ana.cocci demos/external_ana.c \ | |
| 9 | --external-analysis-file demos/external_ana.data | |
| 10 | ||
| 11 | The analysis input was produced with a custom-made plugin for | |
| 12 | frama-c that produced the external_ana.data file using the | |
| 13 | commandline: | |
| 14 | ||
| 15 | frama-c -load-module ValueExport.cmxs -value-export \ | |
| 16 | -export-file ./external_ana.data external_ana.c | |
| 17 | ||
| 18 | */ | |
| 19 | ||
| 20 | @r@ | |
| 21 | idexpression x; | |
| 22 | position p, q; | |
| 23 | statement S; | |
| 24 | @@ | |
| 25 | ||
| 26 | if@q (x@p) S | |
| 27 | ||
| 28 | ||
| 29 | @script:ocaml@ | |
| 30 | x << r.x; | |
| 31 | p << r.p; | |
| 32 | @@ | |
| 33 | ||
| 34 | let p1 = Coccilib.basename_pos (List.hd p) in | |
| 35 | Printf.printf "considering %s at position %s:(%d,%d)-(%d,%d):\n" | |
| 36 | x p1.Coccilib.file p1.Coccilib.line p1.Coccilib.col | |
| 37 | p1.Coccilib.line_end p1.Coccilib.col_end; | |
| 38 | ||
| 39 | let rs = Coccilib.Ana.find p1 in | |
| 40 | Printf.printf " results: %d\n" (List.length rs); | |
| 41 | List.iter (fun r -> Printf.printf " value: %s\n" (Coccilib.Ana.show_result r)) rs; | |
| 42 | ||
| 43 | let is_z = Coccilib.Ana.has_only_nul p1 in | |
| 44 | Printf.printf " Always zero: %B\n" is_z; | |
| 45 | ||
| 46 | Coccilib.include_match is_z | |
| 47 | ||
| 48 | ||
| 49 | @@ | |
| 50 | position r.q; | |
| 51 | statement S; | |
| 52 | @@ | |
| 53 | ||
| 54 | - if@q (...) S |