Merge branch 'master' into assert-ptr

Author: sim642

.gitattributes

@@ -0,0 +1,13 @@
+# GitHub repository language overrides
+# https://github.com/github-linguist/linguist/blob/main/docs/overrides.md
+
+# currently only dune-project is classified: https://github.com/github-linguist/linguist/pull/7126
+dune linguist-language=dune
+dune.inc linguist-language=dune
+
+# avoid misclassification as Standard ML
+*.ml linguist-language=ocaml
+*.mli linguist-language=ocaml
+
+# cram tests are classified as Raku/Terra/Turing, cram isn't separate language so consider them also dune
+*.t linguist-language=dune

.github/workflows/coverage.yml

@@ -39,13 +39,16 @@ 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
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Install coverage dependencies
         run: opam install bisect_ppx
 

.github/workflows/locked.yml

@@ -41,13 +41,16 @@ 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
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -90,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
 
@@ -100,60 +103,11 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
       - name: Test extraction
         run: opam exec -- dune runtest tests/extraction
-
-
-  gobview:
-    strategy:
-      fail-fast: false
-      matrix:
-        os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-        ocaml-compiler:
-          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
-          # don't add any other because they won't be used
-        node-version:
-          - 14
-
-    runs-on: ${{ matrix.os }}
-
-    steps:
-      - name: Checkout code
-        uses: actions/checkout@v4
-
-      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        env:
-          # otherwise setup-ocaml pins non-locked dependencies
-          # https://github.com/ocaml/setup-ocaml/issues/166
-          OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v3
-        with:
-          ocaml-compiler: ${{ matrix.ocaml-compiler }}
-
-      - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
-        with:
-          node-version: ${{ matrix.node-version }}
-
-      - name: Install dependencies
-        run: opam install . --deps-only --locked
-
-      - name: Setup Gobview
-        run: ./make.sh setup_gobview
-
-      - name: Build
-        run: ./make.sh nat
-
-      - name: Build Gobview
-        run: ./make.sh view
-
-      - name: Install selenium
-        run: pip3 install selenium webdriver-manager
-
-      - name: Test Gobview
-        run: |
-          python3 scripts/test-gobview.py

.github/workflows/unlocked.yml

@@ -51,24 +51,23 @@ 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
 
       - 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
@@ -83,57 +82,44 @@ 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
 
       - 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
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
-      - name: Install Apron dependencies
-        run: |
-          opam depext apron
-          opam install apron mlgmpidl.1.2.15
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
 
-      - name: Build
-        if: ${{ false }}
-        run: ./make.sh nat
-
-      - name: Install opam-0install
-        run: opam install opam-0install
+      - name: Install Apron dependencies
+        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
@@ -147,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
@@ -203,17 +154,15 @@ 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
 
       - 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
@@ -251,3 +200,49 @@ jobs:
 
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
+
+  gobview:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+        ocaml-compiler:
+          - ocaml-variants.5.0.0+options,ocaml-option-flambda
+        node-version:
+          - 14
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - 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
+        with:
+          node-version: ${{ matrix.node-version }}
+
+      - name: Install dependencies
+        run: opam install . --deps-only
+
+      - name: Setup Gobview
+        run: ./make.sh setup_gobview
+
+      - name: Build
+        run: ./make.sh nat
+
+      - name: Build Gobview
+        run: ./make.sh view
+
+      - name: Install selenium
+        run: pip3 install selenium webdriver-manager
+
+      - name: Test Gobview
+        run: |
+          python3 scripts/test-gobview.py

.semgrep/batenum.yml

@@ -0,0 +1,28 @@
+rules:
+  - id: batenum-module
+    pattern-either:
+      - pattern: BatEnum.$F
+      - pattern: Enum.$F
+    message: use Seq.$F instead
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: batenum-of_enum
+    patterns:
+      - pattern: $M.of_enum
+      - metavariable-pattern:
+          metavariable: $M
+          pattern-regex: ^[A-Z].*
+    message: use $M.of_seq instead
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: batenum-enum
+    patterns:
+      - pattern: $M.enum
+      - metavariable-pattern:
+          metavariable: $M
+          pattern-regex: ^[A-Z].*
+    message: use $M.to_seq instead
+    languages: [ocaml]
+    severity: WARNING

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2005-2021 University of Tartu & Technische Universität München.
+Copyright (c) 2005-2025 University of Tartu & Technische Universität München.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -60,6 +60,6 @@ For further information, see [documentation](https://goblint.readthedocs.io/en/l
 
 ## Acknowledgements
 
-Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.
+Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 MBAT), ITEA3 project 14014 ASSUME, the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.
 
-We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.
+We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.

bench/basic/benchTuple4.ml

@@ -7,7 +7,7 @@ open Benchmark.Tree
 let () =
   let exists0 =
     let open Batteries in
-    let to_list x = Tuple4.enum x |> List.of_enum |> List.filter_map identity in
+    let to_list (a,b,c,d) = List.filter_map identity [a;b;c;d] in
     let f g = g identity % to_list in
     List.(f exists)
   in
@@ -74,7 +74,7 @@ let () =
 let () =
   let for_all0 =
     let open Batteries in
-    let to_list x = Tuple4.enum x |> List.of_enum |> List.filter_map identity in
+    let to_list (a,b,c,d) = List.filter_map identity [a;b;c;d] in
     let f g = g identity % to_list in
     List.(f for_all)
   in