[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

2016-11-02 Thread Chengyu Zhang
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

[klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path

2016-11-02 Thread s.darabi
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