Hi, On 04/05/2019 06:31, Kihong Heo wrote: > Hi list, > > I am very new to KLEE and have some questions. > I would appreciate if you could answer the followings: > > - Is there a way to read/write intermediate symbolic states of KLEE to files? > If not, would it be simple to implement? I would appreciate if you could > point out some files to be changed. There is currently no such mechanism per se (although we have some ongoing work in the area), but you could generate a test case and then replay it using the seeding functionality.
> - If a value is not defined externally and not observed by KLEE, how does > KLEE handle it? It has the same mechanism as the UC-KLEE paper? (lazy > constraint) Mainline KLEE does not have the lazy initialization mechanisms of UC-KLEE. Best, Cristian > Thanks, > Kihong > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev