demos/external_ana.cocci

   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