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