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

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: roco_process.png
Type: image/png
Size: 166664 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110604/4b5cf0e0/attachment-0001.png>