Hi,
I gave up making the build system work, and manually ran
llvm-ld libstdbuf_so-libstdbuf.o -o libstdbuf.so
to get through the build process. The compilation process completed, but
when I ran a test, I got an error saying external call to
"klee_get_valuel" failed. I tried to find the file that contains the
symbol in klee/Release/lib, but it seems that only
libkleeRuntimePOSIX.bca uses it, and no file defines it.
Any suggestions?
~/fla/example/coreutils-8.9/build-llvm/src$ klee --libc=uclibc
--posix-runtime ./echo.bc --version
KLEE: NOTE: Using model:
/home/louis/fla/klee-FLA/klee/Release/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-12"
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: __overflow
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to variable: program_invocation_name
KLEE: WARNING: undefined reference to variable:
program_invocation_short_name
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: syscall(16, 0, 21505, 56841360)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: __xstat64(1, 53265008, 58016976)
KLEE: WARNING: calling external: vprintf(53059232, 60340352)
echo (GNU coreutils) 8.9
KLEE: WARNING: calling external: klee_get_valuel(53062208)
KLEE: ERROR: /home/louis/fla/klee-FLA/klee/runtime/POSIX/fd.c:1254:
failed external call: klee_get_valuel
KLEE: NOTE: now ignoring this error at this location
Copyright (C) 2011 Free Software Foundation, Inc.
KLEE: done: total instructions = 12062
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
Thanks very much.
Lu
On 06/29/2011 05:09 PM, Lu Zhao wrote:
> Hi,
>
> I'd like to run Klee on GNU Coreutils 8.9. In order to compile the
> suite, I added two extra flags ('-O2' and '-std=c99') in klee-gcc as the
> following:
>
> for a in args:
> if a in ('-g', '-W', '-O', '-D', '-f', '-O2', '-std=c99',
> '-fnested-functions', '-pthread'):
>
> and used the following make command:
>
> make CC="$FLA_KLEE_HOME_DIR/klee/scripts/klee-gcc -std=c99"
>
>
> It seems to work for parts of the system, but at one point, I hit the
> following error:
>
> Making all in src
> make[2]: Entering directory
> `/home/louis/fla/example/coreutils-8.9/build-llvm/src'
> make all-am
> make[3]: Entering directory
> `/home/louis/fla/example/coreutils-8.9/build-llvm/src'
> CCLD libstdbuf.so
> libstdbuf_so-libstdbuf.o: file not recognized: File format not recognized
> collect2: ld returned 1 exit status
> make[3]: *** [libstdbuf.so] Error 1
>
>
> It looks like that the system linker ld instead of llvm-ld is used again
> for "libstdbuf.so." With my limited knowledge on GNU make system, I
> can't find a way to get around this. Any help is appreciated.
>
> Thanks very much.
> Lu
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
