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: anne.pacalet at inria.fr (Anne Pacalet)
  • Date: Tue, 22 Feb 2011 16:32:53 +0100 (CET)
  • In-reply-to: <1298391125.18524.89.camel@residence>
> 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.

Well, 'tmp' is syntactically declared after those function calls, 
but because they are in a loop, it can also be considered *before* 
the next iteration of loop... So those dependencies are not 'impossible'.

I suspect that your problem comes from 
- either an underspecified behavior for the called function f :
  if f doesn't modify its arg, you should specify :
  //@ assigns \nothing;

- or, if it not the case, you can see using :
    frama-c -deps test.c
  that f is supposed to have the following dependencies :
    [from] Function f:
         s.c[0] FROM s.c[0]
         \result FROM s.c[0]
This is because of the last call where arg = s.c.
If you want each call of f to have its own dependencies,
you should consider using the -calldeps option.

Just in case you didn't see it, you can also use :
  frama-c -pdg test.c
to dump the raw results from the PDG computation.
It can help to analyze where the dependencies come from.

Hope this help, and please ask for more if my hints 
don't solve your problem.

Anne.