Hi Wenhua,
In your example, buf2 is read out of bounds, not buf. buf2 isn't
NULL-terminated, so strcpy() continues to read past the end of it.
Hope that helps.
-David
On Oct 27, 2010, at 11:11 AM, Wang, Wenhua wrote:
> 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
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20101027/69e9b6fd/attachment.html
