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

[Chris Hobbs]

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 list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed