[klee-dev] linker problem

[Jonathan Neuschäfer]

On Tue, Jun 04, 2013 at 04:05:17AM -0700, Alexandru Ionut Diaconescu wrote:
> Hello,
> 
> I am trying to build a KLEE project (on a new environment) and I have the
> following problem:
> 
> echo Testing...
> Testing...
> echo There should be no assertion fails!
> There should be no assertion fails!
> klee -taint=direct taint_direct.o
> KLEE: output directory = "klee-out-8"
> klee: error: Cannot find linker input
> '/tmp/taint/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'
> klee: ModuleUtil.cpp:51: llvm::Module* klee::linkWithLibrary(llvm::Module*,
> const string&): Assertion `0 && "linking in library failed!"' failed.
> 0  klee            0x00002ac2ccf576df
> 1  klee            0x00002ac2ccf57c49
> 2  libpthread.so.0 0x00002ac2cd8ffcb0
> 3  libc.so.6       0x00002ac2ce55b425 gsignal + 53
> 4  libc.so.6       0x00002ac2ce55eb8b abort + 379
> 5  libc.so.6       0x00002ac2ce5540ee
> 6  libc.so.6       0x00002ac2ce554192
> 7  klee            0x00002ac2cc78779d klee::linkWithLibrary(llvm::Module*,
> std::string const&) + 253
> 8  klee            0x00002ac2cc783954
> klee::KModule::prepare(klee::Interpreter::ModuleOptions const&,
> klee::InterpreterHandler*) + 2180
> 9  klee            0x00002ac2cc73715d
> klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions
> const&) + 157
> 10 klee            0x00002ac2cc71a94a main + 3546
> 11 libc.so.6       0x00002ac2ce54676d __libc_start_main + 237
> 12 klee            0x00002ac2cc72da6d
> make: *** [direct] Aborted (core dumped)
> 
> The problem is KLEE is trying to look into
> /tmp/taint/....libkleeRuntimeIntrinsic.bca  and not into
> /home/myfolder/taint/...where libkleeRuntimeIntrinsic.bca does exist. I
> think I set correctly all the paths when I installed KLEE (and not from the
> /tmp/ folder).
> 
> Do you know how I can solve this problem ?

We need more information. Which version of klee do you use?
What where the exact commands you used to build/test klee?
How did you obtain taint_direct.o, what does it contain?


Regards,
Jonathan Neuschäfer