--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Scope plugin from command line



Thank you! That was informative. I will look into the options.

-----
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