Hi Cristi and George,
I think I got a false positive from Klee.
My example program is simple.
I have listed all the related information in the following.
Could you double check it ?
1.
Source code of demo.c
~~~~
#include <string.h>
int main() {
char buf[100];
char buf2[9];
klee_make_symbolic(buf2 ,9,"input2");
strcpy(buf,buf2);
return 0;
}
~~~~
2.
Compiling demo.c and running demo.o
Here, you can see Klee reported a memory error "out of bound pointer".
~~~~
root at wwh-desktop:/usr/llvm2.7/llvm-2.7/klee/mytest# llvm-gcc --emit-llvm -c
demo.c
root at wwh-desktop:/usr/llvm2.7/llvm-2.7/klee/mytest# klee --libc=uclibc
demo.oKLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: ioctl(0, 21505, 176545720)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: ERROR: /usr/llvm2.7/llvm-2.7/klee-uclibc/libc/string/strcpy.c:27: memory
error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 10111
KLEE: done: completed paths = 10
KLEE: done: generated tests = 10
~~~~
3.
Here, you can see the 10th test failed.
~~~~
root at wwh-desktop:/usr/llvm2.7/llvm-2.7/klee/mytest/klee-last# ls
assembly.ll test000001.ktest test000006.ktest test000010.pc
info test000002.ktest test000007.ktest test000010.ptr.err
messages.txt test000003.ktest test000008.ktest warnings.txt
run.istats test000004.ktest test000009.ktest
run.stats test000005.ktest test000010.ktest
~~~~
4.
The content of 10th test.
~~~~
root at wwh-desktop:/usr/llvm2.7/llvm-2.7/klee/mytest# ktest-tool
klee-last/test000010.ktest
ktest file : 'klee-last/test000010.ktest'
args : ['demo.o']
num objects: 1
object 0: name: 'input2'
object 0: size: 9
object 0: data: '\x02\x01\x01\x01\x01\x01\x01\x01\x01'
~~~~
Here, we can see Klee just generated an input that is a string with 9
characters.
The 9-character string should not overflow a buffer that can hold 100
characters.
Could you explain a little more about how Klee perform the bounds checking job?
Thanks !
Sincerely,
Wenhua Wang
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20101027/ae338c8c/attachment.html
