On Tue, Mar 9, 2010 at 2:46 PM, Cristian Zamfir <cristian.zamfir at epfl.ch> wrote: > >> 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.
Yeah, it never made it into the repo. If you are interested, I can dig up the source code on my home machine. - Daniel >> 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 > >
