Merge branch 'master' into violation_witnesses

Author: karoliineh

.git-blame-ignore-revs

@@ -40,3 +40,9 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
 
 # Rename ctx -> man
 0c155e68607fede6fab17704a9a7aee38df5408e
+
+# Trim trailing whitespace in BitfieldDomain
+d4e2a5f84ed3b7fbff89e34b2f7833de975e0671
+
+# Fix BaseInvariant indentation
+15e7a7ebd34e9fabdd4129e97eb86830fea8395f

.github/workflows/coverage.yml

@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -39,7 +39,7 @@ jobs:
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
@@ -48,7 +48,7 @@ jobs:
 
       - name: Install os gem for operating system detection
         run: sudo gem install os
-        
+
       - name: Install coverage dependencies
         run: opam install bisect_ppx
 

.github/workflows/docker.yml

@@ -35,7 +35,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action

.github/workflows/docs.yml

@@ -25,7 +25,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Check for undocumented modules
         run: python scripts/goblint-lib-modules.py
@@ -50,7 +50,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v3
+        uses: actions/upload-pages-artifact@v4
         with:
           path: _build/default/_doc/_html/
 

.github/workflows/indentation.yml

@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
         with:
           fetch-depth: 0
 

.github/workflows/locked.yml

@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -41,7 +41,7 @@ jobs:
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
@@ -82,7 +82,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -93,7 +93,7 @@ jobs:
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 

.github/workflows/metadata.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -39,10 +39,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/options.yml

@@ -15,10 +15,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/semgrep.yml

@@ -16,13 +16,13 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Run semgrep
         run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
-        uses: github/codeql-action/upload-sarif@v3
+        uses: github/codeql-action/upload-sarif@v4
         with:
           sarif_file: semgrep.sarif
         if: always()

.github/workflows/unlocked.yml

@@ -44,34 +44,30 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
-      
+
       - name: Install os gem for operating system detection
         run: sudo gem install os
 
       - name: Install Apron dependencies
         if: ${{ matrix.apron }}
-        run: |
-          opam depext apron
-          opam install apron mlgmpidl.1.2.15
+        run: opam install apron mlgmpidl.1.2.15
 
       - name: Install Z3 dependencies
         if: ${{ matrix.z3 }}
-        run: |
-          opam depext z3
-          opam install z3
+        run: opam install z3
 
       - name: Build
         run: ./make.sh nat
@@ -86,35 +82,29 @@ jobs:
         run: ruby scripts/update_suite.rb -m
 
   lower-bounds-downgrade:
-    # use external 0install solver to downgrade: https://github.com/ocaml-opam/opam-0install-solver
-    # TODO: will be built in in opam 2.2: https://github.com/ocaml/opam/pull/4909
-
     strategy:
       fail-fast: false
       matrix:
         os:
           - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
     name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
 
     runs-on: ${{ matrix.os }}
 
-    env:
-      OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts
-
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
@@ -125,21 +115,11 @@ jobs:
         run: sudo gem install os
 
       - name: Install Apron dependencies
-        run: |
-          opam depext apron
-          opam install apron mlgmpidl.1.2.15
-
-      - name: Build
-        if: ${{ false }}
-        run: ./make.sh nat
-
-      - name: Install opam-0install
-        run: opam install opam-0install
+        run: opam install apron mlgmpidl.1.2.15
 
       - name: Downgrade dependencies
-        # must specify ocaml-base-compiler again to prevent it from being downgraded
-        # 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.2+options ocaml-option-flambda num.1.5)
+        # without "+removed" in criteria, because it also removes optional apron
+        run: opam install --solver=builtin-0install --criteria="+count[version-lag,solution]" . --deps-only --with-test
 
       - name: Build
         run: ./make.sh nat
@@ -153,41 +133,6 @@ jobs:
       - name: Test marshal regression # not part of @runtest due to time
         run: ruby scripts/update_suite.rb -m
 
-  lower-bounds-docker:
-    # use builtin-0install solver to remove and downgrade, opam normally compiled without, Docker images have it compiled
-
-    if: ${{ false }}
-
-    name: lower-bounds (docker)
-
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Checkout code
-        uses: actions/checkout@v4
-
-      - name: Set up Docker Buildx
-        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@v6
-        with:
-          context: .
-          target: dev
-          load: true # load into docker instead of immediately pushing
-          tags: dev
-          cache-from: type=gha
-          cache-to: type=gha,mode=max # max mode caches all layers for multi-stage image
-
-      - name: Run opam downgrade and tests in dev Docker image
-        uses: addnab/docker-run-action@v3
-        with:
-          image: dev
-          run: |
-            OPAMCRITERIA=+removed,+count[version-lag,solution] OPAMEXTERNALSOLVER=builtin-0install opam-2.1 install . --deps-only --with-test --confirm-level=unsafe-yes
-            opam exec -- dune runtest
-
   opam-install:
     strategy:
       fail-fast: false
@@ -202,24 +147,22 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
-      - name: Install graph-easy # TODO: remove if depext --with-test works
+      - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
         if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test
         run: opam install goblint --with-test
 
       - name: Install Apron dependencies
-        run: |
-          opam depext apron
-          opam install apron mlgmpidl.1.2.15
+        run: opam install apron mlgmpidl.1.2.15
 
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint
@@ -265,23 +208,23 @@ jobs:
         os:
           - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - ocaml-variants.5.0.0+options,ocaml-option-flambda 
+          - ocaml-variants.5.0.0+options,ocaml-option-flambda
         node-version:
           - 14
 
     runs-on: ${{ matrix.os }}
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}