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
[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
