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

[Cristian Cadar]

I would just modify the instructions at 
http://klee.github.io/docs/developers-guide/#adding-a-class, in the same 
style.

Thanks,
Cristian

On 18/03/2018 11:50, Alberto Barbaro wrote:
> 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 
> <mailto: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
>     <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>
>         <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
> 
> 
>     _______________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>     <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
> 
>