Pdg plugin

API Documentation

The Pdg plugin is integrated with the Frama-C kernel:

Internal Documentation

Overview

The main modules are :

What is a PDG ?

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 :

A dependency between two nodes can have any combination of these kinds.

You can find more documentation, particularly on how this graph is built, in this report (in French).

Dynamic dependencies

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.

How to see a PDG ?

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 :

So a solid blue edge with a circle arrow represent a data+control dependency for instance, while a dotted black edge with a triangle arrow represent a address dependency.

You are invited to look at a simple example to see the different kinds of dependencies.