Hi,
On Tue, 15 Dec 2020 20:17:31 +0800 miao Tian <[email protected]> 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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
