Hi Chengyu, > On 18 Nov 2016, at 15:16, Chengyu Zhang <dale.chengyu.zh...@gmail.com> wrote: > > 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? >
Well, the current implementation is quite costly, therefore the high value of 30s. This might be less of a problem with older machines but becomes more problematic with newer ones, as they number of instructions per second might be much higher. So you update less often and might work more often with outdated information. So you should vary that number according to your needs. (Of course, patches, which improve that situation are always welcome ;) ) Cheers, Martin > 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 --------------------------------------------------- Martin Nowack Research Assistant Technische Universität Dresden Computer Science Institute of Systems Architecture Systems Engineering 01062 Dresden Phone: +49 351 463 39608 Email: martin_now...@tu-dresden.de ---------------------------------------------------- _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
