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

Alberto Barbaro barbaro.alberto at gmail.com
Sun Mar 18 11:50:54 GMT 2018


Hi,
sure i'll prepare something as soon as I have some free time. Would you
prefer a full example or just a comment about updating CMakeList.txt?

Thanks

2018-03-10 10:30 GMT+00:00 Cristian Cadar <c.cadar at imperial.ac.uk>:

> 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