[klee-dev] KLEE ERROR (Coreutils): failed external call: klee_init_env

[Oswaldo Olivo]

Hi,
The problem has been solved.
You were right in the issue about there being version mismatch.
I recompiled KLEE and LLVM, and the POSIX library stopped being empty. I
was probably running
an "outdated" version of KLEE with a newly built version of LLVM 2.9.
Thank you very much.
Regards,
 Oswaldo.

On Sun, Sep 15, 2013 at 3:53 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> On 15 September 2013 21:36, Oswaldo Olivo <ozzyo86 at gmail.com> wrote:
> > Hi,
> > I get an empty output from:
> >
> > llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca | grep
> > klee_init_env
>
> I should of mentioned that the version of llvm-nm you use must be part
> LLVM you built for KLEE (probably LLVM 2.9) else you get blank output.
> For example if I use llvm-nm from LLVM3.3 (which is also installed on
> my system) on a bitcode archive I see no output
>
> Check that
> $ llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
>
> gives output. If not you're **not** using the version of llvm-nm that
> comes with the version of LLVM you built for KLEE.
>
> If you do get output then you need to investigate what went wrong with
> your build of the POSIX runtime library.
>
> On my system I can do (after the runtime library is built)
>
> $ llvm-nm ~/klee/runtime/POSIX/Debug+Asserts/klee_init_env.bc
>          t __get_sym_str
>          T klee_init_env
>          U klee_init_fds
>          U klee_make_symbolic
>          U klee_mark_global
>          U klee_prefer_cex
>          U klee_range
>          U klee_report_error
>          U llvm.dbg.declare
>          U llvm.dbg.value
>          U llvm.memcpy.p0i8.p0i8.i64
>          U malloc
>
> If klee_init_env.bc doesn't exist then run the build again
> $ cd ~klee/runtime/POSIX
> $ make VERBOSE=1
>
> >
> > 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
>
> I see that error too, but I uclibc won't build for me right now so I
> can't help there.
>
> Hope that helps.
>
> Thanks,
> Dan Liew.
>
-------------- next part --------------
HTML attachment scrubbed and removed