-
Notifications
You must be signed in to change notification settings - Fork 41
SVComp
Ultimate allows the user to run benchmarks provided by the Software Verification Competition (SVComp). This page will explain how to check out the benchmarks from their official repository (https://github.com/sosy-lab/sv-benchmarks) and how to use Ultimate to verify the benchmarks.
In the official SVComp benchmark repository, there are different sets of benchmarks that can be used for different purposes. This guide only focuses on the benchmarks written in C.
-
Create a directory for the benchmarks
cd /some/toplevel/directory mkdir svcomp
-
Create a fresh git repository
cd svcomp git init
-
Add the remote from where to pull later
git remote add origin https://github.com/sosy-lab/sv-benchmarks
-
In order to conserve space on the hard disk, only the c/ directory is going to be checked out. Therefore, it is necessary to tell git to perform a sparse checkout later
git config --local core.sparsecheckout true echo c/ >> .git/info/sparse-checkout
-
Pull the repository without the history
git pull origin master --depth=1
After that, the repository should be pulled, while only the c/ directory is being checked out. The space that is being used up should be somewhere around 5 GB.
In order for Ultimate's test suites to run correctly, the svcomp benchmarks need to be located in /trunk/examples/svcomp. You can accomplish this by adding a symlink:
ln -s /some/toplevel/directory/svcomp/c /path/to/ultimate/repository/trunk/examples/svcomp
In case you need to change the sparse-checkout file for some reason, you need to issue the following command after the change in order for git to still work with the sparse checkout:
cd /some/toplevel/directory/svcomp
git read-tree -mu HEAD
If you are using windows, this guide is the same for all the git-related commands. The commands themselves can be issued from a command prompt (cmd.exe
).
To create the link of the SVComp directory to the examples directory of Ultimate, use the following command from an Administrator command prompt (Click Start, enter "cmd" right click on the appearing command, select "Run as Administrator"):
mklink /D Drive:\path\to\ultimate\repository\trunk\examples\svcomp Drive:\some\toplevel\directory\svcomp\c
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics