diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md index fcf69ea533..d875c0d3bf 100644 --- a/docs/developer-guide/releasing.md +++ b/docs/developer-guide/releasing.md @@ -70,7 +70,7 @@ This is required such that the created archive would have everything in a single directory called `goblint`. -4. Update SV-COMP year in `sv-comp/archive.sh`. +4. Update SV-COMP year in `scripts/sv-comp/archive.sh`. This includes: git tag name, git tag message and zipped conf file. @@ -83,9 +83,9 @@ 2. Make sure you have nothing valuable that would be deleted by `make clean`. 3. Delete git tag from previous prerun: `git tag -d svcompXY`. -4. Create archive: `./sv-comp/archive.sh`. +4. Create archive: `./scripts/sv-comp/archive.sh`. - The resulting archive is `sv-comp/goblint.zip`. + The resulting archive is `scripts/sv-comp/goblint.zip`. 5. Check unextracted archive in latest SV-COMP container image: . diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md index f4f6036f1b..266a4866c6 100644 --- a/docs/user-guide/inspecting.md +++ b/docs/user-guide/inspecting.md @@ -23,3 +23,20 @@ To build GobView (also for development): `./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"` 4. Visit + +## Witnesses + +### GraphML + +#### yEd + +1. Open (Ctrl+o) `witness.graphml` from Goblint root directory. +2. Click menu "Edit" → "Properties Mapper". + 1. _First time:_ Click button "Imports additional configurations" and open `scripts/sv-comp/yed-sv-comp.cnfx`. + 2. Select "SV-COMP (Node)" and click "Apply". + 3. Select "SV-COMP (Edge)" and click "Ok". +3. Click menu "Layout" → "Hierarchial" (Alt+shift+h). + 1. _First time:_ Click tab "Labeling", select "Hierarchic" in "Edge Labeling". + 2. Click "Ok". + +yEd manual for the Properties Mapper: . diff --git a/docs/user-guide/running.md b/docs/user-guide/running.md index 97d2587be8..aac1c21ca6 100644 --- a/docs/user-guide/running.md +++ b/docs/user-guide/running.md @@ -67,3 +67,20 @@ Here is a list of issues and workarounds for different compilation database gene #### bear 1. Bear 2.3.11 from Ubuntu 18.04 produces incomplete database (, ). * Bear 3.0.8 seems fine. + + +## SV-COMP +The most up-to-date SV-COMP configuration is in `conf/svcomp.json`. +There are also per-year configurations (e.g. `conf/svcomp24.json`) which try to reflect that year's submission using current option names. +Due to unconfigurable changes (e.g. bug fixes) these do not _exactly_ behave as that year's submission. +See SV-COMP submissions in GitHub releases for exact submitted versions. + +In SV-COMP Goblint is run as follows: +```console +./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} input.c +``` + +Goblint YAML correctness witness validator is run as: +```console +./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} --set witness.yaml.unassume witness.yml --set witness.yaml.validate witness.yml input.c +``` diff --git a/sv-comp/archive.sh b/scripts/sv-comp/archive.sh similarity index 93% rename from sv-comp/archive.sh rename to scripts/sv-comp/archive.sh index 5d8605dc70..37fa2758d9 100755 --- a/sv-comp/archive.sh +++ b/scripts/sv-comp/archive.sh @@ -23,9 +23,9 @@ wget -O lib/LICENSE.APRON https://raw.githubusercontent.com/antoinemine/apron/ma # done outside to ensure archive contains goblint/ directory cd .. -rm goblint/sv-comp/goblint.zip +rm goblint/scripts/sv-comp/goblint.zip -zip goblint/sv-comp/goblint.zip \ +zip goblint/scripts/sv-comp/goblint.zip \ goblint/goblint \ goblint/lib/libapron.so \ goblint/lib/liboctD.so \ diff --git a/sv-comp/sv-comp-run-no-overflow.py b/scripts/sv-comp/sv-comp-run-no-overflow.py similarity index 100% rename from sv-comp/sv-comp-run-no-overflow.py rename to scripts/sv-comp/sv-comp-run-no-overflow.py diff --git a/sv-comp/sv-comp-run.py b/scripts/sv-comp/sv-comp-run.py similarity index 100% rename from sv-comp/sv-comp-run.py rename to scripts/sv-comp/sv-comp-run.py diff --git a/sv-comp/witness-isomorphism.py b/scripts/sv-comp/witness-isomorphism.py similarity index 100% rename from sv-comp/witness-isomorphism.py rename to scripts/sv-comp/witness-isomorphism.py diff --git a/sv-comp/yed-sv-comp.cnfx b/scripts/sv-comp/yed-sv-comp.cnfx similarity index 100% rename from sv-comp/yed-sv-comp.cnfx rename to scripts/sv-comp/yed-sv-comp.cnfx diff --git a/sv-comp/README.md b/sv-comp/README.md deleted file mode 100644 index 9f5c203213..0000000000 --- a/sv-comp/README.md +++ /dev/null @@ -1,28 +0,0 @@ -# Goblint for SV-COMP -All the SV-COMP configuration is in `conf/svcomp.json`. - -## Run Goblint in SV-COMP mode -### ReachSafety -``` -./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/DIR/FILE.i -``` - -### NoDataRace -``` -./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/no-data-race.prp ../sv-benchmarks/c/DIR/FILE.i -``` - - -# Inspecting witnesses -## yEd - -1. Open (Ctrl+o) `witness.graphml` from Goblint root directory. -2. Click menu "Edit" → "Properties Mapper". - 1. _First time:_ Click button "Imports additional configurations" and open `yed-sv-comp.cnfx` from this directory. - 2. Select "SV-COMP (Node)" and click "Apply". - 3. Select "SV-COMP (Edge)" and click "Ok". -3. Click menu "Layout" → "Hierarchial" (Alt+shift+h). - 1. _First time:_ Click tab "Labeling", select "Hierarchic" in "Edge Labeling". - 2. Click "Ok". - -yEd manual for the Properties Mapper: https://yed.yworks.com/support/manual/properties_mapper.html. diff --git a/sv-comp/my-bench-sv-comp/.gitignore b/sv-comp/my-bench-sv-comp/.gitignore deleted file mode 100644 index 2eb047c8d6..0000000000 --- a/sv-comp/my-bench-sv-comp/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*-tmp.xml diff --git a/sv-comp/my-bench-sv-comp/README.md b/sv-comp/my-bench-sv-comp/README.md deleted file mode 100644 index b401a1898c..0000000000 --- a/sv-comp/my-bench-sv-comp/README.md +++ /dev/null @@ -1,46 +0,0 @@ -# my-bench-sv-comp -This directory contains BenchExec benchmark and table definitions for a number of use cases and shell scripts for running them. - -## goblint-all-fast -Run Goblint on a large number of reachability benchmarks with decreased timeout. - -Files: -* `goblint-all-fast.sh` -* `goblint-all-fast.xml` -* `table-generator-all-fast.xml` - - -## goblint-data-race -Run Goblint on data-race benchmarks. - -Files: -* `goblint-data-race.sh` -* `goblint-data-race.xml` -* `table-generator-data-race.xml` - - -## goblint-lint -Run Goblint and validate witnesses using witnesslinter. - -Files: -* `goblint-lint.sh` -* `goblint-lint.xml` -* `table-generator-lint.xml` -* `witnesslint-validate.xml` - - -## goblint -Run Goblint and validate witnesses using: -* CPAChecker, -* Ultimate Automizer, -* witnesslinter. - -Files: -* `cpa-validate-correctness.xml` -* `cpa-validate-violation.xml` -* `goblint.sh` -* `goblint.xml` -* `table-generator-witness.xml` -* `uautomizer-validate-correctness.xml` -* `uautomizer-validate-violation.xml` -* `witnesslint-validate2.xml` diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml b/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml deleted file mode 100644 index dca5c52c6d..0000000000 --- a/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml +++ /dev/null @@ -1,25 +0,0 @@ - - - - - - **.graphml - - - - - - - RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml - - - - /home/simmo/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /home/simmo/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml b/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml deleted file mode 100644 index 8fcffd7321..0000000000 --- a/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml +++ /dev/null @@ -1,30 +0,0 @@ - - - - - - **.graphml - - - - - - - - - - - - RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml - - - - /home/simmo/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /home/simmo/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.sh b/sv-comp/my-bench-sv-comp/goblint-all-fast.sh deleted file mode 100755 index c47ff10141..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-all-fast.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/70-all-fast-no-interval -GOBLINTPARALLEL=14 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-all-fast.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-all-fast.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.xml b/sv-comp/my-bench-sv-comp/goblint-all-fast.xml deleted file mode 100644 index 6d4bb8fc3c..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-all-fast.xml +++ /dev/null @@ -1,74 +0,0 @@ - - - - - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ConcurrencySafety-Main.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/* - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64Large-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.sh b/sv-comp/my-bench-sv-comp/goblint-data-race.sh deleted file mode 100755 index b42e69d5ce..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-data-race.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/data-race-results21-concurrencysafety-new -GOBLINTPARALLEL=14 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-data-race.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-data-race.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.xml b/sv-comp/my-bench-sv-comp/goblint-data-race.xml deleted file mode 100644 index f8c00b582a..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-data-race.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoDataRace-ConcurrencySafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-lint.sh b/sv-comp/my-bench-sv-comp/goblint-lint.sh deleted file mode 100755 index bbd1270a31..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-lint.sh +++ /dev/null @@ -1,42 +0,0 @@ -#!/bin/bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/new-results28-all-fast-systems-witness-linter -GOBLINTPARALLEL=15 -VALIDATEPARALLEL=15 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-lint.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Construct validation XMLs -cd $MYBENCHDIR -# witnesslint -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" witnesslint-validate.xml > witnesslint-validate-tmp.xml - -# Run validation -# witnesslint -cd /mnt/goblint-svcomp/benchexec/tools/witnesslint -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/witnesslint-validate-tmp.xml - -# Merge witness validation results -cd $RESULTSDIR -python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint*.results.!(*merged*).xml.bz2 witnesslint-validate-tmp.*.results.*.xml.bz2 - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-lint.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip -unzip -o witnesslint-validate-tmp.*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-lint.xml b/sv-comp/my-bench-sv-comp/goblint-lint.xml deleted file mode 100644 index 8cae0a2c69..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-lint.xml +++ /dev/null @@ -1,68 +0,0 @@ - - - - - - **.graphml - - - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint.sh b/sv-comp/my-bench-sv-comp/goblint.sh deleted file mode 100755 index eaf74350de..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint.sh +++ /dev/null @@ -1,63 +0,0 @@ -#!/bin/bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/new-results32-overflow -GOBLINTPARALLEL=15 -VALIDATEPARALLEL=4 # not enough memory for more - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint.*.files` -echo $LOGDIR - -# Construct validation XMLs -cd $MYBENCHDIR -# witnesslint -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" witnesslint-validate2.xml > witnesslint-validate2-tmp.xml -# CPAChecker -# sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" cpa-validate-correctness.xml > cpa-validate-correctness-tmp.xml -# sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" cpa-validate-violation.xml > cpa-validate-violation-tmp.xml -# Ultimate -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" uautomizer-validate-correctness.xml > uautomizer-validate-correctness-tmp.xml -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" uautomizer-validate-violation.xml > uautomizer-validate-violation-tmp.xml - -# Run validation -# witnesslint -cd /mnt/goblint-svcomp/benchexec/tools/witnesslint -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/witnesslint-validate2-tmp.xml -# CPAChecker -# cd /home/simmo/benchexec/tools/CPAchecker-1.9-unix -# benchexec --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/cpa-validate-correctness-tmp.xml -# benchexec --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/cpa-validate-violation-tmp.xml -# Ultimate -cd /mnt/goblint-svcomp/benchexec/tools/UAutomizer-linux -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/uautomizer-validate-correctness-tmp.xml -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/uautomizer-validate-violation-tmp.xml - -# Merge witness validation results -cd $RESULTSDIR -# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.!(*merged*).xml.bz2 cpa-validate-correctness-tmp.*.results.*.xml.bz2 cpa-validate-violation-tmp.*.results.*.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 -# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.!(*merged*).xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 witnesslint-validate2-tmp.*.results.*.xml.bz2 -python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.*no-overflow.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*no-overflow.xml.bz2 uautomizer-validate-violation-tmp.*.results.*no-overflow.xml.bz2 witnesslint-validate2-tmp.*.results.*no-overflow.xml.bz2 - -# Generate table with merged results and witness validation results -# table-generator goblint.*.results.*.xml.bz2.merged.xml.bz2 cpa-validate-correctness-tmp.*.results.*.xml.bz2 cpa-validate-violation-tmp.*.results.*.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-witness.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint.*.logfiles.zip -# unzip -o cpa-validate-correctness-tmp.*.logfiles.zip -# unzip -o cpa-validate-violation-tmp.*.logfiles.zip -unzip -o uautomizer-validate-correctness-tmp.*.logfiles.zip -unzip -o uautomizer-validate-violation-tmp.*.logfiles.zip -unzip -o witnesslint-validate2-tmp.*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint.xml b/sv-comp/my-bench-sv-comp/goblint.xml deleted file mode 100644 index c5773f3569..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint.xml +++ /dev/null @@ -1,38 +0,0 @@ - - - - - - **.graphml - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoOverflows-BitVectors.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoOverflows-Other.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-BusyBox-NoOverflows.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-uthash-NoOverflows.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - - - diff --git a/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml b/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml deleted file mode 100644 index c9b9932390..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-data-race.xml b/sv-comp/my-bench-sv-comp/table-generator-data-race.xml deleted file mode 100644 index 28410d1805..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-data-race.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-lint.xml b/sv-comp/my-bench-sv-comp/table-generator-lint.xml deleted file mode 100644 index 6ca64dc84e..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-lint.xml +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - - - - witness - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-witness.xml b/sv-comp/my-bench-sv-comp/table-generator-witness.xml deleted file mode 100644 index 876c08d392..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-witness.xml +++ /dev/null @@ -1,20 +0,0 @@ - - - - - - - - - witness - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml b/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml deleted file mode 100644 index efb0861775..0000000000 --- a/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml +++ /dev/null @@ -1,33 +0,0 @@ - - - - - **.graphml - - diff --git a/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml b/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml deleted file mode 100644 index fdf61b1bab..0000000000 --- a/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml +++ /dev/null @@ -1,32 +0,0 @@ - - - - - **.graphml - - diff --git a/sv-comp/my-bench-sv-comp/witnesslint-validate.xml b/sv-comp/my-bench-sv-comp/witnesslint-validate.xml deleted file mode 100644 index 96a41ef731..0000000000 --- a/sv-comp/my-bench-sv-comp/witnesslint-validate.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - diff --git a/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml b/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml deleted file mode 100644 index 475bc9846e..0000000000 --- a/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml +++ /dev/null @@ -1,31 +0,0 @@ - - - - -