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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
