[klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path
Dear Klee developers,
I am trying to use Klee for specification generation. To do that I need Klee's
intermediate symbolic results. Specifically, I need the guards of each path in
the program to be printed in their symbolic forms. For example, in the
following program:
get_sign(int a,char * sign)
{
if (a==0) *sign = 0;
else if (a<0) *sign = -1;
else *sign = 1;
}
I want,
Path1 : (a==0)
Path2 : (a<0)
Path3: (a>0)
as output and if it is possible to have the value of sign or the range of sign
value for each path.
Path1: (a==0)==> *sign = 0;
Path2: (a<0)==> *sign = -1;
Path3: (a>0)==> *sign = 1;
Questions:
?Is there any Klee command line option that can activate any symbolic output?
If yes please refer me to its manual page.
If no, can Klee basically be extended to generate such an output?
Thanks in advance,
Saeed Darabi
?
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher
Hi all, I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. In my opinion, md2u is the strategy that when selecting a state KLEE aways consider about the states have the minimum distance to uncovered part of the code. I read the source code of the MinDistToUncovered, but I'm still confused about the implement of computeMinDistToUncovered function. So I have two questions: 1. If someone could give the algorithm description about how to compute the minimum distance to uncovered part in KLEE or explain the implement of computeMinDistToUncovered function in KLEE. And if I could compute the distance between two instructions in KLEE. 2. What's the difference between CovNew and MD2U search heuristic ? Thanks a lot. Chengyu Zhang -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: 18685412181 Mail: dale.chengyu.zh...@gmail.com ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
