Revert "Merge remote-tracking branch 'upstream/master' into relationa…

…lArray" This reverts commit 9a033b4.
goblint · Jan 24, 2024 · a9c9eb7 · a9c9eb7
1 parent 97edbd7
commit a9c9eb7
Show file tree

Hide file tree

Showing 462 changed files with 6,249 additions and 9,522 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -65,9 +65,6 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
-      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
-        run: ruby scripts/update_suite.rb group termination -s
-
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -88,7 +85,7 @@ jobs:
           COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
           PULL_REQUEST_NUMBER: ${{ github.event.number }}
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v3
         if: always()
         with:
           name: suite_result

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -46,7 +46,7 @@ jobs:
 
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v4
+        uses: actions/configure-pages@v3
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc
@@ -68,4 +68,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v3
+        uses: actions/deploy-pages@v2
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -64,9 +64,6 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
-      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
-        run: ruby scripts/update_suite.rb group termination -s
-
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -82,10 +79,10 @@ jobs:
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v3
         if: always()
         with:
-          name: suite_result-${{ matrix.os }}
+          name: suite_result
           path: tests/suite_result/
 
   extraction:
@@ -156,7 +153,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v3
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
@@ -27,9 +27,6 @@ jobs:
           args: --validate
 
   zenodo-validate:
-    # Zenodo schema URL is dead
-    if: ${{ false }}
-
     strategy:
       matrix:
         node-version:
@@ -42,7 +39,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v3
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
@@ -18,18 +18,18 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v3
         with:
           node-version: ${{ matrix.node-version }}
 
       - name: Install ajv-cli
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/config/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
@@ -22,7 +22,7 @@ jobs:
         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@v2
         with:
           sarif_file: semgrep.sarif
         if: always()
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -92,10 +92,6 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
-      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
-        if: ${{ matrix.apron }}
-        run: ruby scripts/update_suite.rb group termination -s
-
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
@@ -160,8 +156,7 @@ jobs:
 
       - 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.0+options ocaml-option-flambda num.1.4)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda)
 
       - name: Build
         run: ./make.sh nat

diff --git a/.gitignore b/.gitignore
@@ -29,6 +29,7 @@ linux-headers
 .goblint*/
 goblint_temp_*/
 
+src/spec/graph
 .vagrant
 
 g2html.jar

diff --git a/.gitmodules b/.gitmodules
@@ -4,3 +4,6 @@
 [submodule "g2html"]
 	path = g2html
 	url = https://github.com/goblint/g2html.git
+[submodule "gobview"]
+	path = gobview
+	url = https://github.com/goblint/gobview.git
diff --git a/.mailmap b/.mailmap
@@ -23,7 +23,6 @@ Kerem Çakırer <[email protected]> <[email protected]>
 Sarah Tilscher <[email protected]>
 Karoliine Holter <[email protected]>
 <[email protected]> <[email protected]>
-<[email protected]> <[email protected]>
 
 Elias Brandstetter <[email protected]> <[email protected]>
 wherekonshade <[email protected]> <[email protected]>
@@ -38,6 +37,3 @@ Mireia Cano Pujol <[email protected]>
 Felix Krayer <[email protected]>
 Felix Krayer <[email protected]> <[email protected]>
 Manuel Pietsch <[email protected]>
