Merge branch 'master' into logs

goblint · Jan 10, 2024 · eb8b14d · eb8b14d
2 parents bf4cb31 + 910b152
commit eb8b14d
Show file tree

Hide file tree

Showing 669 changed files with 16,504 additions and 8,377 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -65,6 +65,9 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -85,7 +88,7 @@ jobs:
           COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
           PULL_REQUEST_NUMBER: ${{ github.event.number }}
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: always()
         with:
           name: suite_result

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
@@ -35,21 +35,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -30,7 +30,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
+
+      - name: Check for undocumented modules
+        run: python scripts/goblint-lib-modules.py
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -43,7 +46,7 @@ jobs:
 
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v4
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc
@@ -65,4 +68,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v2
+        uses: actions/deploy-pages@v3
diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -64,6 +64,9 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -79,10 +82,10 @@ jobs:
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: always()
         with:
-          name: suite_result
+          name: suite_result-${{ matrix.os }}
           path: tests/suite_result/
 
   extraction:
@@ -101,7 +104,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -141,7 +144,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -153,7 +156,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
@@ -19,14 +19,17 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
         with:
           args: --validate
 
   zenodo-validate:
+    # Zenodo schema URL is dead
+    if: ${{ false }}
+
     strategy:
       matrix:
         node-version:
@@ -36,10 +39,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
@@ -15,21 +15,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
       - name: Install ajv-cli
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/util/options.schema.json
+        run: ajv migrate -s src/config/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"
diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
@@ -16,13 +16,13 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run semgrep
-        run: semgrep scan --sarif --output=semgrep.sarif
+        run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
-        uses: github/codeql-action/upload-sarif@v2
+        uses: github/codeql-action/upload-sarif@v3
         with:
           sarif_file: semgrep.sarif
         if: always()
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -18,6 +18,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
+          - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
           - 4.14.x
           - 4.13.x
@@ -45,7 +46,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -91,6 +92,10 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        if: ${{ matrix.apron }}
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -131,7 +136,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -155,7 +160,8 @@ jobs:
 
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda)
+        # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.4)
 
       - name: Build
         run: ./make.sh nat
@@ -208,14 +214,14 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           target: dev
@@ -246,7 +252,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2

diff --git a/.gitignore b/.gitignore
@@ -29,7 +29,6 @@ linux-headers
 .goblint*/
 goblint_temp_*/
 
-src/spec/graph
 .vagrant
 
 g2html.jar

diff --git a/.mailmap b/.mailmap
@@ -23,6 +23,7 @@ Kerem Çakırer <[email protected]> <[email protected]>
 Sarah Tilscher <[email protected]>
 Karoliine Holter <[email protected]>
 <[email protected]> <[email protected]>
+<[email protected]> <[email protected]>
 
 Elias Brandstetter <[email protected]> <[email protected]>
 wherekonshade <[email protected]> <[email protected]>
@@ -37,3 +38,6 @@ Mireia Cano Pujol <[email protected]>
 Felix Krayer <[email protected]>
 Felix Krayer <[email protected]> <[email protected]>
 Manuel Pietsch <[email protected]>
+Tim Ortel <[email protected]>
+Tomáš Dacík <[email protected]>
+<[email protected]> <[email protected]>
diff --git a/.readthedocs.yaml b/.readthedocs.yaml
@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/
diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
@@ -9,6 +9,7 @@ rules:
         - pattern: Messages.traceu
         - pattern: Messages.traceli
       - pattern-not-inside: if Messages.tracing then ...
+      - pattern-not-inside: if Messages.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING
diff --git a/.zenodo.json b/.zenodo.json
@@ -10,15 +10,18 @@
     },
     {
       "name": "Schwarz, Michael",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-9828-0308"
     },
     {
       "name": "Erhard, Julian",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-1729-3925"
     },
     {
       "name": "Tilscher, Sarah",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0009-0009-9644-7475"
     },
     {
       "name": "Vogler, Ralf",
@@ -30,14 +33,16 @@
     },
     {
       "name": "Vojdani, Vesal",
-      "affiliation": "University of Tartu"
+      "affiliation": "University of Tartu",
+      "orcid": "0000-0003-4336-7980"
     }
   ],
   "contributors": [
     {
       "name": "Seidl, Helmut",
       "type": "ProjectLeader",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-2135-1593"
     },
     {
       "name": "Schwarz, Martin D.",