> Yes, its certainly possible to use the istats to get more information. > However, from a purity perspective there is something nice about > getting the data from replayed runs with gcov, since that prevents > bugs in KLEE from skewing any results. My zcov tool could easily be > adapted to support loading information that KLEE spit out directly > (http://minormatter.com/zcov).
I agree, however, computing other metrics besides line coverage might be useful. I will probably take a look soon at how zcov could be used to interpret the information spit by KLEE. > I personally use the run stats information as a runtime monitor, in > conjunction with some emacs foo which just runs a command periodically > in a separate frame. I just leave it there running klee-stats on a > directory which is useful for watching the summary. > > If you want more detailed information, it should be easy enough to > collect it. A simple approach would be to just check point the istats > files every once in a while. A more sophisticated approach could use > the TreeStreamer ADT to monitor all the coverage data, even > partitioned by state. I have used the TreeStreamer path information to > generate some movies of the state space exploration over time. For > example: > http://minormatter.com/movie_1.avi This looks very nice. Do you have more details about the code that did the drawing of the tree for this movie? I did not find the code in the KLEE repository. > The nice thing about the TreeStreamer approach is it is relatively > efficient at capturing boatloads of information, if you really want to > do a comprehensive analysis later. This could be useful both for debugging and for monitoring various coverage metrics over time, once a KLEE run ends. Thanks, Cristi
