[klee-dev] Linking C++ runtime

[Reza Ahmadi]

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> wrote:

> On 26 September 2016 at 20:56, Eric Laberge <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
> 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
https://sites.google.com/site/reahmdi/
-------------- next part --------------
HTML attachment scrubbed and removed