Merge branch 'master' into suppress_ovwarn

Author: sim642

.git-blame-ignore-revs

@@ -43,3 +43,6 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
 
 # Trim trailing whitespace in BitfieldDomain
 d4e2a5f84ed3b7fbff89e34b2f7833de975e0671
+
+# Fix BaseInvariant indentation
+15e7a7ebd34e9fabdd4129e97eb86830fea8395f

.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@v4
+        uses: actions/setup-node@v5
         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@v4
+        uses: actions/setup-node@v5
         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@v4
+        uses: actions/setup-node@v5
         with:
           node-version: ${{ matrix.node-version }}
 

CHANGELOG.md

@@ -1,18 +1,19 @@
-## v2.6.0 Awkward Aardvark (unreleased)
+## v2.6.0 Awkward Aardvark
 * Add division by zero analysis (#1764).
 * Add bitfield domain (#1623).
 * Add weakly-relational C-2PO pointer analysis (#1485).
 * Add widening delay (#1358, #1442, #1483).
 * Add narrowing of globals to top-down solver (#1636).
 * Add weak dependencies to top-down solver (#1746, #1747).
 * Add YAML ghost witness generation (#1394).
+* Remove GraphML witness generation (#1732, #1733, #1738).
 * Use C standard option for preprocessing (#1807).
 * Add bash completion for array options (#1670, #1705, #1750).
 * Make `malloc(0)` semantics configurable (#1418, #1777).
 * Update path-sensitive analyses (#1785, #1791, #1792).
 * Fix evaluation of library function arguments (#1758, #1761).
 * Optimize affine equalities analysis using sparse matrices (#1459, #1625).
-* Prepare for parallelism (#1708, #1744, #1748).
+* Prepare for parallelism (#1708, #1744, #1748, #1781, #1790).
 
 ## v2.5.0
 Functionally equivalent to Goblint in SV-COMP 2025.

docs/developer-guide/releasing.md

@@ -2,38 +2,41 @@
 
 ## opam
 
-1. Update list of authors and contributors in `.zenodo.json`, `CITATION.cff` and `dune-project`.
-2. Update `CHANGELOG.md`:
+1. Choose version name (collaboratively).
+2. Update list of authors and contributors in `.zenodo.json`, `CITATION.cff` and `dune-project`.
+3. Update `CHANGELOG.md`:
 
-    1. Add a desired version number (`vX.Y.Z`) header at the top.
+    1. Add a desired version number (`vX.Y.Z`) and name header at the top.
     2. Add a list of biggest changes compared to the previous version.
 
-3. Install dune-release: `opam install dune-release`.
 4. Remove all opam pins because _opam-repository doesn't allow them_.
 
     * If the pinned changes have been released and published in opam, remove the pin (and add a version lower bound).
     * If the pinned changes are not strictly necessary for building (but just optimization or stability), then temporarily remove the pin.
 
-5. Regenerate `goblint.opam`: `dune build`.
-6. Regenerate `goblint.opam.locked`: `opam pin add goblint.dev . --no-action` and `opam lock .`.
+5. Check opam file for previous release on opam-repository for changes.
+6. Regenerate `goblint.opam`: `dune build`.
+7. Regenerate `goblint.opam.locked`: `opam pin add goblint.dev . --no-action` and `opam lock .`.
 
     Pinning the package is necessary for locking, otherwise lockfile will be generated for previously published version.
     Manually remove not installed `depopts` from `conflicts`.
 
-7. Check with `dune-release check`.
+8. Install dune-release: `opam install dune-release`.
+
+9. Check with `dune-release check`.
 
     All changes must be committed because the working tree is not checked.
 
     The warning `[FAIL] opam field doc cannot be parsed by dune-release` is fine and can be ignored (see <https://github.com/ocamllabs/dune-release/issues/154>).
 
-8. Check that "unlocked" workflow passes on GitHub Actions.
+10. Check that "unlocked" workflow passes on GitHub Actions.
 
     It can be run manually on the release branch for checking.
 
-9. Tag the release: `dune-release tag`.
-10. Create the distribution archive: `dune-release distrib`.
+11. Tag the release: `dune-release tag`.
+12. Create the distribution archive: `dune-release distrib`.
 
-11. Check created _distribution archive_ (in `_build`) in a clean environment:
+13. Check created _distribution archive_ (in `_build`) in a clean environment:
 
     1. Pull Docker image: `docker pull ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
     2. Extract distribution archive.
@@ -46,21 +49,22 @@
     9. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
     10. Exit Docker container.
 
-12. Temporarily enable Zenodo GitHub webhook.
+14. Temporarily enable Zenodo GitHub webhook.
 
     This is because we only want numbered version releases to automatically add a new version to our Zenodo artifact.
     Other tags (like SV-COMP or paper artifacts) have manually created Zenodo artifacts anyway and thus shouldn't add new versions to the main Zenodo artifact.
 
-13. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
+15. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
 
     Explicitly specify `distrib` because we don't want to publish OCaml API docs.
     Environment variable workaround for the package having a Read the Docs `doc` URL (see <https://github.com/ocamllabs/dune-release/issues/154>).
 
-14. Re-disable Zenodo GitHub webhook.
+16. Re-disable Zenodo GitHub webhook.
 
-15. Create an opam package: `dune-release opam pkg`.
-16. Submit the opam package to opam-repository: `dune-release opam submit`.
-17. Revert temporary removal of opam pins.
+17. Edit GitHub release to add version name.
+18. Create an opam package: `dune-release opam pkg`.
+19. Submit the opam package to opam-repository: `dune-release opam submit`.
+20. Revert temporary removal of opam pins.
 
 
 ## SV-COMP

dune-project

@@ -37,7 +37,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     "concurrency"))
   (depends
     (ocaml (>= 4.14))
-    (goblint-cil (>= 2.0.5)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
+    (goblint-cil (>= 2.0.7)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
     (zarith (>= 1.10))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
@@ -71,13 +71,14 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     domain_shims
   )
   (depopts
-    (apron (>= v0.9.15))
-    (camlidl (>= 1.13)) ; for stability (https://github.com/goblint/analyzer/issues/1520)
+    apron
     z3
     domainslib
   )
   (conflicts
     (result (< 1.5)) ; transitive dependency, overrides standard Result module and doesn't have map_error, bind
+    (apron (< v0.9.15)) ; lower bounds for depopts seem to not properly constrain in builtin-0install lower-bounds job, so upper bounds for conflicts instead
+    (camlidl (< 1.13)) ; for stability (https://github.com/goblint/analyzer/issues/1520)
     (ez-conf-lib (= 1)) ; https://github.com/nberth/ez-conf-lib/issues/3
   )
   (sites

goblint.opam

@@ -37,7 +37,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.14"}
-  "goblint-cil" {>= "2.0.5"}
+  "goblint-cil" {>= "2.0.7"}
   "batteries" {>= "3.9.0"}
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0" & < "3"}
@@ -70,14 +70,11 @@ depends: [
   "domain-local-await"
   "domain_shims"
 ]
-depopts: [
-  "apron" {>= "v0.9.15"}
-  "camlidl" {>= "1.13"}
-  "z3"
-  "domainslib"
-]
+depopts: ["apron" "z3" "domainslib"]
 conflicts: [
   "result" {< "1.5"}
+  "apron" {< "v0.9.15"}
+  "camlidl" {< "1.13"}
   "ez-conf-lib" {= "1"}
 ]
 build: [
@@ -101,8 +98,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
+  [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -66,7 +66,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.6"}
+  "goblint-cil" {= "2.0.7"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -135,15 +135,17 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 conflicts: [
   "result" {< "1.5"}
+  "apron" {< "v0.9.15"}
+  "camlidl" {< "1.13"}
   "ez-conf-lib" {= "1"}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
 pin-depends: [
   [
-    "goblint-cil.2.0.6"
-    "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b"
+    "goblint-cil.2.0.7"
+    "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
+  [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]