Thanks. I'll check out the latest build and try it again. Regards, --wm
On Sun, Oct 14, 2012 at 10:03 PM, Jonathan Neuschäfer <[email protected]> wrote: > On Thu, Oct 11, 2012 at 04:43:13PM +0100, Wei Ming Khoo wrote: >> Hi devs, >> >> I ran the following on klee-cde-v1 and klee-cde-v2 with the same outcome. >> >> #include<klee/klee.h> >> int p1(int x){ >> int x1=x; >> return x1*x1+2*x+1; >> } >> >> int p2(int x){ >> int x1=x; >> return x1*x+2*x+1; >> } >> >> int p3(int x){ >> return x*x+2*x+1; >> } >> >> int p4(int x){ >> return (x+1)*(x+1); >> } >> >> int main(){ >> int x; >> klee_make_symbolic( &x, sizeof(x), "x" ); >> // This passes without failed assertions >> //klee_assert( p3(x) == p4(x) ); >> // This passes without failed assertions >> //klee_assert( p2(x) == p4(x) ); >> // This hangs >> klee_assert( p1(x) == p4(x) ); >> return 0; >> } >> >> The first 2 tests passed, but the third hung (I killed it after 30 mins). >> I ran with -debug-print-instructions and it hangs on the klee_assert >> statement. >> I ran with -use-stp-query-pc-log but the stp-queries.qlog file was empty. >> >> Any idea what went wrong? Or what else I could try doing? > > On my system (LLVM 2.9/KLEE r165499/STP r940 built from source, llvm-gcc > from the LLVM 2.9 binary package) klee immediately returns: > > $ time klee weiming.o > KLEE: output directory = "klee-out-27" > > KLEE: done: total instructions = 127 > KLEE: done: completed paths = 1 > KLEE: done: generated tests = 1 > > real 0m0.164s > user 0m0.056s > sys 0m0.016s > > > You might be able to identify the problem by using a profiler (such as > kchachegrind), or stopping klee a few times and letting gdb print a > backtrace each time. _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
