NULL ptr dereferences found with Calysto static checker

[Domagoj Babic]

Hi Ken,

On 6/15/07, Ken Raeburn <raeburn at 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/