Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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