Thanks for sharing your experience, Eric. C++ is not officially supported by KLEE, and we don't have a full list of features that we support -- although this email and Dan's recent email did a good job highlighting what we do not support. As I said, we welcome any contributions!


On 13/10/16 14:53, Eric Laberge wrote:

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 <> a
écrit :


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

klee@77c9c1d55f4a:/tmp$ klee
hello.bc KLEE: Linking in library:

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
0x00002ac38e4ee330 3       0x00002ac390babc37 gsignal +
55 4       0x00002ac390baf028 abort + 328 5
0x00002ac390ba4bf6 6       0x00002ac390ba4ca2 7  klee
0x00000000005c8135 klee::linkWithLibrary(llvm::Module*, std::string
const&) + 3925 8  klee            0x0000000000576c6c main + 5740 9       0x00002ac390b96f45 __libc_start_main + 245 10 klee
0x00000000005718d9 Aborted

Thanks! — Eric Laberge

_______________________________________________ klee-dev mailing

klee-dev mailing list

Reply via email to