pyrox.dev
lol
1{ stdenv, lib, fetchurl
2, coq, ocaml, findlib, menhir, zarith
3, tools ? stdenv.cc
4}:
5
6assert lib.versionAtLeast ocaml.version "4.02";
7
8stdenv.mkDerivation rec {
9 name = "verasco-1.3";
10 src = fetchurl {
11 url = "http://compcert.inria.fr/verasco/release/${name}.tgz";
12 sha256 = "0zvljrpwnv443k939zlw1f7ijwx18nhnpr8jl3f01jc5v66hr2k8";
13 };
14
15 buildInputs = [ coq ocaml findlib menhir zarith ];
16
17 preConfigure = ''
18 substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
19 '';
20
21 configureFlags = [
22 "-toolprefix ${tools}/bin/"
23 (if stdenv.isDarwin then "ia32-macosx" else "ia32-linux")
24 ];
25
26 prefixKey = "-prefix ";
27
28 enableParallelBuilding = true;
29 buildFlags = "proof extraction ccheck";
30
31 installPhase = ''
32 mkdir -p $out/bin
33 cp ccheck $out/bin/
34 ln -s $out/bin/ccheck $out/bin/verasco
35 if [ -e verasco.ini ]
36 then
37 mkdir -p $out/share
38 cp verasco.ini $out/share/
39 fi
40 mkdir -p $out/lib/compcert
41 cp -riv runtime/include $out/lib/compcert
42 '';
43
44 meta = {
45 homepage = http://compcert.inria.fr/verasco/;
46 description = "A static analyzer for the CompCert subset of ISO C 1999";
47 maintainers = with stdenv.lib.maintainers; [ vbgl ];
48 license = stdenv.lib.licenses.unfree;
49 platforms = with stdenv.lib.platforms; darwin ++ linux;
50 };
51}