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
- Subject: [Frama-c-discuss] Scope plugin from command line
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Mon, 6 Jun 2011 16:56:56 +0200
- In-reply-to: <BANLkTimUrEvk1M0br69uyWbfgExwaxFtOw@mail.gmail.com>
- References: <4DEA5811.email@example.com> <BANLkTinWLofxvGt+sDy+HJLJV4QdHqYaig@mail.gmail.com> <4DEAE8DE.firstname.lastname@example.org> <BANLkTimUrEvk1M0br69uyWbfgExwaxFtOw@mail.gmail.com>
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
- Prev by Date: [Frama-c-discuss] Scope plugin from command line
- Next by Date: [Frama-c-discuss] Scope plugin from command line
- Previous by thread: [Frama-c-discuss] Scope plugin from command line
- Next by thread: [Frama-c-discuss] Plugin development >> Going through loops twice.