Skip to content

Commit

Permalink
Merge pull request #1295 from goblint/sv-comp-cleanup
Browse files Browse the repository at this point in the history
Clean up SV-COMP directory
  • Loading branch information
sim642 authored Dec 20, 2023
2 parents 3015607 + cbece4f commit ea1bf23
Show file tree
Hide file tree
Showing 29 changed files with 39 additions and 668 deletions.
6 changes: 3 additions & 3 deletions docs/developer-guide/releasing.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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>.

Expand Down
17 changes: 17 additions & 0 deletions docs/user-guide/inspecting.md
Original file line number Diff line number Diff line change
Expand Up @@ -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>.
17 changes: 17 additions & 0 deletions docs/user-guide/running.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
4 changes: 2 additions & 2 deletions sv-comp/archive.sh → scripts/sv-comp/archive.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
28 changes: 0 additions & 28 deletions sv-comp/README.md

This file was deleted.

1 change: 0 additions & 1 deletion sv-comp/my-bench-sv-comp/.gitignore

This file was deleted.

46 changes: 0 additions & 46 deletions sv-comp/my-bench-sv-comp/README.md

This file was deleted.

25 changes: 0 additions & 25 deletions sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml

This file was deleted.

30 changes: 0 additions & 30 deletions sv-comp/my-bench-sv-comp/cpa-validate-violation.xml

This file was deleted.

26 changes: 0 additions & 26 deletions sv-comp/my-bench-sv-comp/goblint-all-fast.sh

This file was deleted.

74 changes: 0 additions & 74 deletions sv-comp/my-bench-sv-comp/goblint-all-fast.xml

This file was deleted.

26 changes: 0 additions & 26 deletions sv-comp/my-bench-sv-comp/goblint-data-race.sh

This file was deleted.

17 changes: 0 additions & 17 deletions sv-comp/my-bench-sv-comp/goblint-data-race.xml

This file was deleted.

Loading

0 comments on commit ea1bf23

Please sign in to comment.