Merge branch 'master' into null-byte-arrayDomain

.github/workflows/coverage.yml

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

.github/workflows/locked.yml

@@ -64,6 +64,9 @@ 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
 
@@ -153,7 +156,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/metadata.yml

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

.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@v3
+        uses: actions/setup-node@v4
         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/util/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/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/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"

.github/workflows/unlocked.yml

@@ -92,6 +92,10 @@ 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
 
@@ -156,7 +160,8 @@ jobs:
 
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda)
+        # 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)
 
       - name: Build
         run: ./make.sh nat

.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/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/

.zenodo.json

@@ -10,15 +10,18 @@
     },
     {
       "name": "Schwarz, Michael",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-9828-0308"
     },
     {
       "name": "Erhard, Julian",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-1729-3925"
     },
     {
       "name": "Tilscher, Sarah",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0009-0009-9644-7475"
     },
     {
       "name": "Vogler, Ralf",
@@ -30,14 +33,16 @@
     },
     {
       "name": "Vojdani, Vesal",
-      "affiliation": "University of Tartu"
+      "affiliation": "University of Tartu",
+      "orcid": "0000-0003-4336-7980"
     }
   ],
   "contributors": [
     {
       "name": "Seidl, Helmut",
       "type": "ProjectLeader",
-      "affiliation": "Technische Universität München"
+      "affiliation": "Technische Universität München",
+      "orcid": "0000-0002-2135-1593"
     },
     {
       "name": "Schwarz, Martin D.",

CHANGELOG.md

@@ -1,3 +1,15 @@
+## 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.

CITATION.cff

@@ -12,12 +12,15 @@ 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"
@@ -27,6 +30,7 @@ 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"

conf/ldv-races.json

@@ -53,8 +53,11 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "solver": "td3",
   "sem": {

conf/svcomp-yaml.json

@@ -76,7 +76,9 @@
     "region-offsets": true
   },
   "witness": {
-    "enabled": false,
+    "graphml": {
+      "enabled": false
+    },
     "yaml": {
       "enabled": true
     },

conf/svcomp.json

@@ -32,6 +32,15 @@
       "thread",
       "threadJoins"
     ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
     "context": {
       "widen": false
     },
@@ -52,14 +61,19 @@
 
         "ldv_xmalloc",
         "ldv_xzalloc",
-        "ldv_calloc"
+        "ldv_calloc",
+        "ldv_kzalloc"
       ]
     },
     "base": {
       "arrays": {
         "domain": "partitioned"
       }
     },
+    "race": {
+      "free": false,
+      "call": false
+    },
     "autotune": {
       "enabled": true,
       "activated": [
@@ -70,7 +84,10 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
       ]
     }
   },
@@ -90,8 +107,38 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
   },
   "pre": {
     "enabled": false

conf/svcomp21.json

@@ -64,6 +64,9 @@
     }
   },
   "witness": {
-    "id": "enumerate"
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate"
+    }
   }
 }

conf/svcomp22-intervals-novareq-affeq-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-affeq-native.json

@@ -65,7 +65,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-octagon-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-polyhedra-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22.json

@@ -67,7 +67,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp23.json

@@ -90,7 +90,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }