cnc-0.8.6.jarcontains sources and executables.
changes.txtfor details about changes and improvements.
build.xmlAnt project build script, defines the configuration of the project and the CnC components
testees.txtdefines the classes under test
inferee.txtdefines the test-case used to infer invariants of the tested classes
srccontains the project's source code
cnc-binwill be created by by the
build.xmlscript and will contain compiled project classes
cnc-test-srcwill be created by by the
build.xmlscript and contain CnC-generated test sources
cnc-test-binwill be created by by the
build.xmlscript and contain CnC-generated test class binaries
cnc-mini-subjects-cnc-0.8.6-2005-10-30-2328-demo-daikon-cnc.zipwill contain CnC's results in an archive named DirectoryName
.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
<!--Daikon-->.) Running CnC alone produces two warnings:
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.
http://groovy.codehaus.org/. We have used CnC 0.8.6 with the following configuration files:
cnc-bundle-0.4.10.jarcontains sources and executables.
Simplify-1.5.4.tru64). Alternatively you can get Simplify also as part of ESC/Java2 or ESC/Java.
cnc-bundlejar file and the testee class files are reachable via your classpath.
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
Simplify-1.5.4.exewith the Simplify executable name (not path) for your platform.
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.
BSTNodeTest.javaand at least
BSTNodeTest1.java. CnC prints ESC's output, which contains three warnings.
java edu.gatech.cc.junit.textui.RaGTestRunner -noreinit BSTNodeTest
-NPEas a first argument turns CnC's search for null dereference (
-counterexampleemits Simplify's counterexamples, specifying the conditions under wich the problems being warned of can occur.
-eaenables Java's assert statements.
-source 1.4interprets testees as Java 1.4 source files.
-loop 3.5increases the number of loop unrollings from the default 1.5 to 3.5, for example.
-noreinitturns class reinitialialization off.
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>
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.
<!-- use.xml --> <project name="CnC" [..]> <!-- test.generate --> <!-- test.compile --> <!-- test.run --> <!-- test.archive --> </project>