[klee-dev] Read/write symbolic state

[Cadar, Cristian]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>