pkgs/development/tools/analysis/frama-c/default.nix

   1 { lib, stdenv, fetchurl, fetchpatch, makeWrapper, writeText
   2 , graphviz, doxygen
   3 , ocamlPackages, ltl2ba, coq, why3
   4 , gdk-pixbuf, wrapGAppsHook
   5 }:
   6
   7 let
   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;
  36 in
  37
  38 stdenv.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 = [ wrapGAppsHook ] ++ (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 }