Hello,
1. You may replace && with & as suggested if all operands are boolean
values and have no side-effects. This can work well in most scenarios.
See below to understand why.
2. The tricky part in your example is not about klee_assume, but how it
interacts with the code generated by the compiler. Consider the simpler
code below:
int b = (((c==2)||(d==1)));
klee_assume(b && "b cannot be true");
which produces a similar output:
KLEE: output directory = "klee-out-0"
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 53
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3
The code gets compiled to
if (c == 2) {
b = 1;
} else if (d == 1) {
b = 1;
} else {
b = 0;
}
klee_assume(b && "b cannot be true");
Since there are 3 paths and all are feasible, klee_assume will be called
3 times with trivial arguments
klee_assume(1)
klee_assume(1)
klee_assume(0)
The first two paths go further while the 3rd is terminated, which is
pretty much what is intended. Ideally the paths which satisfy the assume
would be merged, but that's a different story and klee has only some
experimental support for it.
Regarding your other question (21 paths vs 9 test cases), that's because
by default klee generates a single test case per error. Use
--emit-all-errors to get all the test cases.
Paul
On 11/11/13 14:59, Urmas Repinski wrote:
Hi, AKhalil.
I suggest to try instead of using of logical 'and - &&' and 'or - ||'
use bitwise 'and - &' and 'or - |'.
Difference practically between them is following: if logical && is used
, a && b as example, and if a is false, then whole expression is false
and b is not checked at all.
If to use bitwise &, then second parameter is checked too.
Practically in this case there is no difference what form to use, but i
have no idea how klee_assume() function exactly is implemented and it is
safer to use bitwise 'and' and 'or' operators instead of logical ones.
There is no misunderstanding, simply i suggest to use safer condition
form, try to replace &&-s with &-s, and ||-s with |-s.
Urmas Repinski.
------------------------------------------------------------------------
Date: Mon, 11 Nov 2013 06:27:30 -0800
From: [email protected]
To: [email protected]
Subject: [klee-dev] Need to understand how klee_assume() works
Hello,
I have the following program and I want to create the set of test cases
and their corresponding constraints that only satisfy the conditions
included in the klee_assume() expression.
#include <klee/klee.h>
int main()
{
int c,d,e,f;
klee_make_symbolic(&c, sizeof(c), "c");
klee_make_symbolic(&d, sizeof(d), "d");
klee_make_symbolic(&e, sizeof(e), "e");
klee_make_symbolic(&f, sizeof(f), "f");
klee_assume((((c==2)||(d==1))&&((e>=2)||((f<600)&&(e>=1))))||(((c ==
1)||(d == 0))&&((e>=3)||((f<600)&&(e>=2)))));
return 0;
}
When I run this program, klee gives me the following:
KLEE: output directory = "klee-out-14"
KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12:
invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 242
KLEE: done: completed paths = 21
KLEE: done: generated tests = 9
My question is why only 9 tests are generated however there are 21
paths? And if klee generates tests for only satisfiable paths, why the
message "KLEE: ERROR:
/home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid
klee_assume call (provably false)" is generated and what does it indicate?
As you notice I used the junction operators && and ||, are these
operators the right ones to use? I guess I have some misunderstanding of
the use of klee_assume() function, so can I have more explanation of its
usage?
Thanks
AKhalil
_______________________________________________ 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
