Move SV-COMP README to documentation

goblint · Dec 15, 2023 · b984383 · b984383
1 parent 88d4d32
commit b984383
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 28 deletions.
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/README.md b/sv-comp/README.md