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



Jonathan-Christofer Demay a ?crit :
> Let's say I need to get a node from its id for a particular pdg, for
> now, in order to get this, I use Db.Pdg.iter_nodes looking for the
> correct id (I'm not sure it's worth creating a hashtable for this), but
> I was wondering if there were an easier way to do it (I did search but
> found nothing) or if maybe frama-c's dev would consider adding such
> feature.

I can add something like that easily, because it already exists 
internally, but using the nodes key given by [Db.Pdg.node_key] (not the 
id). But I am not sure to understand why you need that :
where do you get the node id from ?

> Also, if I'm talking about this on the ML, it's because I've also
> considered the fact that maybe if I need such feature, it's because I
> went wrong somewhere.

Let's see ;-)

> So just in case, I will tell why I need this. Let's consider this simple
> piece of C code:
> 
> 1.	b += z;
> 	
> 2.	c = toto(b,a);
> 
> 3.	c++;
> 
> 4.	e = toto(c,a);
> 
> For the statement 4, I ask for the corresponding nodes (using
> Db.Pdg.find_simple_stmt_nodes), then I ask for all its dependencies
> (using Db.Pdg.all_dpds). I get statements 2 and 3.

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.

> But since statement 2 is a call, from which the result might depend (in
> worst case scenario) on all it's dependencies, I want to add those to
> the dependencies of the statement 4.

The dependencies in the call are given by the value analysis,
so normally, it is a sur-approximation at all that can possibly happen.

Do you know that for simple cases like that, you should consider to use
[Db.Pdg.extract] to generate a .dot file so you can have a look at the 
graph. I think it helps a lot at the beginning...

Hope this help, and tell me it you still want :
   Db.Pdg.find_node : node_key -> node.

-- 
Anne Pacalet  -
INRIA - 2004, route des Lucioles BP.93 F-06902 Sophia Antipolis Cedex.
Tel : +33 (0) 4 9715 5345