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 <[email protected]
<mailto:[email protected]>> wrote:
On 26 September 2016 at 20:56, Eric Laberge <[email protected]
<mailto:[email protected]>> 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@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
>
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
[email protected] <mailto:[email protected]>
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 | [email protected] <mailto:[email protected]>
https://sites.google.com/site/reahmdi/
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
