Merge pull request #5 from tautschnig/document-all-steps

Added full SV-COMP benchmarking instructions

Author: peterschrammel

README.md

@@ -6,9 +6,11 @@
 
 #### Build wrapper script
 
+If you you want to build the wrapper script only, use
+
 `make` tool`-wrapper`
 
-where tool is `cbmc` or `2ls`, for instance
+where tool is `cbmc` or `2ls`.
 
 #### Benchexec tool script
 
@@ -23,3 +25,30 @@ where tool is `cbmc` or `2ls`, for instance
 #### License
 
 https://github.com/diffblue/cbmc/blob/master/LICENSE
+
+#### Running experiments in SV-COMP style
+
+```
+git clone --depth=1 https://github.com/sosy-lab/sv-benchmarks
+git clone https://github.com/sosy-lab/benchexec
+cd benchexec
+tar xzf ../2ls-sv-comp-2017.tar.gz
+wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/2ls.xml
+sed -i 's/witness.graphml/${logfile_path_abs}${inputfile_name}-witness.graphml/' 2ls.xml
+bin/benchexec 2ls.xml --tasks <those categories that you want to run>
+wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-correctness-witnesses.xml
+wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-violation-witnesses.xml
+git clone --depth=1 https://github.com/sosy-lab/cpachecker.git
+cd cpachecker
+ant
+cd ..
+ln -s cpachecker/scripts/cpa.sh cpa.sh
+ln -s cpachecker/config/ config
+# manually tweak the requiredfiles and option name=-witness lines in cpa-seq-validate*.xml
+bin/benchexec cpa-seq-validate-correctness-witnesses.xml
+PYTHONPATH=. python3 contrib/mergeBenchmarkSets.py #needs more parameters
+bin/table-generator results/*xml.bz2
+```
+
+Replace 2ls by cbmc to use the above with CBMC.
+