--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on March 2009 ---
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.