KLEE running C++ error

[이원준]

Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit

[Martin Nowack]

Hi,

The problem is that the following function is not linked (marked as external) and can not be called: _ZNSolsEPFRSoS_E.

You can demangle the name here: http://demangler.com/
Which leads to the following:
std::ostream::operator<<(std::ostream& (*)(std::ostream&))

So, it’s a typical problem with not linking libstdc++.

Cheers,
Martin

I trying to running c++ but error occurrenced
this error JPG
http://puu.sh/8ROTH
Im using ubuntu 13.03 and 64bit
// and my source , llvm-g++ compile is well done
#include <iostream>
#include <klee/klee.h>
using namespace std;
class Car
{
int position;
int fuel;
Car()
{
position=0;
fuel=10;
}
int forward()
{
position++;
fuel--;
return check();
}
int backward()
{
int result;
position--;
fuel--;
return check();
}
void charge()
{
fuel+=5;
if(fuel>10)fuel=10;
}
int check()
{
if(fuel<0)
return -1;
if(position==7)
return 1;
else
return 0;
}
};
int main()
{
Car car;
char path[24];
klee_make_symbolic(path, 24, "path");
//cin>>path;
int success=0, i, result;
for(i=0;path[i]!='ï¿Š0';i++)
{
if(path[i]=='f')
{
result=car.forward();
if(result==1)
{
success=1;
break;
}
else if(result==-1)
{
return -1;
}
}
else if(path[i]=='b')
{
result=car.backward();
if(result==1)
{
success=1;
break;
}
else if(result==-1)
{
return -1;
}
}
else if(path[i]=='c')
{
car.charge();
}
}
if(success)
{
cout<<"Success!"<<endl<<"Answer: "<<path<<endl;
return 1;
}
cout<<"Failed..."<<endl;
return 0;
}
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische UniversitÀt Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: [phone]
Email: martin_nowack-***@public.gmane.org
----------------------------------------------------