[klee-dev] klee seems to crash when testing a simple program

[Hongxu Chen]

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 <chobbs at qnx.com> 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 listklee-dev at imperial.ac.ukhttps://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed