frama-c: add version 20111001

3 files changed, 106 insertions, 2 deletions

diff --git a/pkgs/development/tools/misc/frama-c/0007-Port-to-OCamlgraph-1.8.2.patch b/pkgs/development/tools/misc/frama-c/0007-Port-to-OCamlgraph-1.8.2.patch
new file mode 100644
index 00000000000..1c16e1794ab
--- /dev/null
+++ b/pkgs/development/tools/misc/frama-c/0007-Port-to-OCamlgraph-1.8.2.patch
@@ -0,0 +1,64 @@
+From: Mehdi Dogguy <mehdi@debian.org>
+Date: Wed, 16 May 2012 14:48:40 +0200
+Subject: Port to OCamlgraph 1.8.2
+
+ o Graph.Topological: as of OCamlgraph 1.8.2, the input graph must
+   implement Sig.COMPARABLE instead of Sig.HASHABLE
+---
+ src/misc/service_graph.ml           |    2 +-
+ src/misc/service_graph.mli          |    2 +-
+ src/semantic_callgraph/register.ml  |    1 +
+ src/syntactic_callgraph/register.ml |    1 +
+ 4 files changed, 4 insertions(+), 2 deletions(-)
+
+diff --git a/src/misc/service_graph.ml b/src/misc/service_graph.ml
+index f30a1be..567698f 100644
+--- a/src/misc/service_graph.ml
++++ b/src/misc/service_graph.ml
+@@ -24,7 +24,7 @@ module Make
+   (G: sig
+      type t
+      module V: sig
+-       include Graph.Sig.HASHABLE
++       include Graph.Sig.COMPARABLE
+        val id: t -> int
+        val name: t -> string
+        val attributes: t -> Graph.Graphviz.DotAttributes.vertex list
+diff --git a/src/misc/service_graph.mli b/src/misc/service_graph.mli
+index 5ebb570..8006977 100644
+--- a/src/misc/service_graph.mli
++++ b/src/misc/service_graph.mli
+@@ -28,7 +28,7 @@ module Make
+   (G: sig
+      type t
+      module V: sig
+-       include Graph.Sig.HASHABLE
++       include Graph.Sig.COMPARABLE
+        val id: t -> int
+          (** assume is >= 0 and unique for each vertices of the graph *)
+        val name: t -> string
+diff --git a/src/semantic_callgraph/register.ml b/src/semantic_callgraph/register.ml
+index 0b3b4df..064dca8 100644
+--- a/src/semantic_callgraph/register.ml
++++ b/src/semantic_callgraph/register.ml
+@@ -107,6 +107,7 @@ module Service =
+                (if Kernel_function.is_definition v then `Bold
+                 else `Dotted) ]
+          let equal = Kernel_function.equal
++         let compare v1 v2 = Datatype.Int.compare (id v1) (id v2)
+          let hash = Kernel_function.hash
+          let entry_point () =
+            try Some (fst (Globals.entry_point ()))
+diff --git a/src/syntactic_callgraph/register.ml b/src/syntactic_callgraph/register.ml
+index 4efb594..d9d78b9 100644
+--- a/src/syntactic_callgraph/register.ml
++++ b/src/syntactic_callgraph/register.ml
+@@ -41,6 +41,7 @@ module Service =
+              | NIVar (_,b) when not !b -> `Style `Dotted
+              | _ -> `Style `Bold ]
+          let equal v1 v2 = id v1 = id v2
++         let compare v1 v2 = Datatype.Int.compare (id v1) (id v2)
+          let hash = id
+          let entry_point () = !entry_point_ref
+        end
+-- 
diff --git a/pkgs/development/tools/misc/frama-c/default.nix b/pkgs/development/tools/misc/frama-c/default.nix
index 2f597d29c75..ede316b4b7b 100644
--- a/pkgs/development/tools/misc/frama-c/default.nix
+++ b/pkgs/development/tools/misc/frama-c/default.nix
@@ -1,4 +1,12 @@
-{ stdenv, fetchurl, ocamlPackages }:
+# Note on a potential dependency-bloat:
+# Frama-c ships with several plugins that have dependencies on other
+# software. Not providing the dependencies has as effect that certain
+# plugins will not be available.
+# I've included the dependencies that are well-supported by nixpkgs
+# and seem useful in general. Not included are:
+#   alt-ergo, ltl2ba, otags, why-dp
+
+{ stdenv, fetchurl, ncurses, ocamlPackages, coq, graphviz }:
 
 let
 
@@ -14,9 +22,39 @@ in stdenv.mkDerivation {
   };
 
   buildInputs = with ocamlPackages; [
-    ocaml findlib
+    ncurses ocaml findlib ocamlgraph
+    lablgtk coq graphviz  # optional dependencies
+  ];
+
+  patches = [
+    # this patch comes from the debian frama-c package, and was
+    # posted on the frama-c issue tracker.
+    ./0007-Port-to-OCamlgraph-1.8.2.patch
   ];
 
+  postPatch = ''
+    # strip absolute paths to /usr/bin
+    for file in ./configure ./share/Makefile.common ./src/*/configure; do
+      substituteInPlace $file  --replace '/usr/bin/' ""
+    done
+
+    # find library paths
+    OCAMLGRAPH_HOME=`ocamlfind query ocamlgraph`
+    LABLGTK_HOME=`ocamlfind query lablgtk2`
+
+    # patch search paths
+    # ensure that the tests against the ocamlgraph version succeeds
+    # filter out the additional search paths from ocamldep
+    substituteInPlace ./configure \
+      --replace '$OCAMLLIB/ocamlgraph' "$OCAMLGRAPH_HOME" \
+      --replace '$OCAMLLIB/lablgtk2' "$LABLGTK_HOME" \
+      --replace '+ocamlgraph' "$OCAMLGRAPH_HOME" \
+      --replace '1.8)' '*)'
+    substituteInPlace ./Makefile --replace '+lablgtk2' "$LABLGTK_HOME" \
+      --replace '$(patsubst +%,.,$(INCLUDES) $(GUI_INCLUDES))' \
+                '$(patsubst /%,.,$(patsubst +%,.,$(INCLUDES) $(GUI_INCLUDES)))'
+  '';
+
   meta = {
     description = "Frama-C is an extensible tool for source-code analysis of C software";
 
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 0c127b49d34..ad80feb1272 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -2964,6 +2964,8 @@ let
 
   coccinelle = callPackage ../development/tools/misc/coccinelle { };
 
+  framac = callPackage ../development/tools/misc/frama-c { };
+
   cppi = callPackage ../development/tools/misc/cppi { };
 
   cproto = callPackage ../development/tools/misc/cproto { };