I feel strange that although klee runs ok on my machine it generates a different result from yours(I run it for several times, and the statistics are the same).
KLEE: done: total instructions = 1222 KLEE: done: completed paths = 92 KLEE: done: generated tests = 84 Also, there are 2 memory error ktests generated. Here I used the simple command line "klee test.bc" without any additional options(also, without any optimizations when using llvm-gcc generating llvm IR). When using "klee -optimize test.bc", there are still 2 memory errors(the other statistics are changed since llvm IR is different). So is there any inconsistency? I also notice that there is something weired when change "int main(void)" to "int main(int argc, char** argv)": KLEE will run *much slower* on my machine for this case. Is it because the search strategy is changed? Best Regards, Hongxu Chen On Fri, Feb 22, 2013 at 2:13 AM, Chris Hobbs <[email protected]> wrote: > Works OK for me. I copied your program and went through the same steps as > you. The result was: > > KLEE: output directory = "klee-out-0" > KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer > KLEE: NOTE: now ignoring this error at this location > KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer > KLEE: NOTE: now ignoring this error at this location > > KLEE: done: total instructions = 3835 > KLEE: done: completed paths = 288 > KLEE: done: generated tests = 273 > > I'm using > > Low Level Virtual Machine (http://llvm.org/): > llvm version 2.7 > Optimized build with assertions. > Built May 24 2011 (18:07:32). > Host: i386-pc-linux-gnu > Host CPU: i686 > > Registered Targets: > x86 - 32-bit X86: Pentium-Pro and above > x86-64 - 64-bit X86: EM64T and AMD64 > > Cheers > > Chris Hobbs > QNX Software Systems > > > On 13-02-21 01:02 PM, 陈厅 wrote: > > Hi > > I use klee to test a simple program, but klee seems to crash. Who > knows the reason? The tested program is shown below: > > int pointer_test(int x, int y) { > int a[4] = {0}; > a[0] = x; > a[1] = 0; > a[2] = 1; > a[3] = 2; > if(a[x] == a[y] + 2) > return 1; > return 2; > } > int main() { > int a, b; > klee_make_symbolic(&a, sizeof(a), "a"); > klee_make_symbolic(&b, sizeof(b), "b"); > return pointer_test(a, b); > } > > The program is in a file named pointer.c. So the command line to > compile the program is: > llvm-gcc --emit-llvm -c -g pointer.c > I use this command to run this program: > klee pointer.o > > But an error happened, below is the output in terminal: > > KLEE: output directory = "klee-out-1" > klee: /home/ting/work/klee/include/klee/Expr.h:391: static > klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t, > klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) && > "invalid constant"' failed. > 0 klee 0x0000000000d5f39f > 1 klee 0x0000000000d5f8a9 > 2 libpthread.so.0 0x00002b2c542edcb0 > 3 libc.so.6 0x00002b2c54f49425 gsignal + 53 > 4 libc.so.6 0x00002b2c54f4cb8b abort + 379 > 5 libc.so.6 0x 00002b2c54f420ee > 6 libc.so.6 0x00002b2c54f42192 > 7 klee 0x0000000000540a26 > 8 klee 0x00000000005a9898 > klee::AddressSpace::resolve(klee::ExecutionState&, klee::TimingSolver*, > klee::ref<klee::Expr>, std::vector<std::pair<klee::MemoryObject const*, > klee::ObjectState const*>, std::allocator<std::pair<klee::MemoryObject > const*, klee::ObjectState const*> > >&, unsigned int, double) + 4632 > 9 klee 0x000000000057fcfa > klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, > klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 1930 > 10 klee 0x0000000000584fee > klee::Executor::executeInstruction(klee::ExecutionState&, > klee::KInstruction*) + 6910 > **11 klee 0x000000000058936b > klee::Executor::run(klee::ExecutionState&) + 1883** > 12 klee 0x0000000000589de6 > klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + > 1846 > 13 klee 0x00000000005611f7 main + 10071 > 14 libc.so.6 0x00002b2c54f3476d __libc_start_main + 237 > 15 klee 0x000000000056d3d1 > Abandon(core dumped) > > Thanks very much > > Ting Chen > > > > > > _______________________________________________ > klee-dev mailing > [email protected]https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
