[klee-dev] Linking C++ runtime

[Cristian Cadar]

Hi, improved support for C++ is not on our current list of priorities, 
but we would be of course happy to accept any contributions.

Best,
Cristian

On 26/09/16 21:28, Reza Ahmadi wrote:
> How to get to know what exactly it supports and what not? Do you have
> any idea if C++ will be supported more in the future and when?
>
> On Mon, Sep 26, 2016 at 4:15 PM, Dan Liew <dan at su-root.co.uk
> <mailto:dan at su-root.co.uk>> wrote:
>
>     On 26 September 2016 at 20:56, Eric Laberge <e.laberge at gmail.com
>     <mailto:e.laberge at gmail.com>> wrote:
>     > 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
>     >
>
>     KLEE does not properly support running C++ code. Some things might
>     work but a lot of things don't.
>
>     The option you are using is meant for use on archives of LLVM bit code
>     files, not native dynamic libraries. I protested about the inclusion
>     of this option in KLEE because I believe that the majority of the
>     linking should be done outside of KLEE but I was over-ruled.
>
>     _______________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>     <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
>
> --
> Best regards,
> Reza Ahmadi
> Ph.D. student at MASE lab
> 624 Goodwin Hall
> Queen's University, Kingston, ON
> +1 (613) 7708830 | ahmadi at cs.queensu.ca <mailto:ahmadi at cs.queensu.ca>
> https://sites.google.com/site/reahmdi/
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>