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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
