The Pdg plugin is integrated with the Frama-C kernel:
The main modules are :
PdgIndex
that can be used to store different kind of information related to a function (not only related to PDG)PdgTypes
.Build
. It also use the lexical successor graph, which is computed in Lexical_successors
. Sets
provides functions to read a PDG.Print
provides functions to print a PDG either in textual form or in
a dot file (See "How to see a PDG" below).A Program Dependences Graph represent the dependences between the statements of a function. So the nodes of the graph mainly represent the statements (some more nodes are used to represents things like declarations, inputs, outputs, etc.) and the edges represent the dependences.
Y -> X
means that the computation of the statement Y depend on (the result of)
the statement X. Example :
X : x = a + b; Y : y = x + 1;
There are three kinds of dependencies :
if (c) X : x = a + b;
t[i] = 3;
tab
and the computation of i
.You can find more documentation, particularly on how this graph is built, in this report (in French).
After having built the PDG for a function, there is a way of adding dynamically some dependencies to it. There are not stored directly in the PDG so they can be cleared later on.
As PDG doesn't interpret the annotations of the code, this feature can for instance be used to add dependencies on assertions.
To see an example of how to use it, please have a look at
tests/pdg/dyn_dpds.ml
.
Please, use the -help
option of the tool to get the PDG options names.
The PDG of a function can be seen either in textual form or exported in a dot file which is the format of the Graphviz tool set. They can be viewed using zgrviewer or exported in SVG format to be seen with some browser or Inkscape.
The graph is unfortunately generated with the output of the function at the top
and its inputs at the bottom. If you find it uncomfortable to read,
just change TB
by BT
in the rankdir
property at the beginning of the
dot file before viewing it.
The color and the shape of the nodes are used to make it easier to read the graph, but add no more meaning.
For the edges :
You are invited to look at
a simple example
to see the different kinds of dependencies.