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

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