--- layout: fc_discuss_archives title: Message 67 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 Fri, 2009-03-20 at 10:23 +0100, Anne Pacalet wrote:
> But if you _did_ have to try to do these computations,  it is probably 
> because something went wrong...
> So, let's try to find out want.
> On the file :
> --------------------------
> int toto (int x, int y);
> 
> void main (int a, int b, int c, int z, int e) {
>    int e = 3;
>    b += z;
>    c = toto(b,a);
>    c++;
>    e = toto(c,a);
> }
> --------------------------
> and you can see that you get (among others) : [Elem] 11 : b += z;
> which is the node that you want, don't you ?

Indeed, that was the one I was missing (in this small example), so it
works, I now have all the nodes I want (thanks !).

Now I think I figured out why I didn't get all of them before, it was
caused by the way toto's declaration was written. If I replace in the C
file 'int toto (int x, int y);' by 'int toto (int,int);' (which is still
a valid C syntax I think, right ?), then '[Elem] 11 : b += z' (among
other nodes) will no longer appear.

Do you happen to get a similar result ? If you don't, well I have to
figure out what's wrong in my frama-c's setup. If you do, well is it the
intended behavior ?

Anyway, thanks a lot for your time !