tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{ lib, stdenv, fetchurl, fetchpatch, makeWrapper, writeText
2, graphviz, doxygen
3, ocamlPackages, ltl2ba, coq, why3
4, gdk-pixbuf, wrapGAppsHook
5}:
6
7let why3_1_5 = why3.overrideAttrs (o: rec {
8 version = "1.5.1";
9 src = fetchurl {
10 url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
11 hash = "sha256-vNR7WeiSvg+763GcovoZBFDfncekJMeqNegP4fVw06I=";
12 };
13 }); in
14let why3 = why3_1_5; in
15
16let
17 mkocamlpath = p: "${p}/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib";
18 runtimeDeps = with ocamlPackages; [
19 apron.dev
20 bigarray-compat
21 biniou
22 camlzip
23 easy-format
24 menhirLib
25 mlgmpidl
26 num
27 ocamlgraph
28 ppx_deriving
29 ppx_deriving_yojson
30 ppx_import
31 stdlib-shims
32 why3
33 re
34 result
35 seq
36 sexplib
37 sexplib0
38 parsexp
39 base
40 yojson
41 zarith
42 ];
43 ocamlpath = lib.concatMapStringsSep ":" mkocamlpath runtimeDeps;
44in
45
46stdenv.mkDerivation rec {
47 pname = "frama-c";
48 version = "26.1";
49 slang = "Iron";
50
51 src = fetchurl {
52 url = "https://frama-c.com/download/frama-c-${version}-${slang}.tar.gz";
53 hash = "sha256-UT7ajIyu8e5vzrz2oBKDDrtZqUacgUP/TRi0/kz9Qkg=";
54 };
55
56 patches = [
57 (fetchpatch {
58 name = "fixes-yojson-2_1-support.patch";
59 url = "https://git.frama-c.com/pub/frama-c/-/commit/647eace02ed8dac46e75452898c3470f82576818.patch";
60 hash = "sha256-XfLi4kW1Y2MCLjHHQZAD8DvXvfZuDH3OKd9hlTV0XCw=";
61 })
62 ];
63
64 postConfigure = "patchShebangs src/plugins/eva/gen-api.sh";
65
66 strictDeps = true;
67
68 nativeBuildInputs = [ wrapGAppsHook ] ++ (with ocamlPackages; [ ocaml findlib dune_3 ]);
69
70 buildInputs = with ocamlPackages; [
71 dune-site dune-configurator
72 ltl2ba ocamlgraph yojson menhirLib camlzip
73 lablgtk3 lablgtk3-sourceview3 coq graphviz zarith apron why3 mlgmpidl doxygen
74 ppx_deriving ppx_import ppx_deriving_yojson
75 gdk-pixbuf
76 ];
77
78 buildPhase = ''
79 runHook preBuild
80 dune build -j$NIX_BUILD_CORES --release @install
81 runHook postBuild
82 '';
83
84 installFlags = [ "PREFIX=$(out)" ];
85
86 preFixup = ''
87 gappsWrapperArgs+=(--prefix OCAMLPATH ':' ${ocamlpath}:$out/lib/)
88 '';
89
90 # Allow loading of external Frama-C plugins
91 setupHook = writeText "setupHook.sh" ''
92 addFramaCPath () {
93 if test -d "''$1/lib/frama-c/plugins"; then
94 export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN-}''${FRAMAC_PLUGIN:+:}''$1/lib/frama-c/plugins"
95 export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}''$1/lib/frama-c/plugins"
96 fi
97
98 if test -d "''$1/lib/frama-c"; then
99 export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}''$1/lib/frama-c"
100 fi
101
102 if test -d "''$1/share/frama-c/"; then
103 export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE-}''${FRAMAC_EXTRA_SHARE:+:}''$1/share/frama-c"
104 fi
105
106 }
107
108 addEnvHooks "$targetOffset" addFramaCPath
109 '';
110
111
112 meta = {
113 description = "An extensible and collaborative platform dedicated to source-code analysis of C software";
114 homepage = "http://frama-c.com/";
115 license = lib.licenses.lgpl21;
116 maintainers = with lib.maintainers; [ thoughtpolice amiddelk ];
117 platforms = lib.platforms.unix;
118 };
119}