[klee-dev] segmentation fault

[Reza Ahmadi]

Hi all,

I tried to run a simple .cpp code using Klee. My code includes some
float-related operations. If I remove the float-related stuff, then, Klee
is successful in generating 3 test cases but fails if I include float
things.

My questions (sorry if too stupid, I am new to Klee):

1- Is Klee supposed to support C++ (or just C?). I know that Klee runs llvm
bytecodes, but I am just curious as there is no C++ sample code in Klee
tutorials. If C++ is supported, fully supported? to what extent?

2- Does Klee support float data type (or any floating point in general)? It
crashed totally if I include some float-related functions in my code
(function GetDiv in the below code).

Here is my code .cpp code:

/*
 * First KLEE tutorial: testing a small function
 */

#include <klee/klee.h>
#include <iostream>
using namespace std;

class MyMath{
public:
int GetPow2 (int g1){
int res = 0;
if (g1 >= 10000)
  //assuming too big input, just to add another branch
  return -1;
if ( g1 == 0 )
  return 0;
else
  res = g1 * g1;
// cout << "res is" << res << endl;
return res;
}

float GetDiv(int x, int y){
if (x <= 0)
 throw;// "devision by zero!"
return x/y;
}

};

int main() {

  int p, x1, y1;

  klee_make_symbolic(&p, sizeof(p), "input1");
  klee_make_symbolic(&x1, sizeof(x1), "input2");
  klee_make_symbolic(&y1, sizeof(y1), "input3");

  MyMath myMath;
  int pow = myMath.GetPow2(p);
  float div = myMath.GetDiv (x1, y1);
  return 1;
}


Klee's output:

KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev
KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev
KLEE: WARNING: undefined reference to function: __cxa_atexit
KLEE: WARNING: undefined reference to function: __cxa_rethrow
KLEE: WARNING: undefined reference to variable: __dso_handle
KLEE: WARNING: undefined reference to function: pthread_cancel
KLEE: WARNING: undefined reference to function: pthread_create
KLEE: WARNING: undefined reference to function: pthread_getspecific
KLEE: WARNING: undefined reference to function: pthread_key_create
KLEE: WARNING: undefined reference to function: pthread_key_delete
KLEE: WARNING: undefined reference to function: pthread_mutex_init
KLEE: WARNING: undefined reference to function: pthread_mutex_lock
KLEE: WARNING: undefined reference to function: pthread_mutex_trylock
KLEE: WARNING: undefined reference to function: pthread_mutex_unlock
KLEE: WARNING: undefined reference to function: pthread_mutexattr_destroy
KLEE: WARNING: undefined reference to function: pthread_mutexattr_init
KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype
KLEE: WARNING: undefined reference to function: pthread_once
KLEE: WARNING: undefined reference to function: pthread_setspecific
KLEE: WARNING ONCE: calling external: _ZNSt8ios_base4InitC1Ev(45819336)
KLEE: WARNING ONCE: calling external: __cxa_atexit(45904000, 0, 45819352)
KLEE: WARNING ONCE: calling external: __cxa_rethrow()
terminate called without an active exception
0  klee            0x0000000000d61eff
1  klee            0x0000000000d6241c
2  libpthread.so.0 0x00007f3c150db3d0
3  libc.so.6       0x00007f3c13bf9418 gsignal + 56
4  libc.so.6       0x00007f3c13bfb01a abort + 362
5  libstdc++.so.6  0x00007f3c1453b84d
__gnu_cxx::__verbose_terminate_handler() + 365
6  libstdc++.so.6  0x00007f3c145396b6
7  libstdc++.so.6  0x00007f3c14539701
8  libstdc++.so.6  0x00007f3c14539969 __cxa_rethrow + 73
9  libstdc++.so.6  0x00007f3c1545c10d __cxa_rethrow + 15869933
Aborted (core dumped)


Thank you!
-- 
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