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.labe...@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@77c9c1d55f4a:/tmp$ cat hello.cpp > int main() { > return 0; > } > > klee@77c9c1d55f4a:/tmp$ clang++ -c hello.cpp -emit-llvm -g -o hello.bc > > klee@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 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev