Skip to content

Commit 9fecf6e

Browse files
committed
Add Goblint code references to VMCAI25 artifact description
1 parent fa3538c commit 9fecf6e

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

docs/artifact-descriptions/vmcai25.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,16 @@ More recent versions of Ultimate can be found at <https://github.com/ultimate-pa
236236

237237
The Goblint analyzer (<https://goblint.in.tum.de>) is developed by TU Munich and University of Tartu. The source code for Goblint at the time of evaluation can be found in this artifact in the `~/goblint` directory.
238238

239+
The code for this paper is the following:
240+
241+
1. `src/witness/witnessGhostVar.ml` and `src/witness/witnessGhost.ml` define the data types for ghost variables.
242+
2. `src/analyses/mutexGhosts.ml` defines the analysis which determines the ghost variables for a specific program and their updates.
243+
3. `src/analyses/basePriv.ml` lines 342-365 define the invariants with mutex ghost variables from non-relational _mutex-meet_ analysis.
244+
4. `src/analyses/apron/relationPriv.apron.ml` lines 717-750 define the invariants with mutex ghost variables from relational _mutex-meet_ analysis.
245+
5. `src/analyses/base.ml` lines 1269-1289 and `src/analyses/apron/relationAnalysis.apron.ml` lines 637-644 define the wrapping of the invariants with multithreaded mode ghost variables.
246+
6. `src/analyses/basePriv.ml` lines 882-909 define the invariants with mutex ghost variables from (non-relational) _protection_ analysis.
247+
7. `src/witness/yamlWitness.ml` lines 398-421 and 589-621 define the YAML output of ghost variables, their updates and the invariants.
248+
239249
More recent versions of Goblint can be found at <https://github.com/goblint>.
240250

241251
----------------------------------------------------------------------------------

0 commit comments

Comments
 (0)