--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2011 ---
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. ----- Vijayaraghavan Murali http://www.comp.nus.edu.sg/~mvijayar On 05/06/2011 01:04, Pascal Cuoq wrote: > Hello, > > from the command-line, you can use the -pdg -dot-pdg filename options. > It is not exactly what you want, but what interface would you have > wanted for a command-line version of the "Show defs" GUI feature > anyway? > > The emitted files are in the popular DOT format, but if you find that > it is not convenient enough to use for what you want to do, your next > question may be "Is there a way to invoke the scope plug-in > programmatically?". The answer to this question is much richer, but I > am not familiar enough with the programmatic interface to say much > about this. > > If you do not like the DOT file, you may also try to take advantage of > the textual output of the -pdg option itself. > > On some files that I had around and that came from > http://icpc2011.cs.usask.ca/conf_site/IndustrialTrack.html , > the DOT file looks like this: > > digraph G { > rankdir=TB; > node [style=filled]; > 123 [shape=box, fillcolor="#CCCCCC", label=";"]; > 124 [shape=box, fillcolor="#FFCA6E", label="InCtrl"]; > 125 [shape=box, fillcolor="#FFCA6E", label="In1"]; > 126 [shape=box, fillcolor="#FFCA6E", label="In2"]; > 127 [shape=box, fillcolor="#FFCA6E", label="In3"]; > 128 [shape=box, fillcolor="#FFCA6E", label="In4"]; > 129 [shape=box, fillcolor="#FFCA6E", label="OutRet"]; > 130 [shape=box, fillcolor="#FFCA6E", label="Out(standstillDelay)"]; > 131 [shape=diamond, fillcolor="#CCCCCC", label="tmp_6"]; > 132 [shape=doublecircle, fillcolor="#CCCCCC", label="{}"]; > 133 [shape=diamond, fillcolor="#CCCCCC", label="! initBackwards"]; > 134 [shape=box, fillcolor="#CCCCCC", label="initBackwards = (char)1;"]; > 135 [shape=box, fillcolor="#CCCCCC", label="RoCo_error = (char)1;"]; > 136 [shape=box, fillcolor="#FFCA6E", label="InCtrl"]; > 137 [shape=box, fillcolor="#FFCA6E", label="In1"]; > 138 [shape=box, fillcolor="#FFCA6E", label="Out(initTimer)"]; > 139 [shape=box, fillcolor="#CCCCCC", label="RoCo_isActive = (char)0;"]; > 140 [shape=box, fillcolor="#FFCA6E", label="InCtrl"]; > 141 [shape=box, fillcolor="#FFCA6E", label="In1"]; > 142 [shape=box, fillcolor="#FFCA6E", label="In2"]; > 143 [shape=box, fillcolor="#FFCA6E", label="In3"]; > 144 [shape=box, fillcolor="#FFCA6E", label="In4"]; > 145 [shape=box, fillcolor="#FFCA6E", label="Out(standstillDelay)"]; > 146 [shape=box, fillcolor="#CCCCCC", label="init = (char)0;"]; > 147 [shape=diamond, fillcolor="#CCCCCC", > label="(int)initBackwards ^ (int)t14"]; > 148 [shape=box, fillcolor="#CCCCCC", > label="rampTarget = RoCo_initMoveSpeed_PARAM;"]; > 149 [shape=box, fillcolor="#CCCCCC", > label="rampTarget = - RoCo_initMoveSpeed_PARAM;"]; > ? > > and the output of option -pdg in the log looks like: > > [pdg] RESULT for RoCo_process: > [Elem] 123 : ; > -[-c-]-> 114 > -[-c-]-> 117 > [Elem] 124 : Call234-InCtrl : tmp_6 = Turn_on_delay(& > standstillDelay,(char)(tmp_5< 0.001), > RoCo_initStandstillTimeout_PARAM,dT); > -[-c-]-> 114 > -[-c-]-> 117 > [Elem] 125 : Call234-In1 : tmp_6 = Turn_on_delay(& > standstillDelay,(char)(tmp_5< 0.001), > RoCo_initStandstillTimeout_PARAM,dT); > -[-c-]-> 114 > -[-c-]-> 117 > -[-c-]-> 124 > [Elem] 126 : Call234-In2 : tmp_6 = Turn_on_delay(& > standstillDelay,(char)(tmp_5< 0.001), > RoCo_initStandstillTimeout_PARAM,dT); > -[--d]-> 19 > -[-c-]-> 114 > -[-c-]-> 117 > -[--d]-> 122 > -[-c-]-> 124 > [Elem] 127 : Call234-In3 : tmp_6 = Turn_on_delay(& > standstillDelay,(char)(tmp_5< 0.001), > RoCo_initStandstillTimeout_PARAM,dT); > -[-c-]-> 114 > -[-c-]-> 117 > -[-c-]-> 124 > -[--d]-> 401 > [Elem] 128 : Call234-In4 : tmp_6 = Turn_on_delay(& > standstillDelay,(char)(tmp_5< 0.001), > RoCo_initStandstillTimeout_PARAM,dT); > -[-c-]-> 114 > -[-c-]-> 117 > -[-c-]-> 124 > -[--d]-> 359 > ? > Tools that manipulate the DOT format can transform the DOT file into a > graph such as the attached picture. > > Pascal > > > Pascal