Thanks Daniel and David. A further question. According to the David's warning, the BCov(%) provided by the klee-stats is a low-level measure on the number of the branches in the byte-code, e.g. short circuiting operators, and not a measure at statement level, which is impossible to be extracted (at the moment).
Am I correct? G. > -----Original Message----- > From: daniel.dunbar at gmail.com [mailto:daniel.dunbar at gmail.com] On > Behalf Of Daniel Dunbar > Sent: Tuesday, November 02, 2010 12:43 AM > To: Giuseppe Di Guglielmo > Cc: klee-dev at keeda.stanford.edu > Subject: Re: [klee-dev] Maximizing Branch Coverage (not path coverage) > > 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 > > > >
