[klee-dev] Question about KLEE

[Frank Busse]

Hi,


On Tue, 15 Dec 2020 20:17:31 +0800
miao Tian <tianmmcat at gmail.com> wrote:

> 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?

Just in case you're still interested in a solution: could you clarify
what you expect as "symbolic execution result"? Do you want an
assignment, the path constraint, tests at intermediate points, ...?


Kind regards,

Frank