You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/sas21-artifact-description.md
+7-5Lines changed: 7 additions & 5 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,6 +1,7 @@
1
1
# SAS21 Artifact Description
2
2
3
-
The artifact is a Virtual Box Image based on Ubuntu 20.04.1. The login is goblint:goblint.
3
+
The artifact is a VirtualBox Image based on Ubuntu 20.04.1. The login is `goblint:goblint`.
4
+
4
5
## Validation
5
6
6
7
### Step by Step Instructions
@@ -28,7 +29,7 @@ Navigate to the folder `~/analyzer`. All paths are given relative to it.
28
29
29
30
30
31
### Notes
31
-
* The source code for benchmarks can be found in `./../bench/pthread/` and `./../bench/svcomp/`.
32
+
* The source code for benchmarks can be found in `../bench/pthread/` and `../bench/svcomp/`.
32
33
* Although it takes ~25 min to run all the benchmarks, the script continually updates the results HTML. Therefore it's possible to observe the first results in the partially-filled table without having to wait for the script to finish.
33
34
* If you get messages such as `dune: command not found` run `eval $(opam env)`
34
35
@@ -38,7 +39,8 @@ Navigate to the folder `~/analyzer`. All paths are given relative to it.
38
39
**Goblint is a general framework for Abstract Interpretation and has been used to implement a wide variety of analyses. For extending Goblint with some entirely different analysis,
39
40
one can use `./src/analyses/constants.ml` as a jumping-off point showing how to specify an analysis in the framework.**
40
41
41
-
The following description is about how to more specifically extend one of the analyses presented in the paper at hand.
42
+
The following description is specifically about extending one of the thread-modular analyses presented in the paper at hand.
43
+
42
44
### Implementation of Analyses in the Paper
43
45
The OCaml source code for the core of the analyses is found in `./src/analyses/basePriv.ml`.
44
46
Each one is an appropriately-named module, e.g. `ProtectionBasedPriv`, with the following members:
@@ -61,7 +63,7 @@ presented in the paper quickly.
61
63
62
64
### Step by Step Instructions to Extending these Analyses
63
65
64
-
1. Modify or add thread-modular analyses in `./src/analyses/basePriv.ml`. (In case of adding also add to case distinction in `priv_module`)
66
+
1. Modify or add thread-modular analyses in `./src/analyses/basePriv.ml`. (In case of addition also add to a case distinction in `priv_module` at the end of this file.)
65
67
2. Run `make` and `make privPrecCompare`.
66
68
3. Observe updated behavior, either:
67
69
* Re-run the benchmarking as described above under Validation.
@@ -73,7 +75,7 @@ presented in the paper quickly.
73
75
or
74
76
75
77
* Run some of the regression tests in `tests/regression/13-privatized` by calling `./regtest.sh 13 xx` where `xx` is the number of the test. Especially `xx > 16` are interesting, these were added with the paper and highlight
76
-
differences between different approaches. If you added a new analysis make sure to pass `--sets exp.privatization chosenname` to the script.
78
+
differences between different approaches. Use the `--sets exp.privatization chosenname`option to choose which thread-modular analysis to use.
77
79
78
80
### Outline of how the code is structured
79
81
Lastly, we give a general outline of how code in the Goblint framework is organized:
0 commit comments