From b98438306a97e0a7431130d9bf1985fab526a266 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 15 Dec 2023 12:17:46 +0200
Subject: [PATCH] Move SV-COMP README to documentation

---
 docs/user-guide/inspecting.md | 17 +++++++++++++++++
 docs/user-guide/running.md    | 17 +++++++++++++++++
 sv-comp/README.md             | 28 ----------------------------
 3 files changed, 34 insertions(+), 28 deletions(-)
 delete mode 100644 sv-comp/README.md

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 <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
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 (<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
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.