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 +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 { };