[klee-dev] segmentation fault

[Dan Liew]

On 23 September 2016 at 23:43, Reza Ahmadi <re.ahmdi at gmail.com> wrote:
> 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?

C++ code is not properly supported. Multiple features are missing including

* Support for exceptions
* Support for a symbolic C++ standard library

> 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).

KLEE doesn't support symbolic floating point operations yet. I'm
currently working on a fork of it that does but it isn't ready for
public use yet.

HTH,
Dan.