From eb80bce46dc125984e76f549aaa5d5365d5fddeb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Sep 2023 14:34:03 +0300 Subject: [PATCH] [new release] goblint (2.2.0) CHANGES: * Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019). * Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016). * Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082). * Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073). * Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048). * Add affine equalities analysis (goblint/analyzer#592). * Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114). * Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979). * Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952). * Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124). * Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777). * Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031). * Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078). * Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091). * Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027). * Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053). * Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138). * Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162). --- packages/goblint/goblint.2.2.0/opam | 93 +++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 packages/goblint/goblint.2.2.0/opam diff --git a/packages/goblint/goblint.2.2.0/opam b/packages/goblint/goblint.2.2.0/opam new file mode 100644 index 00000000000..0b912026f59 --- /dev/null +++ b/packages/goblint/goblint.2.2.0/opam @@ -0,0 +1,93 @@ +opam-version: "2.0" +synopsis: "Static analysis framework for C" +maintainer: [ + "Simmo Saan " + "Michael Schwarz " +] +authors: [ + "Simmo Saan" + "Michael Schwarz" + "Julian Erhard" + "Sarah Tilscher" + "Ralf Vogler" + "Kalmer Apinis" + "Vesal Vojdani" +] +license: "MIT" +homepage: "https://goblint.in.tum.de" +doc: "https://goblint.readthedocs.io/en/latest/" +bug-reports: "https://github.com/goblint/analyzer/issues" +depends: [ + "dune" {>= "3.6"} + "ocaml" {>= "4.10"} + "goblint-cil" {>= "2.0.2"} + "batteries" {>= "3.4.0"} + "zarith" {>= "1.8"} + "yojson" {>= "2.0.0"} + "qcheck-core" {>= "0.19"} + "ppx_deriving" + "ppx_deriving_hash" + "ppx_deriving_yojson" {>= "3.7.0"} + "ounit2" {with-test} + "qcheck-ounit" {with-test} + "odoc" {with-doc} + "fpath" + "dune-site" + "dune-build-info" + "json-data-encoding" + "jsonrpc" {>= "1.12"} + "sha" {>= "1.12"} + "fileutils" {>= "0.6.4"} + "cpu" + "arg-complete" + "yaml" {>= "3.0.0"} + "uuidm" + "catapult" + "catapult-file" + "conf-gmp" {>= "3"} + "conf-ruby" {with-test} + "benchmark" {with-test} + "conf-gcc" +] +depopts: ["apron" "z3"] +conflicts: [ + "result" {< "1.5"} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +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.2 is currently up-to-date, so no pin needed + # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ] + # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) + # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] +# ] +post-messages: [ + "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} +] +url { + src: + "https://github.com/goblint/analyzer/releases/download/v2.2.0/goblint-2.2.0.tbz" + checksum: [ + "sha256=33eb081049a15b3db884b370766517dd9e79394873079b9d9f7b10cb6e6453d0" + "sha512=5ead207f73ee022957a1c98191278bf6942f8e4e3351da8e34fa90b3ff76c33b055269b67f5a869695549f55c7aeed1f1cbe848c961f11cad590eeadea9df7fc" + ] +} +x-commit-hash: "b46aeda9eaecd3ec42ec14c977d1550faad0de23"