From 8063adb66e6d7289e79a9ea8aa208fc4e62bdbb4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 5 Sep 2025 14:09:39 +0300 Subject: [PATCH] [new release] goblint (2.6.0) CHANGES: * Add division by zero analysis (goblint/analyzer#1764). * Add bitfield domain (goblint/analyzer#1623). * Add weakly-relational C-2PO pointer analysis (goblint/analyzer#1485). * Add widening delay (goblint/analyzer#1358, goblint/analyzer#1442, goblint/analyzer#1483). * Add narrowing of globals to top-down solver (goblint/analyzer#1636). * Add weak dependencies to top-down solver (goblint/analyzer#1746, goblint/analyzer#1747). * Add YAML ghost witness generation (goblint/analyzer#1394). * Remove GraphML witness generation (goblint/analyzer#1732, goblint/analyzer#1733, goblint/analyzer#1738). * Use C standard option for preprocessing (goblint/analyzer#1807). * Add bash completion for array options (goblint/analyzer#1670, goblint/analyzer#1705, goblint/analyzer#1750). * Make `malloc(0)` semantics configurable (goblint/analyzer#1418, goblint/analyzer#1777). * Update path-sensitive analyses (goblint/analyzer#1785, goblint/analyzer#1791, goblint/analyzer#1792). * Fix evaluation of library function arguments (goblint/analyzer#1758, goblint/analyzer#1761). * Optimize affine equalities analysis using sparse matrices (goblint/analyzer#1459, goblint/analyzer#1625). * Prepare for parallelism (goblint/analyzer#1708, goblint/analyzer#1744, goblint/analyzer#1748, goblint/analyzer#1781, goblint/analyzer#1790). --- packages/goblint/goblint.2.6.0/opam | 123 ++++++++++++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 packages/goblint/goblint.2.6.0/opam diff --git a/packages/goblint/goblint.2.6.0/opam b/packages/goblint/goblint.2.6.0/opam new file mode 100644 index 00000000000..1d128034ac5 --- /dev/null +++ b/packages/goblint/goblint.2.6.0/opam @@ -0,0 +1,123 @@ +opam-version: "2.0" +synopsis: "Static analysis framework for C" +description: """ +Goblint is a sound static analysis framework for C programs using abstract interpretation. +It specializes in thread-modular verification of multi-threaded programs, especially regarding data races. +Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses. +""" +maintainer: [ + "Simmo Saan " + "Michael Schwarz " + "Karoliine Holter " +] +authors: [ + "Simmo Saan" + "Michael Schwarz" + "Julian Erhard" + "Sarah Tilscher" + "Karoliine Holter" + "Ralf Vogler" + "Kalmer Apinis" + "Vesal Vojdani" +] +license: "MIT" +tags: [ + "program analysis" + "program verification" + "static analysis" + "abstract interpretation" + "C" + "data race analysis" + "concurrency" +] +homepage: "https://goblint.in.tum.de" +doc: "https://goblint.readthedocs.io/en/latest/" +bug-reports: "https://github.com/goblint/analyzer/issues" +depends: [ + "dune" {>= "3.13"} + "ocaml" {>= "4.14"} + "goblint-cil" {>= "2.0.7"} + "batteries" {>= "3.9.0"} + "zarith" {>= "1.10"} + "yojson" {>= "2.0.0" & < "3"} + "qcheck-core" {>= "0.19"} + "ppx_deriving" {>= "6.0.2"} + "ppx_deriving_hash" {>= "0.1.2"} + "ppx_deriving_yojson" {>= "3.7.0"} + "ppx_blob" {>= "0.8.0"} + "ppxlib" {>= "0.30.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" {>= "0.2.1"} + "yaml" {>= "3.0.0"} + "uuidm" + "catapult" + "catapult-file" + "conf-gmp" {>= "3"} + "conf-ruby" {with-test} + "benchmark" {with-test} + "conf-gcc" + "domain-local-await" + "domain_shims" +] +depopts: ["apron" "z3" "domainslib"] +conflicts: [ + "result" {< "1.5"} + "apron" {< "v0.9.15"} + "camlidl" {< "1.13"} + "ez-conf-lib" {= "1"} +] +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-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") +# pin-depends: [ + # published goblint-cil 2.0.7 is currently up-to-date, so no pin needed + # [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ] + # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release + # [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] +# ] +depexts: [ + ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} # doesn't work (https://github.com/ocaml/opam/issues/5836) +] +post-messages: [ + "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} +] +x-ci-accept-failures: [ + "macos-homebrew" # newer MacOS headers cannot be parsed (https://github.com/ocaml/opam-repository/pull/26307#issuecomment-2258080206) + "opensuse-tumbleweed" # not GNU diff, so some cram tests fail (https://discuss.ocaml.org/t/opensuse-and-opam-tests/14641/2) +] +url { + src: + "https://github.com/goblint/analyzer/releases/download/v2.6.0/goblint-2.6.0.tbz" + checksum: [ + "sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41" + "sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71" + ] +} +x-commit-hash: "9c6a2462792b3e947b4c4fd1836fea500d5ce46a"