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

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