On Mon, Nov 1, 2010 at 8:08 AM, Giuseppe Di Guglielmo <giuseppe.diguglielmo at gmail.com> wrote: > Dear David, > thanks for the paper and suggestions. > But I am insisting, is there the possibility to measure just the branch > coverage with KLEE?
We can (and do) measure it, but just optimizing for any kind of coverage is a very hard problem. We don't do anything sophisticated enough to benefit from the distinction. The main problem is that optimizing for branch coverage will still require you to optimize many paths for full coverage, in order to have enough coverage of the early parts of the program to get full branch coverage of the later parts of the program. - Daniel > G. > 2010/11/1 David Lightstone <david.lightstone at prodigy.net> >> >> Why on earth would you want just branch coverage? >> >> >> >> As a programming language C has short circuiting logic operators. >> Implicitly when you use them in the condition of a conditional expression, >> you are going to get branching in addition to the branching associated with >> the conditional statement. Best to think of things as nested conditional >> statements achieved by the language syntax. As a consequence you may get >> statement level branch coverage, but you may just never execute the entire >> code. >> >> >> >> The FAA has a CAST paper (CAST 10) titled ?What is a ?Decision? in >> Application of Modified Condition/Decision Coverage (MC/DC) and >> Decision?Coverage (DC)?? >> >> It is intended to address the interaction between the concept of branch >> coverage and the actual branching which occurs complements of the compilier. >> >> >> >> Dave Lightstone >> >> >> >> >> >> From: klee-dev-bounces at keeda.stanford.edu >> [mailto:klee-dev-bounces at keeda.stanford.edu] On Behalf Of Giuseppe Di >> Guglielmo >> Sent: Monday, November 01, 2010 6:11 AM >> To: klee-dev at keeda.stanford.edu >> Subject: [klee-dev] Maximizing Branch Coverage (not path coverage) >> >> >> >> Hi, >> >> is there a way to run the KLEE for maximizing the branch coverage rather >> than >> >> exhaustively enumerating all the possible paths? >> >> >> >> For example, consider the code: >> >> >> >> if (cond1) { >> >> ? // A >> >> } else { >> >> ? // B >> >> } >> >> if (cond2) { >> >> ? // C >> >> } else { >> >> ? // D >> >> } >> >> >> >> there are 4 paths >> >> 1.? A; C; >> >> 2.? A; D; >> >> 3.? B; C; >> >> 4.? B; D; >> >> >> >> but satisfying the two conditions >> >> 1.? ( conv1) && ( conv2 ) >> >> 2.? ( !conv1 ) && ( !conv2 ) >> >> is enough to guarantee 100%-branch coverage. >> >> >> >> Does KLEE support such an approach? >> >> >> >> Thanks, >> >> G. >> >> > > > -- > Se non ci fosse l'ultimo momento non si riuscirebbe a fare niente. > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
