[klee-dev] Executing Coreutils Error

[Zhiyi Zhang]

Hi all,

I am using KLEE with LLVM-3.4 and want to redo the experiments of
Coreutils. Since LLVM-3.4 uses clang-3.4 but not llvm-gcc, I prefer
whole-program-llvm to compile coreutils programs. And I get .bc
files.However , when I run echo.bc with the order *klee ./echo.bc*, there
is an error as following:

*KLEE: output directory is
"/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/./klee-out-6"*
*KLEE: WARNING ONCE: function "vasnprintf" has inline asm*
*KLEE: WARNING: undefined reference to function: __ctype_b_loc*
*KLEE: WARNING: undefined reference to function: __ctype_get_mb_cur_max*
*KLEE: WARNING: undefined reference to function: __errno_location*
*KLEE: WARNING: undefined reference to function: __fpending*
*KLEE: WARNING: undefined reference to function: __overflow*
*KLEE: WARNING: undefined reference to function: atexit*
*KLEE: WARNING: undefined reference to function: bindtextdomain*
*KLEE: WARNING: undefined reference to function: dcgettext*
*KLEE: WARNING: undefined reference to function: fclose*
*KLEE: WARNING: undefined reference to function: fprintf*
*KLEE: WARNING: undefined reference to function: fputs_unlocked*
*KLEE: WARNING: undefined reference to function: fwrite*
*KLEE: WARNING: undefined reference to function: getenv*
*KLEE: WARNING: undefined reference to function: getopt_long*
*KLEE: WARNING: undefined reference to function: iswprint*
*KLEE: WARNING: undefined reference to function: mbrtowc*
*KLEE: WARNING: undefined reference to function: mbsinit*
*KLEE: WARNING: undefined reference to function: memcmp*
*KLEE: WARNING: undefined reference to variable: opterr*
*KLEE: WARNING: undefined reference to variable: optind*
*KLEE: WARNING: undefined reference to function: printf*
*KLEE: WARNING: undefined reference to function: setlocale*
*KLEE: WARNING: undefined reference to function: snprintf*
*KLEE: WARNING: undefined reference to variable: stderr*
*KLEE: WARNING: undefined reference to variable: stdout*
*KLEE: WARNING: undefined reference to function: strlen*
*KLEE: WARNING: undefined reference to function: textdomain*
*KLEE: WARNING: undefined reference to function: error (UNSAFE)!*
*KLEE: WARNING ONCE: calling external: getenv(176076616)*
*KLEE: WARNING ONCE: calling external: setlocale(6, 176076944)*
*KLEE: ERROR:
/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/../../src/echo.c:138:
external modified read-only object*
*KLEE: NOTE: now ignoring this error at this location*

*KLEE: done: total instructions = 6*
*KLEE: done: completed paths = 1*
*KLEE: done: generated tests = 1*

Then I use the order* klee --licb=uclibc --posix-runtime ./echo.bc
--sym-arg 3, *the error is as following:

*KLEE: NOTE: Using klee-uclibc :
/home/loveling10/klee/build/Release+Asserts/lib/klee-uclibc.bca*
*KLEE: NOTE: Using model:
/home/loveling10/klee/build/Release+Asserts/lib/libkleeRuntimePOSIX.bca*
*KLEE: output directory is
"/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/./klee-out-7"*
*KLEE: WARNING ONCE: function "vasnprintf" has inline asm*
*KLEE: WARNING: undefined reference to function: __ctype_b_loc*
*KLEE: WARNING: undefined reference to function: __overflow*
*KLEE: WARNING: undefined reference to function: bindtextdomain*
*KLEE: WARNING: undefined reference to function: dcgettext*
*KLEE: WARNING: undefined reference to function: textdomain*
*KLEE: WARNING: executable has module level assembly (ignoring)*
*KLEE: WARNING ONCE: calling external: syscall(54, 0, 21505, 185983048)*
*KLEE: WARNING ONCE: calling __user_main with extra arguments.*
*KLEE: WARNING ONCE: calling external: bindtextdomain(181575080, 181575016)*
*KLEE: WARNING ONCE: calling external: textdomain(181575080)*
*KLEE: WARNING ONCE: calling external: __overflow(181649140, 10)*
*KLEE: ERROR: /usr/include/i386-linux-gnu/bits/stdio.h:107: failed external
call: __overflow*
*KLEE: NOTE: now ignoring this error at this location*


*Segmentation fault (core dumped)*
What should I do to solve these problems?

Thank you very much!
Zhiyi Zhang
-------------- next part --------------
HTML attachment scrubbed and removed