Hi, Now, I am studying klee and use it to test some programs. I test wget and find a bug, but there is something I can't understand clearly. the step I do the experiments is listed as below:
1) I compiler the wget program and get wget.bc file. then 2)yun@yun-pc:~/wget-1.5.3/obj/src$ klee --libc=uclibc --posix-runtime ./wget.bc www.google.com the output of klee show that there is a bug in host.c file because of bound of out of bound pointer. *********************************************************************************************************** yun@yun-pc:~/wget-1.5.3/obj/src$ klee --libc=uclibc --posix-runtime ./wget.bc www.google.com [00000.036] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 [00000.036] Cloud9: Debug: Using uClibc path /home/yun/cloud/uclibc [00000.121] Cloud9: Debug: Using uClibc path /home/yun/cloud/uclibc [00000.122] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 KLEE: NOTE: Using model: /home/yun/cloud/cloud9/Release+Asserts/lib/libkleeRuntimePOSIX.bca [00000.199] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 KLEE: output directory = "klee-out-0" [00000.199] Cloud9: Info: Instrumentation started WARNING: this target does not support the llvm.stacksave intrinsic. KLEE: WARNING: function "iwrite" has inline asm KLEE: WARNING: function "iread" has inline asm KLEE: WARNING: function "acceptport" has inline asm KLEE: WARNING: undefined reference to function: __ctype_b_loc KLEE: WARNING: undefined reference to function: __ctype_tolower_loc KLEE: WARNING: undefined reference to function: __ctype_toupper_loc KLEE: WARNING: undefined reference to function: __libc_fcntl KLEE: WARNING: undefined reference to function: bindtextdomain KLEE: WARNING: undefined reference to function: dcgettext KLEE: WARNING: undefined reference to function: gethostbyaddr KLEE: WARNING: undefined reference to function: gethostbyname KLEE: WARNING: undefined reference to function: snprintf KLEE: WARNING: undefined reference to function: textdomain KLEE: WARNING: undefined reference to function: kill (UNSAFE)! KLEE: WARNING: calling external: stat(140052474042240, 140052474050912) KLEE: WARNING: calling external: syscall(5, 1, 140052474054304) KLEE: WARNING: calling external: snprintf(140052474048704, 16, 140052474048832, 140052474048896, 0) KLEE: WARNING: _ioctl_file: operation not supported on symbolic files KLEE: WARNING: calling __user_main298 with extra arguments. KLEE: WARNING: calling __user_main with extra arguments. KLEE: WARNING: calling external: bindtextdomain(140052473969440, 140052473969504) KLEE: WARNING: calling external: textdomain(140052473969440) KLEE: WARNING: signal: silently ignoring KLEE: WARNING: calling external: __ctype_toupper_loc() Attempting to open: /etc/TZ --17:03:26-- http://www.google.com:80/ => `index.html.3' KLEE: WARNING: calling external: dcgettext(0, 140052473950368, 5) Connecting to www.google.com:80... KLEE: WARNING: calling external: gethostbyname(140052474229248) KLEE: ERROR: /home/yun/cloud/wget-1.5.3/obj/src/../../src/host.c:160: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location [00001.008] Cloud9: Debug: Code coverage is 0/0 (local) and 0/0 (global)... KLEE: done: total instructions = 247972 KLEE: done: completed paths = 3 KLEE: done: generated tests = 1 [00002.001] Cloud9: Info: Instrumentation interrupted. Stopping. ************************************************************************************************************* 3) yun@yun-pc:~/wget-1.5.3/obj/src$ klee-replay ./wget ./klee-last/test000001.ktest the output of klee show that there is no error and the execution of program is normal ************************************************************************************************************** yun@yun-pc:~/wget-1.5.3/obj/src$ klee-replay ./wget ./klee-last/test000001.ktest WARNING: klee_assume(0)! klee-replay: TEST CASE: ./klee-last/test000001.ktest klee-replay: ARGS: "./wget" "www.google.com" --11:16:21-- http://www.google.com:80/ => `index.html.3' Connecting to www.google.com:80... connected! HTTP request sent, awaiting response... 302 Found Location: http://www.google.com.hk/url?sa=p&hl=zh-CN&pref=hkredirect&pval=yes&q=http://www.google.com.hk/&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg [following] --11:16:21-- http://www.google.com.hk:80/url?sa=p&hl=zh-CN&pref=hkredirect&pval=yes&q=http%3A/www.google.com.hk/&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg => `&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg' Connecting to www.google.com.hk:80... connected! HTTP request sent, awaiting response... 200 OK Length: unspecified [text/html] 0K -> . 11:16:21 (1.10 MB/s) - `&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg' saved [1155] klee-replay: EXIT STATUS: NORMAL (0 seconds) *************************************************************************************************************** So I think this is a false bug report or there is something else I don't understand it clearly _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
