Merge branch 'v2.4.x'

goblint · Aug 2, 2024 · b129fab · b129fab
2 parents a592680 + 0ad776f
commit b129fab
Show file tree

Hide file tree

Showing 10 changed files with 39 additions and 23 deletions.
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -33,6 +33,8 @@ jobs:
           - os: ubuntu-latest
             ocaml-compiler: 4.14.x
             z3: true
+          - os: macos-latest
+            ocaml-compiler: 4.14.x
 
     # customize name to use readable string for apron instead of just a boolean
     # workaround for missing ternary operator: https://github.com/actions/runner/issues/409

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,22 @@
+## v2.4.0
+* Remove unmaintained analyses: spec, file (#1281).
+* Add linear two-variable equalities analysis (#1297, #1412, #1466).
+* Add callstring, loopfree callstring and context gas analyses (#1038, #1340, #1379, #1427, #1439).
+* Add non-relational thread-modular value analyses with thread IDs (#1366, #1398, #1399).
+* Add NULL byte array domain (#1076).
+* Fix spurious overflow warnings from internal evaluations (#1406, #1411, #1511).
+* Refactor non-definite mutex handling to fix unsoundness (#1430, #1500, #1503, #1409).
+* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (#1457, #1458).
+* Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
+* Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
+* Improve narrowing operators (#1502, #1540, #1543).
+* Extract automatic configuration tuning for soundness (#1369).
+* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
+* Improve output readability (#1294, #1312, #1405, #1497).
+* Refactor logging (#1117).
+* Modernize all library function specifications (#1029, #688, #1174, #1289, #1447, #1487).
+* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (#1448).
+
 ## v2.3.0
 Functionally equivalent to Goblint in SV-COMP 2024.
 

diff --git a/bench/basic/benchSet.ml b/bench/basic/benchSet.ml
@@ -73,7 +73,7 @@ let () =
         ]
       );
       "const" @> lazy (
-        let args = ((fun x -> 42), set1) in
+        let args = ((fun _ -> 42), set1) in
         throughputN 1 [
           ("map1", map1, args);
           ("map2", map2, args);

diff --git a/dune-project b/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.3)) ; 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.4)) ; 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.5.1))
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))

diff --git a/goblint.opam b/goblint.opam
@@ -37,7 +37,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.14"}
-  "goblint-cil" {>= "2.0.3"}
+  "goblint-cil" {>= "2.0.4"}
   "batteries" {>= "3.5.1"}
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
@@ -93,11 +93,11 @@ build: [
 dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
-available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-]
+available: os-family != "bsd" & os-distribution != "alpine"
+# pin-depends: [
+  # published goblint-cil 2.0.4 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
+# ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -64,7 +64,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.3"}
+  "goblint-cil" {= "2.0.4"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -128,21 +128,14 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
-available: os-distribution != "alpine" & arch != "arm64"
+available: os-family != "bsd" & os-distribution != "alpine"
 conflicts: [
   "result" {< "1.5"}
   "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"}
 ]
-# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
-pin-depends: [
-  [
-    "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
-  ]
-]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 description: """\
 Goblint is a sound static analysis framework for C programs using abstract interpretation.

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,10 +1,10 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
-available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-]
+available: os-family != "bsd" & os-distribution != "alpine"
+# pin-depends: [
+  # published goblint-cil 2.0.4 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
+# ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]

diff --git a/gobview b/gobview
diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml
@@ -698,6 +698,7 @@ struct
     | AAddrOf of t
     | AIndex of t * t
     | AQuestion of t * t * t
+    | AAssign of t * t
   [@@deriving eq, ord, hash]
 
   let name () = "attrparam"

diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
@@ -210,6 +210,7 @@ and eq_attrparam (a: attrparam) (b: attrparam) ~(rename_mapping: rename_mapping)
   | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
   | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc
   | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam middle1 middle2 ~acc &&>> eq_attrparam right1 right2 ~acc
+  | AAssign (left1, right1), AAssign (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc
   | a, b -> a = b, rename_mapping
 
 and eq_attribute (a: attribute) (b: attribute) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = match a, b with