[klee-dev] KLEE running C++ error

[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

On 19 May 2014, at 01:13, 이원준 <net_abc at nate.com> wrote:

> 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
> {
> private:
> int position;
> int fuel;
> 
> public:
> 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
> klee-dev at imperial.ac.uk
> 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: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140521/db2ddd31/attachment.sig>