Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] There may be a problem with the Program Dependence Graph
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Tue, 22 Feb 2011 16:12:05 +0000
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>