I am not an expert but it looks like klee_get_valuel should be handled
by KLEE (in the current version), regardless of any linking problems,
but for you it wasn't.
Is it possible that you somehow have an older version of KLEE and a
newer version of the POSIX runtime libraries?
More simply, if your version of KLEE has the string "klee_get_valuel"
in "lib/Core/SpecialFunctionHandler.cpp" then this error should not be
occurring.
Thanks,
Paul
(This time sent to the mailing list.)
On 30 June 2011 00:46, Lu Zhao <luzhao at cs.utah.edu> wrote:
> 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
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
