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