this repo has no description
anil.recoil.org
1opam-version: "2.0"
2available: opam-version >= "2.1.0"
3flags: avoid-version
4
5synopsis: "Platform dedicated to the analysis of source code written in C"
6description:"""
7Frama-C gathers several analysis techniques in a single collaborative
8framework, based on analyzers (called "plug-ins") that can build upon the
9results computed by other analyzers in the framework.
10Thanks to this approach, Frama-C provides sophisticated tools, including:
11- an analyzer based on abstract interpretation (Eva plug-in);
12- a program proof framework based on weakest precondition calculus (WP plug-in);
13- a program slicer (Slicing plug-in);
14- a tool for verification of temporal (LTL) properties (Aoraï plug-in);
15- a runtime verification tool (E-ACSL plug-in);
16- several tools for code base exploration and dependency analysis
17 (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.).
18These plug-ins communicate between each other via the Frama-C API
19and via ACSL (ANSI/ISO C Specification Language) properties.
20"""
21maintainer: "francois.bobot@cea.fr"
22authors: [
23 "Michele Alberti"
24 "Thibaud Antignac"
25 "Gergö Barany"
26 "Patrick Baudin"
27 "Thibaut Benjamin"
28 "Allan Blanchard"
29 "Lionel Blatter"
30 "François Bobot"
31 "Richard Bonichon"
32 "Quentin Bouillaguet"
33 "David Bühler"
34 "Zakaria Chihani"
35 "Loïc Correnson"
36 "Julien Crétin"
37 "Pascal Cuoq"
38 "Zaynah Dargaye"
39 "Basile Desloges"
40 "Jean-Christophe Filliâtre"
41 "Philippe Herrmann"
42 "Maxime Jacquemin"
43 "Florent Kirchner"
44 "Tristan Le Gall"
45 "Jean-Christophe Léchenet"
46 "Matthieu Lemerre"
47 "Dara Ly"
48 "David Maison"
49 "Claude Marché"
50 "André Maroneze"
51 "Thibault Martin"
52 "Fonenantsoa Maurica"
53 "Melody Méaulle"
54 "Benjamin Monate"
55 "Yannick Moy"
56 "Anne Pacalet"
57 "Valentin Perrelle"
58 "Guillaume Petiot"
59 "Dario Pinto"
60 "Virgile Prevosto"
61 "Armand Puccetti"
62 "Félix Ridoux"
63 "Virgile Robles"
64 "Muriel Roger"
65 "Julien Signoles"
66 "Kostyantyn Vorobyov"
67 "Boris Yakobowski"
68]
69homepage: "https://frama-c.com/"
70license: "LGPL-2.1-only"
71dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
72doc: "http://frama-c.com/download/user-manual-26.0-beta-Iron.pdf"
73bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
74tags: [
75 "deductive"
76 "program verification"
77 "formal specification"
78 "automated theorem prover"
79 "interactive theorem prover"
80 "C"
81 "plugins"
82 "abstract interpretation"
83 "slicing"
84 "weakest precondition"
85 "ACSL"
86 "dataflow analysis"
87 "runtime verification"
88]
89
90build: [
91 ["dune" "build" "-j%{jobs}%" "-p" name "--promote-install-files=false" "@install"]
92 [make "-C" "doc" "download"] {with-doc}
93]
94
95install: [
96 [make "PREFIX=%{prefix}%" "MANDIR=%{mandir}%" "install"]
97 [make "PREFIX=%{prefix}%" "-C" "doc" "install"] {with-doc}
98]
99
100remove: [
101 [make "PREFIX=%{prefix}%" "-f" "ivette/Makefile.installation" "uninstall"]
102]
103
104run-test: [
105 ["dune" "exec" "--" "frama-c-ptests" "tests" "src/plugins/*/tests"
106 ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" & os != "macos" }
107 ["dune" "build" "-j%{jobs}%" "@ptests_config"
108 ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" & os != "macos" }
109]
110
111depends: [
112 "dune" { (>= "3.2.0" & os!="macos") | (>= "3.5.0" & os="macos") }
113 "dune-configurator"
114 "dune-private-libs"
115 "dune-site" { >= "3.2.0" }
116
117 ( "alt-ergo-free" | "alt-ergo" )
118 "conf-graphviz" { post }
119 "conf-time" { with-test }
120 "ocaml" {>= "4.11.1" & < "5.3"}
121 "ocamlfind" # needed beyond build stage, used by -load-module
122 "ocamlgraph" { >= "1.8.8" }
123 "ocamlgraph" { with-test & < "2.1.0" }
124 "why3" {>= "1.5.1" & < "1.6~"}
125 "yojson" {>= "1.6.0" & < "2.1.0" & ( < "2.0.0" | ! with-test)}
126 "zarith" { >= "1.5" }
127
128 # PPXs
129 "ppx_deriving"
130 "ppx_deriving_yojson"
131 "ppx_import"
132
133 # This is hackish but will hopefully work until we remove GTK from Frama-C
134 # GTK 2 for macos only
135 "lablgtk" { >= "2.18.8" & os="macos" }
136 "conf-gnomecanvas" { os="macos" }
137 "conf-gtksourceview" { os="macos" }
138 ("ocamlgraph" { < "2.0" & os="macos" } | "ocamlgraph_gtk" { os="macos" })
139 # GTK3 for non-macos only
140 "lablgtk3" { >= "3.1.0" & os!="macos" }
141 "lablgtk3-sourceview3" { os!="macos" }
142 "conf-gtksourceview3" { os!="macos" }
143]
144
145depopts: [
146 # cannot use {build}: Frama-C must be recompiled when Coq and libraries changes.
147 # Coq: because .vo would would not be loadable by another version of Coq
148 # libraries: because we use dynamic linking
149 "apron"
150 "coq"
151 "mlmpfr"
152 "zmq"
153]
154
155conflicts: [
156 "cairo2" { < "0.6.2" }
157 "mlmpfr" { < "4.1.0-bugfix2" }
158 "pilat" { <= "1.6" }
159 "result" { < "1.5" }
160]
161
162post-messages: [
163"The Frama-C/WP plug-in requires one or more external prover(s).
164Recommended provers are:
165- Alt-Ergo (https://alt-ergo.ocamlpro.com)
166- CVC4 (https://cvc4.github.io)
167- Z3 (https://github.com/Z3Prover/z3)
168Use 'why3 config detect' to configure new provers.
169 "
170"Ivette is a new GUI for Frama-C, currently in development.
171Run 'ivette' once to finalize installation (requires an internet connection).
172Once finalized, 'ivette' will work offline.
173Finalization also requires Node v16 and Yarn:
174- install NVM (https://github.com/nvm-sh/nvm)
175- run 'nvm use 16'
176- run 'npm install --global yarn'"
177]
178
179url {
180 src: "https://www.frama-c.com/download/frama-c-26.0-beta-Iron.tar.gz"
181 checksum: "sha256=d4cce05ab46d66a10664fc3432181b9cbb2edc32a759ce280541c719135ca7e7"
182}