Hi,
On 02/02/16 11:35, Pablo González de Aledo wrote:
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.
but clang generates sdiv instruction, it should not be equivalent to
shifting bits one position to the right, or should it? I think that sdiv
.., 2 should keep the sign, except for the corner cases like sdiv -1, 2
where I would expect the result to be 0. And we certainly don't hit the
corner cases, klee says that n == -9 or n == -5 (depends on assumptions)
Thanks
Marek
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 <[email protected]
<mailto:[email protected]>>:
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
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
