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

[陈厅]

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       0x00002b2c54f420ee
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
  
-------------- next part --------------
HTML attachment scrubbed and removed