Merge pull request #1295 from goblint/sv-comp-cleanup

Clean up SV-COMP directory
goblint · Dec 20, 2023 · ea1bf23 · ea1bf23
2 parents 3015607 + cbece4f
commit ea1bf23
Show file tree

Hide file tree

Showing 29 changed files with 39 additions and 668 deletions.
diff --git 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: <https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image>.
 

diff --git 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 <http://localhost:8080>
+
+## 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: <https://yed.yworks.com/support/manual/properties_mapper.html>.
diff --git 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 (<https://github.com/goblint/bench/issues/7#issuecomment-1011055984>, <https://github.com/goblint/bench/issues/7#issuecomment-1011987188>).
     * 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 → scripts/sv-comp/archive.sh b/sv-comp/archive.sh → 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 → scripts/sv-comp/sv-comp-run-no-overflow.py b/sv-comp/sv-comp-run-no-overflow.py → scripts/sv-comp/sv-comp-run-no-overflow.py
diff --git a/sv-comp/sv-comp-run.py → scripts/sv-comp/sv-comp-run.py b/sv-comp/sv-comp-run.py → scripts/sv-comp/sv-comp-run.py
diff --git a/sv-comp/witness-isomorphism.py → scripts/sv-comp/witness-isomorphism.py b/sv-comp/witness-isomorphism.py → scripts/sv-comp/witness-isomorphism.py
diff --git a/sv-comp/yed-sv-comp.cnfx → scripts/sv-comp/yed-sv-comp.cnfx b/sv-comp/yed-sv-comp.cnfx → scripts/sv-comp/yed-sv-comp.cnfx
diff --git a/sv-comp/README.md b/sv-comp/README.md
diff --git a/sv-comp/my-bench-sv-comp/.gitignore b/sv-comp/my-bench-sv-comp/.gitignore
diff --git a/sv-comp/my-bench-sv-comp/README.md b/sv-comp/my-bench-sv-comp/README.md
diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml b/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml
diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml b/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml
diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.sh b/sv-comp/my-bench-sv-comp/goblint-all-fast.sh
diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.xml b/sv-comp/my-bench-sv-comp/goblint-all-fast.xml
diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.sh b/sv-comp/my-bench-sv-comp/goblint-data-race.sh
diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.xml b/sv-comp/my-bench-sv-comp/goblint-data-race.xml