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

[Frama-c-discuss] PDG semantic



Hi Boris,

Thanks for the information.

The script has worked well.

I will read the paper.

Best regards,
Rovedy


2012/12/1 Boris Yakobowski <boris at yakobowski.org>

> 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
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121204/c018c146/attachment.html>