[27940] in Kerberos
Re: NULL ptr dereferences found with Calysto static checker
daemon@ATHENA.MIT.EDU (Ken Raeburn)
Fri Jun 15 05:30:38 2007
In-Reply-To: <e3684ba30706150138h20ff69b6pe17e4c1566b6b76a@mail.gmail.com>
Mime-Version: 1.0 (Apple Message framework v752.2)
Message-Id: <8DC6861C-5D7D-4D89-B648-9BD93914BFA8@mit.edu>
From: Ken Raeburn <raeburn@mit.edu>
Date: Fri, 15 Jun 2007 05:29:49 -0400
To: "Domagoj Babic" <babic.domagoj@gmail.com>
Cc: kerberos@mit.edu
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Errors-To: kerberos-bounces@mit.edu
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
________________________________________________
Kerberos mailing list Kerberos@mit.edu
https://mailman.mit.edu/mailman/listinfo/kerberos
