[klee-dev] Question about KLEE

[miao Tian]

Dear Sir,

I have a question about the symbolic execution result in KLEE. I already
know that we can obtain test cases through KLEE. But now I only want to get
the result of symbolic execution, and I don’t need to solve it to get test
cases. For example, the example in the figure below: I just need to get the
result of x->Y, y->X when X>Y, and  x->X, y->Y when X<=Y. So I want to know
whether users can complete the simplification and normalization of symbolic
execution through KLEE and get the corresponding results. Or can I call
some low-level functions of KLEE to get some symbolic execution results. If
I can, how can I do it?

[image: image.png]

Thank you!

Best regards,

Miao Tian
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 300780 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20201215/37b806bc/attachment.png>