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