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 |