diff --git a/frama-c.opam b/frama-c.opam deleted file mode 100644 index d988d4431d4eba5cc5ee0b5afc2ad9b47e521f2d..0000000000000000000000000000000000000000 --- a/frama-c.opam +++ /dev/null @@ -1,118 +0,0 @@ -opam-version: "1.2" -name: "frama-c-base" -version: "20170501" -maintainer: "francois.bobot@cea.fr" -authors: [ - "Michele Alberti" - "Gergö Barany" - "Patrick Baudin" - "François Bobot" - "Richard Bonichon" - "David Bühler" - "Loïc Correnson" - "Julien Crétin" - "Pascal Cuoq" - "Zaynah Dargaye" - "Jean-Christophe Filliâtre" - "Philippe Herrmann" - "Florent Kirchner" - "Tristan Le Gall" - "Jean-Christophe Léchenet" - "Matthieu Lemerre" - "David Maison" - "Claude Marché" - "André Maroneze" - "Benjamin Monate" - "Yannick Moy" - "Anne Pacalet" - "Valentin Perrelle" - "Guillaume Petiot" - "Virgile Prevosto" - "Armand Puccetti" - "Muriel Roger" - "Julien Signoles" - "Kostyantyn Vorobyov" - "Boris Yakobowski" -] -homepage: "http://frama-c.com/" -license: "GNU Lesser General Public License version 2.1" -dev-repo: "https://github.com/Frama-C/Frama-C-snapshot.git" -doc: ["http://frama-c.com/download/user-manual-Phosphorus-20170501.pdf"] -bug-reports: "https://bts.frama-c.com/" -tags: [ - "deductive" - "program verification" - "formal specification" - "automated theorem prover" - "interactive theorem prover" - "C" - "plugins" - "abstract interpretation" - "slicing" - "weakest precondition" - "ACSL" - "dataflow analysis" -] - -build: [ - ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode, - # the configure *cannot* yet be - # generated - ["./configure" "--prefix" prefix - "--disable-gui" { !conf-gtksourceview:installed | - !conf-gnomecanvas:installed } -] - [make "-j%{jobs}%"] -] - -install: [ - [make "install"] -] - -remove: [ - ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode, - # the configure *cannot* yet be - # generated - ["./configure" "--prefix" prefix - "--disable-gui" { !conf-gtksourceview:installed | - !conf-gnomecanvas:installed } -] - [make "uninstall"] - ["rm" "-rf" frama-c-base:doc] -] - -build-doc: [ - [make "-C" "doc" "download"] - [make "-C" "doc" "FRAMAC_DOCDIR=%{frama-c-base:doc}%" "install"] -] - -build-test: [ - [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] -] - -depends: [ - "ocamlgraph" { >= "1.8.5" & < "1.9~" } - "ocamlfind" - "zarith" -] - -depopts: [ - "lablgtk" - "conf-gtksourceview" - "conf-gnomecanvas" - "coq" { build } - "why3" { build } -] - -messages: [ - "Why3 can be used by the WP plug-in for running additional automatic solvers" { !why3:installed } - "Coq can be used with the WP plug-in for proving interactively proof obligations" { !coq:installed } -] - -conflicts: [ - "why3-base" { < "0.86" } #for WP plug-in - "coq" { < "8.4.6" } #for WP plug-in - "lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1 -] - -available: [ ocaml-version >= "4.02.3" ]