add Frama-C

packages/frama-c/frama-c.24.0/opam

+opam-version: "2.0"
+name: "frama-c"
+synopsis: "Platform dedicated to the analysis of source code written in C"
+version: "24.0"
+description:"""
+Frama-C gathers several analysis techniques in a single collaborative
+framework, based on analyzers (called "plug-ins") that can build upon the
+results computed by other analyzers in the framework.
+Thanks to this approach, Frama-C provides sophisticated tools, including:
+- an analyzer based on abstract interpretation (Eva plug-in);
+- a program proof framework based on weakest precondition calculus (WP plug-in);
+- a program slicer (Slicing plug-in);
+- a tool for verification of temporal (LTL) properties (Aoraï plug-in);
+- a runtime verification tool (E-ACSL plug-in);
+- several tools for code base exploration and dependency analysis
+  (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.).
+These plug-ins communicate between each other via the Frama-C API
+and via ACSL (ANSI/ISO C Specification Language) properties.
+"""
+maintainer: "francois.bobot@cea.fr"
+authors: [
+  "Michele Alberti"
+  "Thibaud Antignac"
+  "Gergö Barany"
+  "Patrick Baudin"
+  "Thibaut Benjamin"
+  "Allan Blanchard"
+  "Lionel Blatter"
+  "François Bobot"
+  "Richard Bonichon"
+  "Quentin Bouillaguet"
+  "David Bühler"
+  "Zakaria Chihani"
+  "Loïc Correnson"
+  "Julien Crétin"
+  "Pascal Cuoq"
+  "Zaynah Dargaye"
+  "Basile Desloges"
+  "Jean-Christophe Filliâtre"
+  "Philippe Herrmann"
+  "Maxime Jacquemin"
+  "Florent Kirchner"
+  "Tristan Le Gall"
+  "Jean-Christophe Léchenet"
+  "Matthieu Lemerre"
+  "Dara Ly"
+  "David Maison"
+  "Claude Marché"
+  "André Maroneze"
+  "Thibault Martin"
+  "Fonenantsoa Maurica"
+  "Melody Méaulle"
+  "Benjamin Monate"
+  "Yannick Moy"
+  "Anne Pacalet"
+  "Valentin Perrelle"
+  "Guillaume Petiot"
+  "Dario Pinto"
+  "Virgile Prevosto"
+  "Armand Puccetti"
+  "Félix Ridoux"
+  "Virgile Robles"
+  "Muriel Roger"
+  "Julien Signoles"
+  "Kostyantyn Vorobyov"
+  "Boris Yakobowski"
+]
+homepage: "https://frama-c.com/"
+license: "LGPL-2.1-only"
+dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
+doc: "http://frama-c.com/download/user-manual-24.0-beta-Chromium.pdf"
+bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
+tags: [
+  "deductive"
+  "program verification"
+  "formal specification"
+  "automated theorem prover"
+  "interactive theorem prover"
+  "C"
+  "plugins"
+  "abstract interpretation"
+  "slicing"
+  "weakest precondition"
+  "ACSL"
+  "dataflow analysis"
+  "runtime verification"
+]
+
+build: [
+  ["autoconf"] {dev}
+  ["./configure" "--prefix" prefix
+                 "--mandir=%{man}%"
+  ]
+  [make "-j%{jobs}%"]
+  [make "-C" "doc" "download"] {with-doc}
+]
+
+install: [
+  [make "install"]
+  [make "-C" "doc" "install"] {with-doc}
+]
+
+run-test: [
+  [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
+  # tests are disabled on PPC64 due to floating-point oracle differences
+  # (some ULPs in libc trigonometric functions) and due to the lack of
+  # available hardware to test them locally
+]
+
+# Please keep depends and depopts sorted by package name
+depends: [
+  "conf-autoconf" { build }
+  ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
+      & ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
+    | ( "lablgtk3" { >= "3.1.0" & os!="macos" }
+        & "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
+  ( "alt-ergo-free" | "alt-ergo" )
+  "conf-graphviz" { post }
+  "conf-time" { with-test }
+  "ocaml" { >= "4.08.1" }
+  "ocamlfind" # needed beyond build stage, used by -load-module
+  "ocamlgraph" { >= "1.8.8" }
+  "why3" { >= "1.4.0" & < "1.5~" }
+  "yojson" {>= "1.6.0"}
+  "zarith" {>= "1.5"}
+]
+
+depopts: [
+  # cannot use {build}: Frama-C must be recompiled when Coq and libraries changes.
+  # Coq: because .vo would would not be loadable by another version of Coq
+  # libraries: because we use dynamic linking
+  "apron"
+  "coq"
+  "mlgmpidl"
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "zmq"
+]
+
+post-messages: [
+  "Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect"
+]
+
+url {
+  src: "https://gitlab.isae-supaero.fr/lustrec/frama-c/-/archive/24.0-tacinstance-fix/frama-c-24.0-tacinstance-fix.tar.gz"
+  checksum: "md5=3566a8df42f5244f91a58a3adf236bc4"
+}