On Wed, Aug 11, 2010 at 05:04:40PM +0800, Kuan Xiang Wen wrote: > Hello, > > I tried to use klee testdoc1.o command in terminal and got this error. > > xiangwen at xiangwen-laptop:~/klee-nush/testcases$ klee ./testdoc1.o > KLEE: output directory = "klee-out-5" > klee: error: Cannot find linker input > '/home/xiangwen/klee-nush/Release/lib/libkleeRuntimeIntrinsic.bca' > klee: ModuleUtil.cpp:42: llvm::Module* klee::linkWithLibrary(llvm::Module*, > const std::string&): Assertion `0 && "linking in library failed!"' failed. > 0 klee 0x08911e18 > Aborted > > I only have the .a files in Release/lib directory. In addition, renaming the > .a file extension to .bca seems to fix the problem. Is it safe to do this?
Hi Xiang, The .a files contain native code, and won't work with Klee. They are built if LLVM was configured without llvm-gcc in your $PATH. Try reconfiguring LLVM with llvm-gcc and recompiling Klee. Thanks, -- Peter
