Merge branch 'master' into violation_witnesses

Author: karoliineh

.github/workflows/coverage.yml

@@ -66,7 +66,7 @@ jobs:
           COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
           PULL_REQUEST_NUMBER: ${{ github.event.number }}
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: suite_result

.github/workflows/locked.yml

@@ -60,7 +60,7 @@ jobs:
       - name: Test
         run: opam exec -- dune runtest
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: suite_result-${{ matrix.os }}

.github/workflows/metadata.yml

@@ -42,7 +42,7 @@ jobs:
         uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v5
+        uses: actions/setup-node@v6
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/options.yml

@@ -18,7 +18,7 @@ jobs:
         uses: actions/checkout@v5
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v5
+        uses: actions/setup-node@v6
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/unlocked.yml

@@ -224,7 +224,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v5
+        uses: actions/setup-node@v6
         with:
           node-version: ${{ matrix.node-version }}
 

.gitignore

@@ -54,6 +54,7 @@ goblint.bc.js
 *.rej
 
 sv-comp/goblint.zip
+scripts/sv-comp/goblint.zip
 
 privPrecCompare
 privPrecCompare-creduce

.semgrep/apron.yml

@@ -0,0 +1,9 @@
+rules:
+  - id: apron-linexp0-get_size
+    pattern-either:
+      - pattern: Linexpr0.get_size
+      - pattern: Apron.Linexpr0.get_size
+      - pattern: GobApron.Linexpr0.get_size
+    message: don't use (returns some internal size, not number of dimensions)
+    languages: [ocaml]
+    severity: ERROR

.semgrep/batio.yml

@@ -0,0 +1,6 @@
+rules:
+  - id: batio-to_input_channel
+    pattern: BatIO.to_input_channel
+    message: don't use (leaks two file descriptors)
+    languages: [ocaml]
+    severity: ERROR

.semgrep/cil.yml

@@ -15,3 +15,11 @@ rules:
     message: use Cilfacade instead
     languages: [ocaml]
     severity: WARNING
+
+  - id: cil-var
+    pattern: (Var $X, NoOffset)
+    # Autofix is broken: https://github.com/semgrep/semgrep/issues/11278
+    # fix: GoblintCil.var $X
+    message: use GoblintCil.var instead
+    languages: [ocaml]
+    severity: WARNING

.semgrep/let.yml

@@ -0,0 +1,6 @@
+rules:
+  - id: let-unit-in
+    pattern: let () = $E in ...
+    message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
+    languages: [ocaml]
+    severity: WARNING