[klee-dev] bug in klee/stp

[Sven]

hi,

You have integer arithmetics here (this is C, after all). This code:

int main(void) {
        int n = -1;
        int d = n/2;
        printf("Result: %d\n", d);
}

prints 0. The problem is that 1/2 is not an integer number, so it is
rounded down. In integer arithmetics 1/2 == 0. The same goes for -1.

So the assumption holds, because n == -1 < 0. But also n/2 == -1/2 == 0,
so the body of the if statement (and thereby the assertion) is executed.

This is not a bug in klee, but just how integer arithmetics work.

Alex

PS: I would not even attribute this to the SMT solver, both gcc and
clang generate code which handles it the same way, so klee is absolutely
correct here.

On 02/02/2016 10:06 AM, Marek Chalupa wrote:
> Hi list,
>
> I have this small trivial program:
>
>
> #include <assert.h>
>
> int main(void)
> {
>   int n;
>   klee_make_symbolic(&n, sizeof n, "n");
>   klee_assume(n < 0);
>
>   if (n/2 > 0)
>     assert(0);
>
>   return 0;
> }
>
>
> KLEE (on master from git) says that the assertion is violated,
> although since n is negative, then n/2 should not be greater than 0
> and the assert() should be never called. I suppose it is a bug, or did
> I overlook something?
>
> P.S. If the condition is just (n > 0), then everything is fine. The
> assumption can be even (n < -1) or (n < -1 && n > -10) (in which case
> I get that the assumption is provably false, which is weird also)
>
> Thanks,
> Marek
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev