NULL ptr dereferences found with Calysto static checker

[Ken Raeburn]

On Jun 15, 2007, at 04:38, Domagoj Babic wrote:
>> > int f(int a, int b) {
>> >    int a1;
>> >    if (a%2) { a1 = a + 1; }
>> >    else { a1 = a; }
>> >    int c = a1 * a1;
>> >    assert(c % 4 == 0);
>> > }
>>
>> If I felt like being picky, I'd point out that overflow in signed
>> integer arithmetic in C produces undefined results according to the
>> standard, so the assertion may not be met. :-)
>
> If it addition overflows, a1+1=0, hence 0*0%4=0. The assertion is
> always true. Calysto and Spear preserve the properties of 2's  
> complement
> (bit-vector | modular arithmetic).

Actually, in two's complement with wrapping signed arithmetic, the  
overflow case would be a=INT_MAX and a1=a+1=INT_MIN, which would  
still be even.

But the C spec doesn't require two's complement, for historical  
reasons, or wrapping signed arithmetic.  For unsigned types the  
result of overflow is defined to wrap (modular arithmetic), but for  
built-in signed types, computing a result outside the range of the  
type can result in a trap or other behavior.  (Sorry to harp on it,  
but lately I've spent too much time in a forum where people think  
they can tell you exactly what behavior expressions like "i = ++i + + 
+i" is required to produce.)

 From what I've read, modern versions of GCC have optimizations that  
take advantage of this undefined behavior to make transformations  
that speed up the code but don't give the wrap-on-signed-overflow  
result.  So, actually, proving whether or not signed arithmetic can  
overflow may also be useful...

Ken