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
