--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on June 2009 ---
Pascal, Thanks for the long email. I think that in general Frama-C is taking a very sensible approach to C verification and it is a great tool. >> Optimizing C compilers including gcc routinely exploit the undefined nature >> of signed overflow! > > Rats! Do you have a reproducible example where the assembly does > not contain the addition at all? Here is an example that does not quite meet your requirement, but is similar: int foo(int y) { return (((unsigned short)y*(unsigned short)-2)>=(y?0:y)); } int main (void) { printf ("%d\n", foo(-2)); return 0; } Running Frama-C's value analysis gives this: Values for function foo: tmp ? {0; } __retres ? {0; } If I understand correctly, this means that the function must return 0. On the other hand, let's see what gcc tells us: [regehr at babel ~]$ current-gcc -Os -S foo2.c -o - -fomit-frame-pointer foo: movl $1, %eax ret It is a different answer! gcc has exploited the overflow of the signed arithmetic 65534*65534. Here I am using some random development snapshot of gcc but I think that the 4.4.0 release generates exactly the same output. > I will try to make this possible soon, either in the form > of a patch published on this list > (hopefully you were compiling Frama-C from sources) > or as an experimental feature in the next release, > whose date it is forbidden to discuss on this list. I would be a happy user of this feature! Thanks, John Regehr