--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] PDG semantic



Hello,

This answer <
http://stackoverflow.com/questions/12328228/the-meaning-of-kinds-of-curve-in-pdg>
by Anne Pacalet should help you understand the PDGs Frama-C produce.
Regarding the definition of each kind of edge, you can consult for example
<
http://www.cc.gatech.edu/~harrold/6340/cs6340_fall2009/Readings/ferrante87jul.pdf>.
Within Frama-C's PDGs, brown rectangles are call summaries, that
abstract over what happens during the call to the function.

Regarding control-flow graphs, those are much easier to build than PDGs --
and in fact only distantly related. See for example this post by Virgile
Prevosto <
http://blog.frama-c.com/index.php?post/2012/09/04/Extracting-information-from-Frama-C-programmatically>,
that you should be able to adapt to your needs. (In particular,
labeling
transitions from conditionals, and fusing successive statements together.)
We never integrated an export from Cil control-flows graphs to dot, because
even for middle-sized functions, the result is quite hard to read. However,
as mentioned in the blog, all the information is available programmatically.

Hope this helps,


On Fri, Nov 30, 2012 at 9:30 PM, Rovedy Aparecida Busquim e Silva <
rovedy at ig.com.br> wrote:

> Hi,
>
> I have investigated the PDG plugin with the example below. I Know little
> about PDGs.
>
> I would like to Know the semantic of the PDG nodes and edges (e.g. what
> does it mean blue edges, dark edges, and dotted edges?
> And about the color of the nodes? What are circle nodes, rectangle nodes,
> ... ). Is there some reference for reading?
>
> Is it possible use the PDG to help the value analysis? Maybe with the
> slevel?
>
> I attached the graphs.
>
> I would like to know if is possible to create a Control Flow Graph as
> showed in the attached figure.  Exist another plugin for this or another
> way to obtain the same information?
>
> Best regards,
> Rovedy
>
>
> //-------------------------------------------------------------------------------------------------
>
>
> void main()
> {
> int a=0,b=0,c=0;
>
>  a=4;
>
> if ( a > 5 )
> {
>    b = 3;
>    c = a + 5;
>    return ;
> }
> else
> {
>    b = 4;
>    a = foo(a);
>    c = a+5;
> }
> }
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121201/9e437bee/attachment.html>