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? ThanksAKhalil _______________________________________________ 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
