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

허희성 gjgmltjd at naver.com
Mon Jul 30 05:25:21 BST 2018


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.
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list