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

Reply via email to