This repository contains a snapshot of the Defects4J source code repository for bug number 01 of the Google Closure compiler. In turns, the Defect4J repository contains a snapshot of the Google Closure compiler source code repository. The only code we added to this third-party software is contained in the sushi-src/ folder.
This repository contains an Eclipse project that is configured to work together with the Eclipse projects for SUSHI. Import in an empty Eclipse workspace the projects in the SUSHI repository, by following the instructions in the README file in it. Then, import this repository in the same workspace: On the Eclipse main menu select File > Import..., in the dialog that pops up select Projects from Git, insert the URI of this repository, and when asked for a wizard for importing projects answer Import Existing Eclipse Projects.
Before launching the experiments you must set a few configuration variables to reflect the paths where you installed the code. Under the sushi-src source folder you find the class settings.Settings. Open it and edit the definitions of the GIT_REPO_ROOT, and Z3_PATH variables to reflect the paths on your system where the Git repositories and the binary of the Z3 SMT solver are installed.
The project contains Eclipse launch configurations that can be used to launch the experiments. The launch configurations are the files sushi-src/Sushi_Closure01_accurate.launch (with accurate invariants) and sushi-src/Sushi_Closure01_partial.launch (with partial invariants).
All the temporary files generated by SUSHI will reside in a subdirectory of the sushi-out/ folder that will have as name the date and time when SUSHI was launched. The generated tests will be put in the sushi-test/ source folder (note that multiple runs of SUSHI might overwrite the tests generated by previous runs).