--- layout: fc_discuss_archives title: Message 67 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



> 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.