[klee-dev] How to add a new class to KLEE?

Alberto Barbaro barbaro.alberto at gmail.com
Sun Mar 18 20:44:36 GMT 2018


Ok thanks, I'll do it ASAP.

Thanks again

On Sat, Mar 10, 2018, 10:30 Cristian Cadar <c.cadar at imperial.ac.uk> wrote:

> We would welcome updates and improvements to the documentation.  Just
> open a pull request at https://github.com/klee/klee.github.io
>
> Best,
> Cristian
>
> On 10/03/2018 07:08, Alberto Barbaro wrote:
> > Hi,
> > sorry for the email... I fix it adding the file to the CMakeList.txt, I
> > would suggest to update the documentation on the website as well. I
> > think it would be useful to everybody.
> >
> > Thanks
> >
> > 2018-03-10 6:17 GMT+00:00 Alberto Barbaro <barbaro.alberto at gmail.com
> > <mailto:barbaro.alberto at gmail.com>>:
> >
> >     Hi all,
> >     I would like to add a new class to KLEE but I have few problems. I
> >     tried to follow the help that is present on the website but not luck
> >     so far.
> >
> >     In my case, I have created TestObject,h and TestObject.cpp in
> >     lib/Core and included TestObject.h in lib/Core/Executor.cpp using
> >     #include "TestObject.h" and finally added into the function
> >     executeInstruction the line TestObject t;
> >
> >     The code for the class in pretty standard:
> >
> >     TestObject.h
> >     #ifndef TESTOBJECT_H
> >     #define TESTOBJECT_H
> >
> >     namespace klee
> >     {
> >
> >     class TestObject
> >     {
> >     public:
> >          TestObject();
> >          ~TestObject();
> >
> >     };
> >
> >     }
> >
> >     #endif // TESTOBJECT_H
> >
> >     TestObject.cpp
> >     #include "TestObject.h"
> >
> >     klee::TestObject::TestObject()
> >     {
> >     }
> >
> >     klee::TestObject::~TestObject()
> >     {
> >     }
> >
> >     The error I got is:
> >     [ 98%] Built target kleeModule
> >     Linking CXX executable ../../bin/klee
> >     ../../lib/libkleeCore.a(Executor.cpp.o): In function
> >     `klee::Executor::executeInstruction(klee::ExecutionState&,
> >     klee::KInstruction*)':
> >     /home/klee/klee-taint/lib/Core/Executor.cpp:1447: undefined
> >     reference to `klee::TestObject::TestObject()'
> >     /home/klee/klee-taint/lib/Core/Executor.cpp:2459: undefined
> >     reference to `klee::TestObject::~TestObject()'
> >
> >     What am I missing? I cannot understand the problem in this case.
> >
> >     Thanks a lot,
> >     A
> >
> >
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list