diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 6a9eced42c..0c4433d0af 100644 --- 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 index d285480259..420cc7145e 100644 --- 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 index 14eb03be82..ae38c156da 100644 --- 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 index 3927e77bdd..f854518419 100644 --- 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 index 7fe108f682..85068b4114 100644 --- 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 index 252459d517..ca03f318b4 100644 --- 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,7 +128,7 @@ 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"} @@ -136,13 +136,6 @@ conflicts: [ 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 index a730d5c064..605f07751c 100644 --- 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 index 03b0682f97..76e42c34d3 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 03b0682f973eab0d26cf8aea74c63a9e869c9716 +Subproject commit 76e42c34d36bd2ab6900efd661a972ba4824f065 diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml index a484a228bd..5a473b7d60 100644 --- 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 index f3de153658..2449cdac47 100644 --- 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