Hi, Most likely this is an invalid memory access which doesn't show up when running the program natively (which is what klee-replay does).
Best, Paul On 26/10/11 04:15, [email protected] wrote: > 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 _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
