Hi all.I want to get the path constraints of each test case that KLEE creates
in a readable way.
for example with the following program:int foo(int x) { if(x>0) return
1;return 0; }
int main() { int x; klee_make_symbolic(&x, sizeof(x), "x");
return foo(x); }
I want to get: -testcase000001.ktest is for x>0-testcase000002.ktest is for
x<0I read on the archive that someone succeed this with the .cvc files. However
the .cvc files look like this __tmpInt8 : BITVECTOR(8);__tmpInt16 :
BITVECTOR(16);__tmpInt32 : BITVECTOR(32);__tmpInt64 :
BITVECTOR(64);x_0xa05ad38 : ARRAY BITVECTOR(32) OF
BITVECTOR(8);%----------------------------------------------------ASSERT(
SBVLT(0hex00000000,(x_0xa05ad38[0hex00000003] @ (x_0xa05ad38[0hex00000002] @
(x_0xa05ad38[0hex00000001] @ x_0xa05ad38[0hex00000000]))))
);%----------------------------------------------------QUERY( FALSE );I'm
looking for a way to get from this x>0.I tried to use STP constrain solver but
was unsuccessful.There is also .pc file that looks like this:array x[4] : w32
-> w8 = symbolic(query [(Slt 0 (ReadLSB w32 0 x))] false)but
again this isn't easily understandable.Thanks for your help.
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
