[klee-dev] How do Klee forks program states?

Thuan Pham thuanpv at comp.nus.edu.sg
Wed Sep 23 10:21:03 BST 2015


Hi Tarannum,
When I tried to get familiar with KLEE code based, I collected some data
from different sources and write this document:
https://dl.dropboxusercontent.com/u/101841567/UnderstandingKLEE.pdf. It
could be helpful. I wrote the document for my future referencing so I did
not check the writing carefully.
Regards,
Thuan

On Wed, Sep 23, 2015 at 2:55 PM, Martin Nowack <martin_nowack at tu-dresden.de>
wrote:

> Hi,
>
> The magic happens in lib/Core/Executor.cpp in the function Executor::fork()
> https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L703
>
> And specifically (if needed to fork the state in the following statement).
>
> https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L857.
>
> Cheers,
> Martin
>
>
> > On 23 Sep 2015, at 00:48, Zaman, Tarannum <tsza223 at g.uky.edu> wrote:
> >
> > Hi,
> >
> > I want to work with the klee code base. But I am not sure about how Klee
> tracks the program states.
> >
> > If anyone can tell me the path in the code of klee with which klee forks
> program states than, it will be very much helpful for me.
> >
> > Thanks
> > Tarannum
> > _______________________________________________
> > 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
> ----------------------------------------------------
>
>
> _______________________________________________
> 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