[klee-dev] Does klee support c++?

[Sang Phan]

I tried KLEE with a couple of C++ programs before without any problem.

Did you run KLEE with the -posix-runtime option?

As I understand, KLEE works on LLVM bitcode, so it doesn't care what is in
the front-end, as long as they can be compiled.

Sang

On Sun, Jul 29, 2018 at 9:25 PM, 허희성 <gjgmltjd at naver.com> wrote:

> Hello all,
>
> I tried to run a very simple c++ program, but immediately got segmentation
> fault message.
>
> #include <iostream>
>
> #include <klee/klee.h>
>
> using namespace std;
>
> int main(void)
>
> {
>
>    int a;
>
>    klee_make_symbolic(&a, sizeof(a), "a");
>
>    if (a == 1)
>
>       cout << "a ==1";
>
>    else
>
>       cout << "a != 1"
>
>    return 0;
>
> }
>
> Result:
>
> clang -x c++ -c -g -emit-llvm main.cpp
>
>
>   ... some undefined reference library function msg ...
>
>
> KLEE: ERROR: .../main.cpp:18 failed external call: _ZStlsISt11char_
> traitsIcEERSt13basic_ostreamIcT_ES5_PKc
>
> KLEE: NOTE: now ignoring this error at this location
>
> Segmentation fault(core dumped)
>
>
> I found that seg fault is occured when klee handle cout function.
>
> When I replaced cout function to printf (I added stdio.h header), klee
> made 2 path but still got segfaulted.
>
> GDB core debugging result:
>
> #0 ... in ??()
>
> #1 in __run_exit_handlers (...) at exit.c:82
>
> #2 in __ GI_exit (...) at exit.c:104:
>
> #3 in __libc_start_main (...)
>
> #4 in __start()
>
> It seems that klee doesn't support c++ properly.
>
> If I remove iostream header & cout function from source code, everything
> is fine.
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed