3 files changed, 60 insertions, 4 deletions
diff --git a/pkgs/development/tools/analysis/cppcheck/default.nix b/pkgs/development/tools/analysis/cppcheck/default.nix
index 5955f34b58e9..e89d8c113a16 100644
--- a/pkgs/development/tools/analysis/cppcheck/default.nix
+++ b/pkgs/development/tools/analysis/cppcheck/default.nix
@@ -12,7 +12,7 @@ stdenv.mkDerivation rec {
     sha256 = "085lm8v7biixy6rykq836gfy91jcccpz9qpk8i9x339dzy2b2q4l";
   };
 
-  buildInputs = [ libxslt docbook_xsl docbook_xml_dtd_45 ];
+  nativeBuildInputs = [ libxslt docbook_xsl docbook_xml_dtd_45 ];
 
   makeFlags = ''PREFIX=$(out) CFGDIR=$(out)/cfg'';
 
diff --git a/pkgs/development/tools/analysis/spin/default.nix b/pkgs/development/tools/analysis/spin/default.nix
index 29559bf8b0ef..ab9954735f35 100644
--- a/pkgs/development/tools/analysis/spin/default.nix
+++ b/pkgs/development/tools/analysis/spin/default.nix
@@ -1,6 +1,9 @@
-{stdenv, fetchurl, yacc }:
+{ stdenv, fetchurl, makeWrapper, yacc, gcc }:
 
-stdenv.mkDerivation rec {
+let
+  binPath = stdenv.lib.makeBinPath [ gcc ];
+
+in stdenv.mkDerivation rec {
   name = "spin-${version}";
   version = "6.4.5";
   url-version = stdenv.lib.replaceChars ["."] [""] version;
@@ -13,11 +16,16 @@ stdenv.mkDerivation rec {
     sha256 = "0x8qnwm2xa8f176c52mzpvnfzglxs6xgig7bcgvrvkb3xf114224";
   };
 
+  nativeBuildInputs = [ makeWrapper ];
   buildInputs = [ yacc ];
 
   sourceRoot = "Spin/Src${version}";
 
-  installPhase = "install -D spin $out/bin/spin";
+  installPhase = ''
+    install -D spin $out/bin/spin
+    wrapProgram $out/bin/spin \
+      --prefix PATH : ${binPath}
+  '';
 
   meta = with stdenv.lib; {
     description = "Formal verification tool for distributed software systems";
diff --git a/pkgs/development/tools/analysis/verasco/default.nix b/pkgs/development/tools/analysis/verasco/default.nix
new file mode 100644
index 000000000000..9b3ff8e570d6
--- /dev/null
+++ b/pkgs/development/tools/analysis/verasco/default.nix
@@ -0,0 +1,48 @@
+{ stdenv, fetchurl, coq, ocamlPackages
+, tools ? stdenv.cc
+}:
+
+stdenv.mkDerivation rec {
+  name = "verasco-1.3";
+  src = fetchurl {
+    url = "http://compcert.inria.fr/verasco/release/${name}.tgz";
+    sha256 = "0zvljrpwnv443k939zlw1f7ijwx18nhnpr8jl3f01jc5v66hr2k8";
+  };
+
+  buildInputs = [ coq ] ++ (with ocamlPackages; [ ocaml findlib menhir zarith ]);
+
+  preConfigure = ''
+    substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
+  '';
+
+  configureFlags = [
+    "-toolprefix ${tools}/bin/"
+    (if stdenv.isDarwin then "ia32-macosx" else "ia32-linux")
+  ];
+
+  prefixKey = "-prefix ";
+
+  enableParallelBuilding = true;
+  buildFlags = "proof extraction ccheck";
+
+  installPhase = ''
+    mkdir -p $out/bin
+    cp ccheck $out/bin/
+    ln -s $out/bin/ccheck $out/bin/verasco
+    if [ -e verasco.ini ]
+    then
+      mkdir -p $out/share
+      cp verasco.ini $out/share/
+    fi
+    mkdir -p $out/lib/compcert
+    cp -riv runtime/include $out/lib/compcert
+  '';
+
+  meta = {
+    homepage = http://compcert.inria.fr/verasco/;
+    description = "A static analyzer for the CompCert subset of ISO C 1999";
+    maintainers = with stdenv.lib.maintainers; [ vbgl ];
+    license = stdenv.lib.licenses.unfree;
+    platforms = with stdenv.lib.platforms; darwin ++ linux;
+  };
+}