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/[email protected]/msg01429.html. I can follow the discussion to run program, get symbolic formula... but I don't understand deeply how it work. Thanks, Thuan.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
