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

[Cristian Cadar]

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
>