Hi, I get an empty output from: llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca | grep klee_init_env
I tried recompiling UCLIBC, like the getting started tutorial says, and I don't really get any errors after make. However, I do get a suspicious warning : cc1: warning: unrecognized gcc debugging option: N The output after make looks like this: __________________________________ ./extra/scripts/conf-header.sh .config > include/bits/uClibc_config.h cc1: warning: unrecognized gcc debugging option: N make locale_headers zcat extra/locale/uClibc-locale-030818.tgz | tar -xv -C extra/locale/ -f - c8tables.h locale_data.c locale_mmap.h ............. ............. CC libc/unistd/usleep.os CC libc/misc/internals/__uClibc_main.os CC libc/stdlib/atexit.os STRIP -x -R .note -R .comment lib/libc.a AR cr lib/libc.a _________________________________ Thanks for your help. Regards, Oswaldo. On Sun, Sep 15, 2013 at 10:37 AM, Daniel Liew <[email protected]>wrote: > Hi, > > It seems that the POSIX runtime library (libkleeRuntimePOSIX.bca) is > linked in as you would get an assertion error if it was not. However > the call to klee_init_env() should not fail and should not be treated > as an external. > > The first thing I would check is that klee_init_env is present in > libkleeRuntimePOSIX.bca by doing > > $ llvm-nm Debug+Asserts/lib/libkleeRuntimePOSIX.bca/libkleeRuntimePOSIX.bca > | grep klee_init_env > Debug+Asserts/lib/libkleeRuntimePOSIX.bca(klee_init_env.b): > T klee_init_env > > Note I built the POSIX runtime library as debug so your output may be > slightly different but llvm-nm should show that klee_init_env is in > the "text section" (T). If klee_init_env is missing or is not in the > text section (.e.g (U) undefined) then libkleeRuntimePOSIX.bca didn't > built correctly. > > If libkleeRuntimePOSIX.bca did built correctly the next thing to look > at is the linking performed by KLEE. Take a look at > klee-last/assembly.ll . This file is generated when you run klee and > it is the llvm bitcode module (i.e. KLEE has already done all the > linking necessary) that klee will interpret. > > You should find that somewhere in user_main() a call is made to > klee_init_env e.g. > > define i32 @__user_main(i32 %argc, i8** %argv) nounwind { > entry: > %argcPtr = alloca i32 > %argvPtr = alloca i8** > store i32 %argc, i32* %argcPtr > store i8** %argv, i8*** %argvPtr > call void @klee_init_env(i32* %argcPtr, i8*** %argvPtr) > ... > } > > and that there is a declaration of klee_init_env in the module too > > define void @klee_init_env(i32* nocapture %argcPtr, i8*** nocapture > %argvPtr) nounwind { > entry: > %new_argv = alloca [1024 x i8*], align 8 > %sym_arg_name = alloca [5 x i8], align 1 > .... > } > > Your output implies that there is no declaration of klee_init_env() in > assembly.ll but you should check this. > > Hope this helps. > > Thanks, > Dan Liew. > > On 14 September 2013 23:07, Oswaldo Olivo <[email protected]> wrote: > > Hi, > > > > I have followed the steps for compiling Klee, UCLIBC, STP and Coreutils > > given > > in : > > > > http://klee.llvm.org/GetStarted.html > > > > and > > > > http://klee.llvm.org/TestingCoreutils.html > > > > After running the command from step 3 of the coreutils tutorial: > > > > klee --libc=uclibc --posix-runtime ./cat.bc --version > > > > > > I get the following output, with the error "failed external call: > > klee_init_env" : > > ____________________________________________ > > > > KLEE: NOTE: Using model: > > /home/oswaldo/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca > > KLEE: output directory = "klee-out-8" > > KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction > > KLEE: WARNING: undefined reference to function: close > > KLEE: WARNING: undefined reference to function: close_stdout > > KLEE: WARNING: undefined reference to function: fcntl > > KLEE: WARNING: undefined reference to function: fstat > > KLEE: WARNING: undefined reference to function: fstat64 > > KLEE: WARNING: undefined reference to function: full_write > > KLEE: WARNING: undefined reference to function: ioctl > > KLEE: WARNING: undefined reference to function: klee_div_zero_check > > KLEE: WARNING: undefined reference to function: klee_init_env > > KLEE: WARNING: undefined reference to function: lseek > > KLEE: WARNING: undefined reference to function: lseek64 > > KLEE: WARNING: undefined reference to function: memmove > > KLEE: WARNING: undefined reference to function: open > > KLEE: WARNING: undefined reference to function: open64 > > KLEE: WARNING: undefined reference to function: quote > > KLEE: WARNING: undefined reference to function: read > > KLEE: WARNING: undefined reference to function: readlink > > KLEE: WARNING: undefined reference to function: safe_read > > KLEE: WARNING: undefined reference to function: version_etc > > KLEE: WARNING: undefined reference to function: write > > KLEE: WARNING: undefined reference to function: xmalloc > > KLEE: WARNING: undefined reference to function: kill (UNSAFE)! > > KLEE: WARNING: executable has module level assembly (ignoring) > > KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 176221000) > > KLEE: WARNING ONCE: calling __user_main with extra arguments. > > KLEE: WARNING ONCE: calling external: klee_init_env(176196176, 176196064) > > KLEE: ERROR: > /home/oswaldo/coreutils-6.11/obj-llvm/src/../../src/cat.c:514: > > failed external call: klee_init_env > > KLEE: NOTE: now ignoring this error at this location > > > > KLEE: done: total instructions = 9336 > > KLEE: done: completed paths = 1 > > KLEE: done: generated tests = 1 > > > > ________________________________ > > > > Any ideas of what the problem is ? > > Is it not loading posix libraries properly ? > > I'm compiling this on Ubuntu 12.04. > > Thanks, > > Oswaldo. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
