[klee-dev] Linking C++ runtime

[Cristian Cadar]

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!

Cristian

On 13/10/16 14:53, Eric Laberge wrote:
> 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
>
>
> _______________________________________________ klee-dev mailing
> list klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>