diff options
author | Austin Seipp <aseipp@pobox.com> | 2014-05-01 02:30:12 -0500 |
---|---|---|
committer | Austin Seipp <aseipp@pobox.com> | 2014-05-01 02:42:34 -0500 |
commit | 628e914f2b59f7096c41780e373767f1a767147d (patch) | |
tree | 92b7c1ba739d8ca8296e0f85ffccca769fcb62e2 /pkgs/development/tools/misc/frama-c/default.nix | |
parent | 6d52463bd338ebe3bdb1aeed6b6557d219c37788 (diff) | |
download | nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar.gz nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar.bz2 nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar.lz nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar.xz nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.tar.zst nixpkgs-628e914f2b59f7096c41780e373767f1a767147d.zip |
frama-c: overhaul, upgrade to 20140301-Neon
This massively upgrades the frama-c package to be far more useful, including support for a lot more plugins, including Jessie. Jessie unfortunately requires that its plugin is installed alongside frama-c, so we install why2 (where it lives) along with frama-c now. This increases the size, but makes it much more useful. In the future, it may be possible to split out the build such that why2 is a separate expression and frama-c only installs the plugin, rather than all of why2. However, right now this is fine. Furthermore, why3 is now a dependency - the Jessie plugin can use either, and defaults to Why3 now. Per the design, Frama-C can also go from Why2->Why3 as well. We also make Coq and Alt-Ergo dependencies, so that out-of-the-box users get at least one SMT solver and a prover for support. Signed-off-by: Austin Seipp <aseipp@pobox.com>
Diffstat (limited to 'pkgs/development/tools/misc/frama-c/default.nix')
-rw-r--r-- | pkgs/development/tools/misc/frama-c/default.nix | 93 |
1 files changed, 61 insertions, 32 deletions
diff --git a/pkgs/development/tools/misc/frama-c/default.nix b/pkgs/development/tools/misc/frama-c/default.nix index ede316b4b7b..baa63855a0a 100644 --- a/pkgs/development/tools/misc/frama-c/default.nix +++ b/pkgs/development/tools/misc/frama-c/default.nix @@ -1,37 +1,53 @@ -# Note on a potential dependency-bloat: -# Frama-c ships with several plugins that have dependencies on other -# software. Not providing the dependencies has as effect that certain -# plugins will not be available. -# I've included the dependencies that are well-supported by nixpkgs -# and seem useful in general. Not included are: -# alt-ergo, ltl2ba, otags, why-dp +{ stdenv, fetchurl, ncurses, ocamlPackages, graphviz +, ltl2ba, coq, alt-ergo, gmp, why3 }: -{ stdenv, fetchurl, ncurses, ocamlPackages, coq, graphviz }: - -let - - version = "20111001"; - sha256 = "8afad848321c958fab265045cd152482e77ce7c175ee7c9af2d4bec57a1bc671"; - -in stdenv.mkDerivation { - name = "frama-c-${version}"; +stdenv.mkDerivation rec { + name = "frama-c-${version}"; + version = "20140301"; + slang = "Neon"; src = fetchurl { - url = "http://frama-c.com/download/frama-c-Nitrogen-${version}.tar.gz"; - inherit sha256; + url = "http://frama-c.com/download/frama-c-${slang}-${version}.tar.gz"; + sha256 = "0ca7ky7vs34did1j64v6d8gcp2irzw3rr5qgv47jhmidbipn1865"; + }; + + why2 = fetchurl { + url = "http://why.lri.fr/download/why-2.34.tar.gz"; + sha256 = "1335bhq9v3h46m8aba2c5myi9ghm87q41in0m15xvdrwq5big1jg"; }; buildInputs = with ocamlPackages; [ - ncurses ocaml findlib ocamlgraph - lablgtk coq graphviz # optional dependencies + ncurses ocaml findlib alt-ergo ltl2ba ocamlgraph gmp + lablgtk coq graphviz zarith why3 zarith ]; - patches = [ - # this patch comes from the debian frama-c package, and was - # posted on the frama-c issue tracker. - ./0007-Port-to-OCamlgraph-1.8.2.patch - ]; + enableParallelBuilding = true; + configureFlags = [ "--disable-local-ocamlgraph" ]; + + unpackPhase = '' + tar xf $src + tar xf $why2 + ''; + + buildPhase = '' + cd frama* + ./configure --prefix=$out + make -j$NIX_BUILD_CORES + make install + cd ../why* + FRAMAC=$out/bin/frama-c ./configure --prefix=$out + make + make install + ''; + + + # Taken from Debian Sid + # https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=746091 + patches = ./0004-Port-to-OCamlgraph-1.8.5.patch; + + # Enter frama-c directory before patching + prePatch = ''cd frama*''; postPatch = '' # strip absolute paths to /usr/bin for file in ./configure ./share/Makefile.common ./src/*/configure; do @@ -49,19 +65,32 @@ in stdenv.mkDerivation { --replace '$OCAMLLIB/ocamlgraph' "$OCAMLGRAPH_HOME" \ --replace '$OCAMLLIB/lablgtk2' "$LABLGTK_HOME" \ --replace '+ocamlgraph' "$OCAMLGRAPH_HOME" \ - --replace '1.8)' '*)' substituteInPlace ./Makefile --replace '+lablgtk2' "$LABLGTK_HOME" \ --replace '$(patsubst +%,.,$(INCLUDES) $(GUI_INCLUDES))' \ '$(patsubst /%,.,$(patsubst +%,.,$(INCLUDES) $(GUI_INCLUDES)))' + + substituteInPlace ./src/aorai/aorai_register.ml --replace '"ltl2ba' '"${ltl2ba}/bin/ltl2ba' + + cd ../why* + substituteInPlace ./frama-c-plugin/Makefile --replace 'shell frama-c' "shell $out/bin/frama-c" + substituteInPlace ./jc/jc_make.ml --replace ' why-dp ' " $out/bin/why-dp " + substituteInPlace ./jc/jc_make.ml --replace "?= why@\n" "?= $out/bin/why@\n" + substituteInPlace ./jc/jc_make.ml --replace ' gwhy-bin@' " $out/bin/gwhy-bin@" + substituteInPlace ./jc/jc_make.ml --replace ' why3 ' " ${why3}/bin/why3 " + substituteInPlace ./jc/jc_make.ml --replace ' why3ide ' " ${why3}/bin/why3ide " + substituteInPlace ./jc/jc_make.ml --replace ' why3replayer ' " ${why3}/bin/why3replayer " + substituteInPlace ./jc/jc_make.ml --replace ' why3ml ' " ${why3}/bin/why3ml " + substituteInPlace ./jc/jc_make.ml --replace ' coqdep@' " ${coq}/bin/coqdep@" + substituteInPlace ./jc/jc_make.ml --replace 'coqc' " ${coq}/bin/coqc" + substituteInPlace ./frama-c-plugin/register.ml --replace ' jessie ' " $out/bin/jessie " + cd .. ''; meta = { description = "Frama-C is an extensible tool for source-code analysis of C software"; - - homepage = http://frama-c.com/; - license = "GPLv2"; - - maintainers = [ stdenv.lib.maintainers.amiddelk ]; - platforms = stdenv.lib.platforms.gnu; + homepage = http://frama-c.com/; + license = stdenv.lib.licenses.lgpl21; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice amiddelk ]; + platforms = stdenv.lib.platforms.linux; }; } |