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



>
> 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 ?

You are right,
int toto(int, int);
int titi(int a, int b);

produce different default specifications.
As shown with option -print:

/*@ behavior generated:
       assigns \at(\result,Post) \from \nothing;
       */
extern int toto(int  , int  ) ;

/*@ behavior generated:
       assigns \at(\result,Post) \from a, b;
       */
extern int titi(int a , int b ) ;

This is a bug. Thanks for pointing it out.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090320/f9ac1a2e/attachment.htm