From 38186e23127875d070d4ea38871f360657f6541b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 14:49:19 +0300 Subject: [PATCH] [new release] goblint (2.4.0) CHANGES: * Remove unmaintained analyses: spec, file (goblint/analyzer#1281). * Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466). * Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439). * Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399). * Add NULL byte array domain (goblint/analyzer#1076). * Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511). * Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409). * Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458). * Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510). * Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407). * Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543). * Extract automatic configuration tuning for soundness (goblint/analyzer#1369). * Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403). * Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497). * Refactor logging (goblint/analyzer#1117). * Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487). * Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448). --- packages/goblint/goblint.2.4.0/opam | 114 ++++++++++++++++++++++++++++ 1 file changed, 114 insertions(+) create mode 100644 packages/goblint/goblint.2.4.0/opam diff --git a/packages/goblint/goblint.2.4.0/opam b/packages/goblint/goblint.2.4.0/opam new file mode 100644 index 00000000000..3a0edfb751d --- /dev/null +++ b/packages/goblint/goblint.2.4.0/opam @@ -0,0 +1,114 @@ +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.7"} + "ocaml" {>= "4.14"} + "goblint-cil" {>= "2.0.4"} + "batteries" {>= "3.5.1"} + "zarith" {>= "1.10"} + "yojson" {>= "2.0.0"} + "qcheck-core" {>= "0.19"} + "ppx_deriving" {>= "6.0.2"} + "ppx_deriving_hash" {>= "0.1.2"} + "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" {>= "v0.9.15"} + "z3" +] +conflicts: [ + "result" {< "1.5"} + "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" +# 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} +] +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.4.0/goblint-2.4.0.tbz" + checksum: [ + "sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6" + "sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af" + ] +} +x-commit-hash: "b129fab7de3ab5fd85d2f1340b2d9c5a4e4e2653"