Hi,
On 02/02/16 12:08, Sven wrote:
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.
if n/2 == -1/2 == 0 then condition (n/2 > 0) --> (0 > 0) is false, isn't
it? So the assert should not be called for n == -1
If I use:
klee_assume(n < 0)
klee_assume(n > -10)
then klee hits the assert and ktest-tool says that n == -9 on that path.
When I use:
klee_assume(n == -9)
no assertion is hit. That does not look like correct to me... or I just
still don't get what's happening here
Thanks,
Marek
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
[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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
