Download

Please note that all software is provided "as is".

Dynamic-Static-Dynamic Analysis (DSD-Crasher)

This is the current version of CnC. The older version from ICSE 2005 is still available below.

Test case generator and runtime

cnc-0.8.6.jar contains sources and executables.
See below under CnC Classic for how to get and set up Simplify.
See the included changes.txt for details about changes and improvements.

Example: How to use CnC and DSD-Crasher

The following is an example setup:

c:\lib\cnc-0.8.6.jar
C:\cs\jcrasher\subjects\cnc-mini-subjects
- build.xml Ant project build script, defines the configuration of the project and the CnC components
- testees.txt defines the classes under test
- inferee.txt defines the test-case used to infer invariants of the tested classes
- src contains the project's source code
  - demo\Testee.java is the tested class
  - demo\Execution.java is the test-case used to infer invariants of demo.Testee
- cnc-bin will be created by by the build.xml script and will contain compiled project classes
- cnc-test-src will be created by by the build.xml script and contain CnC-generated test sources
- cnc-test-bin will be created by by the build.xml script and contain CnC-generated test class binaries
- cnc-mini-subjects-cnc-0.8.6-2005-10-30-2328-demo-daikon-cnc.zip will contain CnC's results in an archive named DirectoryName-cnc-CnCversion-date-time.zip: Daikon-annotated source of tested class, CnC-generated test cases, configuration files, and output of Daikon, ESC, and JUnit.

You can still run CnC without Daikon. To run CnC alone you have to comment out the Daikon configuration parameters in the build.xml file. (They are all in one block that starts with .) Running CnC alone produces two warnings: cnc-mini-subjects-cnc-0.8.6-2005-10-30-2330-demo-cnc-only.zip.

You might consider one of the two warnings produced by CnC alone a false positive though because it violates a precondition that the testee contains as an informal comment. The goal of combining CnC with Daikon is to suppress such false positive warnings. In our example we have a test case (Execution.java) that exercises the testee as intended by the specification. CnC uses Daikon to infer this implicit precondition from the test execution and annotates the testee's source file with JML annotations. Running CnC with Daikon (the default setting of build.xml) CnC suppresses this false positive warning.

Example: Using CnC on a Medium-Size Third-Party Application

We have used the different configurations of CnC on Groovy version 1 beta 1, which is available at: http://groovy.codehaus.org/. We have used CnC 0.8.6 with the following configuration files:

We have also experimented with Eclat using our own build script eclat.xml.

CnC Classic: ICSE 2005

CnC test case generator and runtime

cnc-bundle-0.4.10.jar contains sources and executables.
Requires
- The Simplify theorem prover version for your platform ( Simplify-1.5.4.exe for Windows, Simplify-1.5.4.linux, Simplify-1.5.4.macosx, Simplify-1.5.4.solaris, or Simplify-1.5.4.tru64). Alternatively you can get Simplify also as part of ESC/Java2 or ESC/Java.
- Windows user need to additionally install Cygwin.

Setting up Simplify

Add the directory that contains the Simplify executable to your PATH environment variable, e.g. c:\bin\simplify-1.5.4 on my Windows machine.
Set your PROVER_CC_LIMIT environment variable to 10, which specifies the maximum number of counterexamples Simplify searches for in the same method.

Using CnC

A user project using CnC will integrate the following computation steps into its build process.

Execute CnC on selected testee sources and binaries.
Compile the test cases CnC generated.
Execute JUnit on the generated test cases.
Archive the test results.

Using CnC without Ant

The following assumes that you have installed Java version 1.4.x (Java versions < 1.4 and Java versions >= 1.5 cause problems with the current version of CnC).

Compile your testees like
javac BSTNode.java
Make sure that the cnc-bundle jar file and the testee class files are reachable via your classpath.
Run the CnC test case generator, pass it the testee source file names.
java edu.gatech.cc.cnc.Main -ea -source 1.4 -simplify Simplify-1.5.4.exe -classpath c:\bin\j2sdk1.4.2_05\jre\lib\rt.jar;. BSTNode.java
- Replace Simplify-1.5.4.exe with the Simplify executable name (not path) for your platform.
- Replace c:\bin\j2sdk1.4.2_05\jre\lib\rt.jar;. with your classpath appended to the location of the Java runtime jar file on your machine.
CnC puts each generated test class source file in the same folder as its testee. So now we should have BSTNodeTest.java and at least BSTNodeTest1.java. CnC prints ESC's output, which contains three warnings.
Compile the testfiles like
javac BSTNodeTest.java
Run the generated sources via our modified JUnit like
java edu.gatech.cc.junit.textui.RaGTestRunner -noreinit BSTNodeTest
You should get a report pointing to two class cast exceptions.

You have the following options.

CnC test case generator
- -NPE as a first argument turns CnC's search for null dereference (NullPointerException) on.
- Use any ESC/Java2 options like the following.
  - -counterexample emits Simplify's counterexamples, specifying the conditions under wich the problems being warned of can occur.
  - -ea enables Java's assert statements.
  - -source 1.4 interprets testees as Java 1.4 source files.
  - -loop 3.5 increases the number of loop unrollings from the default 1.5 to 3.5, for example.
CnC runtime
- -noreinit turns class reinitialialization off.

Using CnC with Ant

Our goal is to ease the integration of CnC into a user project's build process. The idea is to separate the general steps of using CnC from the specifics of the user project's build process.

Ant is a popular open source tool to automate the build process of Java projects. Ant takes an XML formatted text file as input, which is also called the build file. An Ant build file is similar to a make file: it declares build targets and their dependencies. Ant interprets a build file and solves its dependencies to execute the build targets in a correct order.

The CnC distribution contains a generic Ant build file use.xml that invokes the CnC computation steps. A user project's build file build.xml then only needs to compile the testees (given by testees.txt) and call CnC's use.xml, passing project specific parameters to use.xml. The following code fragments illustrate the idea.


<!-- build.xml -->
<project name="MyProject" [..]>
  <!-- project properties -->
  <!-- environment properties -->
  <!-- compile -->
  <!-- test by calling use.xml -->
</project>


<!-- use.xml -->
<project name="CnC" [..]>
  <!-- test.generate -->
  <!-- test.compile -->
  <!-- test.run -->
  <!-- test.archive -->
</project>

Some user projects might need to adapt use.xml to integrate the execution of CnC generated test cases with other testing activities or to adapt the archival of test results to the user project requirements.