[klee-dev] "'klee_make_symbolic' was not declared in this scope" - when analyzing C++ code

[Cristian Cadar]

Hi Radu,

Fixing the compilation issue is the easy part: it looks like llvm-g++ 
really wants klee_make_symbolic declared and the correct thing is to add 
"#include <klee/klee.h>" and the corresponding "-I 
<path-to-klee>/include" flag.

However, KLEE has only partial support for C++, and you'll likely run 
into more significant issues, such as unhandled externals and intrinsics.

Cristian

On 17/03/14 09:04, Radu Stoenescu wrote:
> Hello,
>
> I am currently in the experimentation phase of using Klee and I have
> succeed in running klee over a number of C programs.
>
> I have also tried doing so with some C++ code:
>
> // Header Files
> #include <iostream>
> #include <stdio.h>
>
> using namespace std;
>
> // Class Declaration
> class person
> {
>      //Access - Specifier
>      public:
>
>      //Varibale Declaration
>      string name;
>      int number;
>
>      void printName(int x) {
>          if (x > 10)
>              cout << name;
>          else
>              cout << "You have no name";
>      }
> };
>
> //Main Function
> int main()
> {
>      // Object Creation For Class
>      person obj;
>
> obj.name <http://obj.name> = "Foo";
>
>      int a;
>      klee_make_symbolic(&a, sizeof(a), "a");
>      obj.printName(a);
>
>      return 0;
> }
>
> I'm compiling it using:
>
> llvm-g++ -B/usr/lib/x86_64-linux-gnu --emit-llvm -c -g
>
> And I get the following error when invoking klee:
>
> main.cpp:35: error: ‘klee_make_symbolic’ was not declared in this scope
>
> Since I'm not doing the linking phase I thought this shouldn't occur.
>
> Many thanks,
>
> --
> Radu Stoenescu
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>