On 23 September 2016 at 23:43, Reza Ahmadi <re.ah...@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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
