Remove oudated parts of sv-comp/README

Dudeldu · May 13, 2022 · a544002 · a544002
1 parent e60ef1d
commit a544002
Showing 1 changed file with 3 additions and 69 deletions.
diff --git a/sv-comp/README.md b/sv-comp/README.md
@@ -1,83 +1,17 @@
 # Goblint for SV-COMP
-All the SV-COMP configuration is in `conf/svcomp21.json`.
+All the SV-COMP configuration is in `conf/svcomp.json`.
 
 ## Run Goblint in SV-COMP mode
 ### ReachSafety
 ```
-./goblint --conf conf/svcomp21.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/DIR/FILE.i
+./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/svcomp21.json --set ana.specification ../sv-benchmarks/c/properties/no-data-race.prp ../sv-benchmarks/c/DIR/FILE.i
+./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/no-data-race.prp ../sv-benchmarks/c/DIR/FILE.i
 ```
 
-## Run Goblint under BenchExec
-This requires setting up a bunch of XMLs and running a few things in the right places.
-Also all paths must be properly configured.
-
-There's three shell scripts in `sv-comp/benchexec/my-bench-sv-comp` for streamlining this process:
-* `goblint-all-fast.sh` – "quickly" (with 60s timeout) run Goblint on all ReachSafety (or more specifically SoftwareSystems) tasks without witness validation
-* `goblint-data-race.sh` – run Goblint on all NoDataRace tasks
-* `goblint.sh` (probably outdated) – run Goblint on all SoftwareSystems tasks with witness validation using CPAchecker and Ultimate Automizer
-
-They have corresponding XML files for benchexec and table-generator.
-
-
----
-
-
-# Goblint for SV-COMP (old)
-
-## Run Goblint in SV-COMP mode
-Command:
-```
-./goblint --enable ana.sv-comp --enable witness.uncil --enable ana.int.interval ./tests/sv-comp/basic/if_mod_true-unreach-call.c
-```
-
-There's a bunch of very simple files to test with in `./tests/sv-comp/` with the expected results in the filename (old SV-COMP task definition format).
-
-
-## Witness-related Goblint flags
-* `ana.sv-comp`
-
-  Adds SV-COMP `__VERIFIER_*` functions, outputs verdict to stdout and outputs witness to `witness.graphml` in current (Goblint root) directory.
-
-* `witness.path`
-
-  Override witness output filename.
-
-* `witness.uncil`
-
-  Cil transforms `&&` and `||` into `if`s, which causes the witness to contain spurious conditional control edges where the original program didn't. I'm guessing this would mix up things for witness validators.
-
-  This option does some hacks to try to undo that transformation when writing the witness.
-
-* `witness.minimize`
-
-  Minimizes the witness graph by skipping nodes and edges without any useful witness data to make witnesses easier to inspect.
-
-  I don't guarantee this minimization to be correct (it may be too aggressive in some places?) nor useful (it may be not aggressive enough in other places).
-
-* `ana.wp`
-
-  Enables weakest precondition feasibility analysis for SV-COMP violations.
-
-
-## Run Ultimate to verify witness
-From: https://github.com/sosy-lab/sv-witnesses/#validating-a-violation-witness-with-ultimate-automizer.
-
-`PropertyUnreachCall.prp` file:
-```
-CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
-```
-
-Command:
-```
-./Ultimate.py --spec PropertyUnreachCall.prp --architecture 32bit --file ../goblint/tests/sv-comp/basic/if_mod_true-unreach-call.c --validate ../goblint/witness.graphml
-```
-
-
 
 # Inspecting witnesses
 ## yEd