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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
