[27945] in Kerberos
Re: NULL ptr dereferences found with Calysto static checker
daemon@ATHENA.MIT.EDU (Domagoj Babic)
Fri Jun 15 16:40:16 2007
Message-ID: <e3684ba30706150138h20ff69b6pe17e4c1566b6b76a@mail.gmail.com>
Date: Fri, 15 Jun 2007 01:38:29 -0700
From: "Domagoj Babic" <babic.domagoj@gmail.com>
To: "Ken Raeburn" <raeburn@mit.edu>
In-Reply-To: <EDDF1297-3EDF-4EB2-A5A4-AF91A0FAA349@mit.edu>
MIME-Version: 1.0
Content-Disposition: inline
Cc: kerberos@mit.edu
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Errors-To: kerberos-bounces@mit.edu
Hi Ken,
On 6/15/07, Ken Raeburn <raeburn@mit.edu> wrote:
> >> I played a bit with Splint some time
> >> back, and one of its most glaring problems was the inability to
> >> understand stuff like that -- in particular, realloc() success and
> >> failure paths.
> >
> > Note that Calysto is a completely different beast. It's fully
> > path-sensitive. For instance, Calysto easily proves (in 0.02 sec) that
> > the following assertion is always satisfied:
> >
> > 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).
I'll reply to the rest Sun at earliest.
--
Domagoj Babic
http://www.domagoj.info/
________________________________________________
Kerberos mailing list Kerberos@mit.edu
https://mailman.mit.edu/mailman/listinfo/kerberos
