Hi, The STP input language used by the .cvc files is documented here: http://sites.google.com/site/stpfastprover/stp-documentation
The PC language used by the .pc files is documented here: http://klee.llvm.org/KQuery.html Best, Cristian On 03/11/11 15:00, amitaï madar wrote: > 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<0 > I 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 > klee-dev@keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
