Skip to content

SVComp

Jump to bottom
Marius Greitschus edited this page Jun 2, 2016 · 6 revisions

Run SVComp Benchmarks

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.

Checking out the Repository and Creating the Necessary Links

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.

  1. Create a directory for the benchmarks 
    

    2. 



cd /some/toplevel/directory
mkdir svcomp



2. Create a fresh git repository
   ```bash
cd svcomp
git init



    

  1. Add the remote from where to pull later

    

    2. 



git remote add origin https://github.com/sosy-lab/sv-benchmarks



4. 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
   ```bash
git config --local core.sparsecheckout true
echo c/ >> .git/info/sparse-checkout



    

  1. Pull the repository without the history

    

    2. 



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:
```bash
ln -s /some/toplevel/directory/svcomp/c /path/to/ultimate/repository/trunk/examples/svcomp



Useful git commands


Change of the sparse-checkout File


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


Windows


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


              


              

                

                  

                    
                  

                

              

          



  
          

            

              

                

                  

                    

                  

                

              


            
Clone this wiki locally