Merge branch 'master' into enum-to-seq

Author: karoliineh

.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

@@ -46,6 +46,9 @@ 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: Install coverage dependencies
         run: opam install bisect_ppx
 

.github/workflows/locked.yml

@@ -48,6 +48,9 @@ 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
 
@@ -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

@@ -57,6 +57,9 @@ jobs:
 
       - 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 }}
@@ -118,6 +121,9 @@ jobs:
       - 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
         run: |
           opam depext apron
@@ -251,3 +257,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

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.

conf/bench-yaml-validate.json

@@ -71,7 +71,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

conf/bench-yaml.json

@@ -67,7 +67,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

conf/ldv-races.json

@@ -1,7 +1,6 @@
 {
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
@@ -67,13 +66,6 @@
       "klever"
     ]
   },
-  "witness": {
-    "graphml": {
-      "enabled": true,
-      "id": "enumerate",
-      "unknown": false
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {

conf/svcomp-ghost.json

@@ -81,7 +81,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
@@ -112,9 +112,6 @@
     }
   },
   "witness": {
-    "graphml": {
-      "enabled": false
-    },
     "yaml": {
       "enabled": true,
       "format-version": "2.1",