> There are rewrite rules which serve to transform say a Boolean assignment statement based on several conditional clauses, into say a collection of if-then-else statements ( sequential and/or nested as appropriate), each containing a Boolean assignment.
FYI, below is one of our recent papers on doing code transformation (rewriting) to enable a symbolic execution tool such as Pex ( http://research.microsoft.com/en-us/projects/pex/) to achieve boundary value coverage and MC/DC via path exploration: Rahul Pandita, Tao Xie, Nikolai Tillmann, and Jonathan de Halleux. Guided Test Generation for Coverage Criteria. In Proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM 2010<http://icsm2010.upt.ro/>), Timi?oara, Romania, September 2010. Download: [PDF<http://people.engr.ncsu.edu/txie/publications/icsm10-coverage.pdf> ][BibTeX <http://people.engr.ncsu.edu/txie/pubbib.html#icsm10-cov>] Best wishes, Tao ~~~~~~ Tao Xie, Associate Professor North Carolina State University Computer Science Department Raleigh, NC 27695-8206 Email: xie at csc.ncsu.edu http://www.csc.ncsu.edu/faculty/xie/ On Tue, Nov 2, 2010 at 8:51 AM, David Lightstone < david.lightstone at prodigy.net> wrote: > Dear Giuseppe Di Guglielmo > > I was attempting to address a different issue. > > The various metrics (path coverage, branch coverage, statement coverage, > etc) each in some sense of the word serve to evaluate the quality of the > testing performed by the test cases. > There are rewrite rules which serve to transform say a Boolean assignment > statement based on several conditional clauses, into say a collection of > if-then-else statements ( sequential and/or nested as appropriate), each > containing a Boolean assignment. It would be most amusing to discover that > the number of test cases needed is not an invariant of the transformation. > ( > ie x needed before the transformation x + y needed after.) > You could as a consequence play management result cooking games as a > consequence. (ie rewrite the code so as to produce a minimal testing > effort, > according to the coverage metric) > > I interpreted the CAST paper to be an attempt to clarify the metrics in > such > a way to as to make such games unacceptable, and was suggesting caution is > need when evaluating test effort quality > > I would be inclined to agree with your interpretation, but as I have not > looked into the mechanisms used to generate the test cases, the opinion > which I hold is an uninformed opinion > > Dave Lightstone > > > > -----Original Message----- > > 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 8:42 PM > > To: klee-dev at keeda.stanford.edu > > Subject: Re: [klee-dev] Maximizing Branch Coverage (not path coverage) > > > > 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 > > > > > > > > > > > > _______________________________________________ > > klee-dev mailing list > > klee-dev at keeda.stanford.edu > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20101102/bf629a00/attachment-0001.html
