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
