[Frama-c-discuss] integer overflow

John Regehr regehr at cs.utah.edu
Thu Jun 11 23:01:49 CEST 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




More information about the Frama-c-discuss mailing list