Hi, You should check what happens if you use -emit-all-errors command line flags.
It's possible that an optimisation moved the klee_assume() call outside of the if/else branch so that there is **only** one call to the klee_assume() function in the LLVM bitcode. If that is the case then KLEE will ignore any errors at the location if it is visited again. The -emit-all-errors flag will cause KLEE to report all errors even if KLEE has visited that Instruction in the LLVM bitcode before. To see what LLVM Bitcode is interpreting take a look at klee-last/assembly.ll file produced by KLEE. There is probably more to this issue because I didn't expect KLEE to generate a test case for paths with invalid constraints. Thanks, Dan On 24 January 2014 15:16, General Email <[email protected]> wrote: > Hi, > > Can anybody correct me if my notice is wrong? > > I have the following code which should generate two symbolic execution > paths; none of them can by satisfiable. However Klee doesn't show this!!! > > int main() > { > int attr1=100, attr2=12; > int y; > klee_make_symbolic(&y, sizeof(int), "y"); > > if(y>0) > { > attr1=y+7; > attr2=500; > printf("attr2 = %d\n", attr2); > klee_assume(attr1<0); //by all means this cannot be satisfied > } > else > { > attr2=800; > printf("attr2 = %d\n", attr2); > klee_assume(attr1<0); ////by all means this also cannot be satisfied > } > } > > Here is the output from Klee: > attr2 = 800 > KLEE: ERROR: invalid klee_assume call (provably false) > KLEE: NOTE: now ignoring this error at this location > attr2 = 500 > //My question why it doesn't give an error saying "invalid klee_assume call > (provably false)" here also? > KLEE: done: total instructions = 32 > KLEE: done: completed paths = 2 > KLEE: done: generated tests = 2 > > Here are the values of y generated in each test: > ktest file : 'klee-last/test000001.ktest' //This represents the else branch > (i.e., y<=0) > object 0: name: 'y' > object 0: size: 4 > object 0: data: 0 > > ktest file : 'klee-last/test000002.ktest' //This represents the then branch > (i.e., y>0) > object 0: name: 'y' > object 0: size: 4 > object 0: data: 2147483642 > > Note: using klee_assert in place of klee_assume will give assertion fail in > the two branches. > attr2 = 800 > KLEE: ERROR: ASSERTION FAIL: attr1<0 > KLEE: NOTE: now ignoring this error at this location > attr2 = 500 > KLEE: ERROR: ASSERTION FAIL: attr1<0 > > Please advise? > Thanks _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
