--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Scope plugin from command line



I sent this solution to Vijayaraghavan Murali but actually,
someone else in the list may someday be interested by it.
Besides, I wanted to add that the Scope plug-in and
the underlying Program Dependency Graph were instrumental
in solving the ICPC industrial challenge, the write-up of which
starts here:

http://blog.frama-c.com/index.php?post/2011/06/06/Fixing-robots%2C-part-1

______________

> The output from -pdg is almost exactly what I wanted, except since there is
> no line number information printed, there is no way to find out which line
> the [Elem]s correspond to. One can look at the actual code that is printed
> next to [Elem], but the exact same code (syntax-wise) could appear at
> different places in the program.
>
> Is there a way to print line number information or is there any mapping from
> the [Elem]s to program points? This would solve all my problems.

With the very little tested patch below, some nodes that can be
annotated with a program point are.
You may need a little work to adapt this to Carbon (it is a patch
against the development version).

The output is then displayed as:

[pdg] RESULT for main:
? ? ?[Elem] 0 : InCtrl
? ? ?[Elem] 1 : VarDecl : vol
? ? ?[Elem] 2 (tests/misc/alias.i:40) : vol = (int volatile)0;
? ? ? ?-[-c-]-> 0
? ? ? ?-[a--]-> 1
? ? ?[Elem] 3 (tests/misc/alias.i:43) : A = 1;
? ? ? ?-[-c-]-> 0
? ? ?[Elem] 4 (tests/misc/alias.i:44) : B = 2;
? ? ? ?-[-c-]-> 0
? ? ?[Elem] 5 (tests/misc/alias.i:45) : Call18-InCtrl : f((char *)(& A),& B);
? ? ? ?-[-c-]-> 0
? ? ?[Elem] 6 (tests/misc/alias.i:45) : Call18-In1 : f((char *)(& A),& B);
? ? ? ?-[-c-]-> 0
? ? ? ?-[-c-]-> 5

Pascal

--- src/pdg_types/pdgTypes.ml ? (revision 13791)
+++ src/pdg_types/pdgTypes.ml ? (working copy)
@@ -667,7 +667,13 @@

? let pretty_node fmt n =
? ? let id = Node.elem_id n in
- ? ?Format.fprintf fmt "[Elem] %d : " id;
+ ? ?( match Node.stmt n with
+ ? ? ?None ->
+ ? ? ? Format.fprintf fmt "[Elem] %d : " id;
+ ? ?| Some stmt ->
+ ? ? ? Format.fprintf fmt "[Elem] %d (%a) : "
+ ? ? ? ? id
+ ? ? ? ? Cil.d_loc (Cil_datatype.Stmt.loc stmt));
? ? let key = Node.elem_key n in
? ? PdgIndex.Key.pretty fmt key