-Tim Ortel <[email protected]>
-Tomáš Dacík <[email protected]>
-<[email protected]> <[email protected]>
diff --git a/.readthedocs.yaml b/.readthedocs.yaml
@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/
diff --git a/.zenodo.json b/.zenodo.json
@@ -10,18 +10,15 @@
     },
     {
       "name": "Schwarz, Michael",
-      "affiliation": "Technische Universität München",
-      "orcid": "0000-0002-9828-0308"
+      "affiliation": "Technische Universität München"
     },
     {
       "name": "Erhard, Julian",
-      "affiliation": "Technische Universität München",
-      "orcid": "0000-0002-1729-3925"
+      "affiliation": "Technische Universität München"
     },
     {
       "name": "Tilscher, Sarah",
-      "affiliation": "Technische Universität München",
-      "orcid": "0009-0009-9644-7475"
+      "affiliation": "Technische Universität München"
     },
     {
       "name": "Vogler, Ralf",
@@ -33,16 +30,14 @@
     },
     {
       "name": "Vojdani, Vesal",
-      "affiliation": "University of Tartu",
-      "orcid": "0000-0003-4336-7980"
+      "affiliation": "University of Tartu"
     }
   ],
   "contributors": [
     {
       "name": "Seidl, Helmut",
       "type": "ProjectLeader",
-      "affiliation": "Technische Universität München",
-      "orcid": "0000-0002-2135-1593"
+      "affiliation": "Technische Universität München"
     },
     {
       "name": "Schwarz, Martin D.",

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,15 +1,3 @@
-## v2.3.0
-Functionally equivalent to Goblint in SV-COMP 2024.
-
-* Add termination analysis for loops (#1093).
-* Add memory out-of-bounds analysis (#1094, #1197).
-* Add memory leak analysis (#1127, #1241, #1246).
-* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (#1220, #1228, #1201, #1199, #1259, #1262).
-* Add YAML witness version 2.0 support (#1238, #1240, #1217, #1226, #1225, #1248).
-* Add final warnings about unsound results (#1190, #1191).
-* Add many library function specifications (#1167, #1174, #1203, #1205, #1212, #1220, #1239, #1242, #1244, #1254, #1269).
-* Adapt automatic configuration tuning (#912, #921, #987, #1168, #1214, #1234).
-
 ## v2.2.1
 * Bump batteries lower bound to 3.5.0.
 * Fix flaky dead code elimination transformation test.

diff --git a/CITATION.cff b/CITATION.cff
@@ -12,15 +12,12 @@ authors: # same authors as in .zenodo.json and dune-project
   - given-names: Michael
     family-names: Schwarz
     affiliation: "Technische Universität München"
-    orcid: "https://orcid.org/0000-0002-9828-0308"
   - given-names: Julian
     family-names: Erhard
     affiliation: "Technische Universität München"
-    orcid: "https://orcid.org/0000-0002-1729-3925"
   - given-names: Sarah
     family-names: Tilscher
     affiliation: "Technische Universität München"
-    orcid: "https://orcid.org/0009-0009-9644-7475"
   - given-names: Ralf
     family-names: Vogler
     affiliation: "Technische Universität München"
@@ -30,7 +27,6 @@ authors: # same authors as in .zenodo.json and dune-project
   - given-names: Vesal
     family-names: Vojdani
     affiliation: "University of Tartu"
-    orcid: "https://orcid.org/0000-0003-4336-7980"
 
 license: MIT
 repository-code: "https://github.com/goblint/analyzer"

diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json
@@ -61,9 +61,7 @@
       "structs" : {
         "domain" : "combined-sk"
       },
-      "strings": {
-        "domain": "disjoint"
-      }
+      "limit-string-addresses": false
     }
   },
   "exp": {

diff --git a/conf/ldv-races.json b/conf/ldv-races.json
@@ -29,9 +29,7 @@
       "escape",
       "expRelation",
       "mhp",
-      "assert",
-      "var_eq",
-      "symb_locks"
+      "assert"
     ],
     "malloc": {
       "wrappers": [
@@ -54,25 +52,9 @@
       ]
     }
   },
-  "lib": {
-    "activated": [
-      "c",
-      "posix",
-      "pthread",
-      "gcc",
-      "glibc",
-      "linux-userspace",
-      "goblint",
-      "ncurses",
-      "klever"
-    ]
-  },
   "witness": {
-    "graphml": {
-      "enabled": true,
-      "id": "enumerate",
-      "unknown": false
-    }
+    "id": "enumerate",
+    "unknown": false
   },
   "solver": "td3",
   "sem": {

diff --git a/conf/min-unsound.json b/conf/min-unsound.json
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
@@ -76,9 +76,7 @@
     "region-offsets": true
   },
   "witness": {
-    "graphml": {
-      "enabled": false
-    },
+    "enabled": false,
     "yaml": {
       "enabled": true
     },