[klee-dev] Option for generating MC/DC test cases

[David B Lightstone]

Damir

 

The choice to use CIL was motivated by a bit more than just achieving MC/DC coverage

Equivalence class testing based upon a more or less randomly selected member of the equivalence class is really not adequate.

What one really wants is the boundaries of the equivalence class and the successor or predecessor (as appropriate).

That gives you test cases which allow the appropriateness of the equivalence relationship to be evaluated.

 

Achieving that is a candidate for a program transformation type strategy, with new conditional expressions being added as appropriate to select out a test case having as appropriate the successor or predecessor value.

Because CIL simplifies the logic significantly, I figured that it would be easier to carry out the transformation on the CIL output than to try it against the original source.

 

The analysis boils down to identifying the appropriate number of equality conditionals to added (based on the conditional operator of the expression being evaluated), determining the successor or predecessor value to be used in the equality, determining the goto location when the equality is met.

 

Not really knowing compilers I figured a small perl or python program would be sufficient. If significant knowledge about compilers is needed than a transformation tool such as Rose would be appropriate 

 

Dave

 

 

From: Damir [mailto:lost404 at gmail.com] 
Sent: Monday, May 16, 2016 3:52 PM
To: David Lightstone
Cc: klee-dev
Subject: Re: [klee-dev] Option for generating MC/DC test cases

 

Hello again!

 

I've patched klee to support the option to skip CFGSimplification pass.

 

Here's the link for the patch:

 

https://github.com/ShayDamir/klee/commit/83e5b6d8686a831060fcc34016184e7b18d1d1ba

 

It's a part of my larger effort to build klee with cmake and llvm-3.8, based on the work of Richard Trembecky and my own.

 

So far I've been able to build klee with llvm and cmake on Ubuntu 16.04, with only minor patch to LLVM cmake files.

 

The cmake support is work in progress, lots of things to do. 

 

The -no-boolean-simplification patch is usable on klee with llvm-3.4  and autotools. Official docker image can be patched with it and you can get better coverage for complex decisions.

 

I'm sure it will work on llvm-2.9 too, so you won't need CIL anymore to get better coverage.

-------------- next part --------------
HTML attachment scrubbed and removed