On Fri, May 8, 2009 at 9:48 AM, Cristian Zamfir <cristian.zamfir at epfl.ch>
wrote:
>
> Hi,
>
> I managed to compile Apache using the normal compile process, after
> hacking the libtool and Makefiles to compile and link the LLVM bitcode.
Nice!
> However, when running with KLEE, I get the error "do not support
> dependent libraries".
> This is from Executor.cpp
>
> void Executor::initializeGlobals(ExecutionState &state) {
> ? Module *m = kmodule->module;
>
> ....
>
> ? demand(m->lib_begin() == m->lib_end(),
> ? ? ? ? ?"XXX do not support dependent libraries");
>
> Is there any particular reason why these are not supported by KLEE, or
> should I try to add support for that?
I don't think I ever saw these in practice, but I believe these are
added as reference to external references to binary libraries. In
theory we could make them work using the external function calls, but
probably what you want to do instead is to get the build process to
link in bitcode versions of the required libraries, otherwise things
aren't "really" going to work.
- Daniel
> Thanks,
> Cristi
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.Stanford.EDU
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>