--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Getting a node from its id for a particular pdg



On Wed, 2009-03-18 at 16:44 +0100, Anne Pacalet wrote:
> Can you provide more information about the 'toto' function  ?
> Because I suspect that if [Db.Pdg.all_dpds] doesn't return the node 1,
> it is because [c] doesn't depend on [b] in the call.
> 
> The dependencies in the call are given by the value analysis,
> so normally, it is a sur-approximation at all that can possibly happen.
> 
Oops, I forgot to tell that in this particular example, 'toto' is a
function from a library and its definition is not provided to frama-c
for the analysis, just its declaration.

That's why I want to assume a 'worst case scenario' and add all the
statements that statement 2 depends on to the dependencies of statement
4. (because Db.Pdg.all_dpds stops at the OutRet and InCtrl nodes of
statement 2)

Of course, when the definition of the function called is provided, I let
the pdg plugin do its job.

If what I'm doing isn't wrong, then I might have another question:

>From a Call(x)-OutRet node, is there a way to get all the corresponding
Call(x)-In(y) nodes ?

I mean for now, I'm adding all the nodes which ids are between
InCtrl.elem_id and OutRet.elem_id, but I'm not sure if playing with ids
like this is quite the reliable method.

Thanks.