Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] integer overflow

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