--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2011 ---
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