Hi all, After reading the source code, I have figured out how MD2U strategy works. The main idea of MD2U strategy is : Init every uncovered instruction min-distance-to-uncovered value to 1, every covered instruction min-distance-to-uncovered value to 0; Iterate each instruction, inherit min-distance-to-uncovered value from it's successor, until no more min-distance-to-uncovered value have changed. Then we can get the min-distance-to-uncovered for every instruction.
But I have a question that why KLEE set uncovered-update interval default to 30 ticks rather than every time we do stepInstruction function? Is it because of low efficiency or other reasons? Best regards, Chengyu 2016-11-02 18:00 GMT+08:00 Chengyu Zhang <dale.chengyu.zh...@gmail.com>: > 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 > -- 张枨宇 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