Test Cases Manually Added and Generated by KLEE's Shadow Symbolic Execution
This dataset contains test cases that were manually designed and automatically generated using KLEE's shadow symbolic execution (see Shadow ICSE2016) and employed in the empirical study: An Empirical Study on Mutation, Statement and Branch Coverage Fault Revelation that Avoids the Unreliable Clean Program Assumption (ICSE2017).
These tests were designed to run on the version pre/post bux fixing commit of 68 of the 70 CoreBEnch subjects. Users just need integrate these tests with CoreBEnch, for compilation of
NEW verions (see bellow), and run the tests.
OLD version represents the version pre bug fixing commit
NEW version represents the version post bug fixing commit
These tests use the
NEW version's output as oracle to test
OLD version, therefore requires both
OLD version and
NEW version to be compiled.
Integration with Corebench
Insert the call to the CoreBEnch script for building respectively the version pre bug fix commit (OLD) and post bug fix commit (NEW) into the script
corebenchBuild.sh. The executables generated after compilation will be copied into the directory
build-versions described bellow.
klee-replaycontain the executable of the program klee-replay (version used by shadow version of KLEE) necessary to execute KLEE's generated tests.
subjectscontain 68 directory of the 70 bugs of corebench (except IDs 64 and 65). each directory name represent the corresponding CoreBEnch bug ID. Each subject contain:
testscriptswhich contains the modified version of the tests scripts of the programs.
genktestswhich contains the .ktest files generated by KLEE's Shadow and and based on the tests in testscripts
build-versionswhere the executables are store and used in a wrapper duringtest execution
test-verdict-outputcontains the result of test execution in a file
<bugID>-ktestPassFail.txt(automatically created during test execution). in the file, 0 means test pass and 1 means test fail. Note: the list of test generated and manually added are found in
Run the tests
call the script
run.sh with the
corebench bug ID, the
repo root directory and the keyword
tests in order to execute all the tests. for example, assume that the subject bugID 1 have the repo directory path/to/repo/1. the test execution will be:
./run.sh 1 path/to/repo/1 tests
This command will first copy the tests from
testscripts into the repository, then execute the tests and store the results into
test-verdict-output , and finaly restore the original test of the repo.
By Thierry Titcheu Chekam University of Luxembourg (SnT)
please contact me if you have questions about this.