[klee-dev] Linking C++ runtime

[Eric Laberge]

Hi!

I managed to get my app working with a moderately complex C++ library and program (about 13000 lines of code) by replacing some C++ library functions with plain C ones (std::string -> char*, std::cout -> std::printf, std::fstream -> std::FILE*, std::stringstream -> std::sprintf, etc.) and compiling without C++ features ( -emit-llvm -g -fno-exceptions -fno-rtti -O0 ). I had to disable optimizations as it was crashing KLEE somehow.

:-)

— 
Eric Laberge


> Le 26 sept. 2016 à 15:56, Eric Laberge <e.laberge at gmail.com> a écrit :
> 
> Hello!
> 
> I am trying to get KLEE running a simple C++ app through Docker, but am obviously not doing it correctly. Anybody got it working?
> 
> Here’s what I got:
> 
> klee at 77c9c1d55f4a:/tmp$ cat hello.cpp
> int main() {
>  return 0;
> }
> 
> klee at 77c9c1d55f4a:/tmp$ clang++ -c hello.cpp -emit-llvm -g -o hello.bc
> 
> klee at 77c9c1d55f4a:/tmp$ klee -link-llvm-lib=/usr/lib/gcc/x86_64-linux-gnu/4.8/libstdc++.so hello.bc
> KLEE: Linking in library: /usr/lib/gcc/x86_64-linux-gnu/4.8/libstdc++.so.
> 
> klee: /usr/lib/llvm-3.4/build/include/llvm/Support/Casting.h:97: static bool llvm::isa_impl_cl<llvm::object::ObjectFile, const llvm::object::Binary *>::doit(const From *) [To = llvm::object::ObjectFile, From = const llvm::object::Binary *]: Assertion `Val && "isa<> used on a null pointer"' failed.
> 0  klee            0x0000000000dd4432 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
> 1  klee            0x0000000000dd4224
> 2  libpthread.so.0 0x00002ac38e4ee330
> 3  libc.so.6       0x00002ac390babc37 gsignal + 55
> 4  libc.so.6       0x00002ac390baf028 abort + 328
> 5  libc.so.6       0x00002ac390ba4bf6
> 6  libc.so.6       0x00002ac390ba4ca2
> 7  klee            0x00000000005c8135 klee::linkWithLibrary(llvm::Module*, std::string const&) + 3925
> 8  klee            0x0000000000576c6c main + 5740
> 9  libc.so.6       0x00002ac390b96f45 __libc_start_main + 245
> 10 klee            0x00000000005718d9
> Aborted
> 
> Thanks!
> — 
> Eric Laberge