[klee-dev] Explanation about seeding mode

[Thuan Pham]

Hello,
Could someone please explain to me the overview of seeding mode in Klee.
For example, how it work in the Executor::branch method.
I want to get the path constraints while executing the program under test
using concrete input(s) and I found a relevant discussion at
http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01429.html. I can
follow the discussion to run program, get symbolic formula... but I don't
understand deeply how it work.
Thanks,
Thuan.
-------------- next part --------------
HTML attachment scrubbed and removed