--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] There may be a problem with the Program Dependence Graph



I may have found a bug in the pdg plugin but maybe I'm using it the
wrong way so that's why I'm posting here instead of the bts.

Attached in this email a simple plugin that prints the nodes each
function call depends on, according to the pdg, and a small C file to
illustrate what I think is wrong.

If I run 'frama-c -cdn test.c', it tells me that the function calls at
lines 11 and 13 depend on 'VarDecl : tmp' which I think is wrong since
'tmp' is declared *after* those function calls. The same plugin does not
include this node when used with Boron.

Strange thing, if I modify certain nodes on which those function calls
do *not* depend, like 'f(s.c)' at line 19 replaced by 'f(p)', then
'VarDecl : tmp' disappear from the dep nodes.

Regards.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: cdn.tar.bz2
Type: application/x-bzip-compressed-tar
Size: 1056 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110222/2cf9d4bd/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: text/x-csrc
Size: 316 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110222/2cf9d4bd/attachment.c>