[klee-dev] bug in klee/stp

[Pablo González de Aledo]

Hi Marek :-)

Have in mind that klee uses bit-vector arithmetics to interact with the SMT
solver, and things can get a little bit weird when you do so.

if n is a '1' followed by 31 zeros (in binary), it is indeed a negative
number, but when you divide by two (shift the one one position to the
right), it magically becomes positive.

You can see the counter-example generated by klee with "ktest-tool
--write-ints klee-last/test000001.ktest" and the queries to the SMT-solver
with "klee -use-query-log=all:smt2 file.bc"

Regards.

2016-02-02 10:06 GMT+01:00 Marek Chalupa <mchqwerty at gmail.com>:

> 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
-------------- next part --------------
HTML attachment scrubbed and removed