"'klee_make_symbolic' was not declared in this scope" - when analyzing C++ code

[Radu Stoenescu]

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 = "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,

[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

Post by Radu Stoenescu
Hello,
I am currently in the experimentation phase of using Klee and I have
succeed in running klee over a number of C programs.
// Header Files
#include <iostream>
#include <stdio.h>
using namespace std;
// Class Declaration
class person
{
//Access - Specifier
//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;
}
llvm-g++ -B/usr/lib/x86_64-linux-gnu --emit-llvm -c -g
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev