| 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 |