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>
This commit is contained in:
Austin Seipp 2014-05-01 02:30:12 -05:00
parent 6d52463bd3
commit 628e914f2b

View File

@ -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 {
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;
license = stdenv.lib.licenses.lgpl21;
maintainers = with stdenv.lib.maintainers; [ thoughtpolice amiddelk ];
platforms = stdenv.lib.platforms.linux;
};
}