From d14d61fbae157ff713e7c29327361a8462f3c1a7 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Aug 27 2012 22:15:15 +0000 Subject: Use a vastly simpler patch for OCaml 4 that fixes the native build. --- diff --git a/frama-c-ocaml4.patch b/frama-c-ocaml4.patch index 779491a..4083fb1 100644 --- a/frama-c-ocaml4.patch +++ b/frama-c-ocaml4.patch @@ -1,111 +1,42 @@ ---- ./src/type/datatype.mli.orig 2011-10-10 02:38:09.000000000 -0600 -+++ ./src/type/datatype.mli 2012-07-30 15:57:27.983244802 -0600 -@@ -249,10 +249,27 @@ module type Map = sig - - end - -+module type Hashtbl_S = sig -+ type key -+ type 'a t -+ val create : int -> 'a t -+ val clear : 'a t -> unit -+ val copy : 'a t -> 'a t -+ val add : 'a t -> key -> 'a -> unit -+ val remove : 'a t -> key -> unit -+ val find : 'a t -> key -> 'a -+ val find_all : 'a t -> key -> 'a list -+ val replace : 'a t -> key -> 'a -> unit -+ val mem : 'a t -> key -> bool -+ val iter : (key -> 'a -> unit) -> 'a t -> unit -+ val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b -+ val length : 'a t -> int -+end +--- ./cil/ocamlutil/inthash.ml.orig 2011-10-10 02:40:09.000000000 -0600 ++++ ./cil/ocamlutil/inthash.ml 2012-08-27 15:09:37.694716225 -0600 +@@ -61,6 +61,12 @@ let clear h = + done; + h.size <- 0 + ++let reset h = ++ for i = 0 to Array.length h.data - 1 do ++ h.data.(i) <- Empty ++ done; ++ h.size <- 0 + - (** A standard OCaml hashtbl signature extended with datatype operations. *) - module type Hashtbl = sig - -- include Hashtbl.S -+ include Hashtbl_S - - val memo: 'a t -> key -> (key -> 'a) -> 'a - (** [memo tbl k f] returns the binding of [k] in [tbl]. If there is -@@ -468,7 +485,7 @@ module Set(S: Set.S)(E: S with type t = - module Map(M: Map_common_interface.S)(Key: S with type t = M.key)(Info: Functor_info) : - Map with type 'a t = 'a M.t and type key = M.key and module Key = Key - --module Hashtbl(H: Hashtbl.S)(Key: S with type t = H.key)(Info : Functor_info): -+module Hashtbl(H: Hashtbl_S)(Key: S with type t = H.key)(Info : Functor_info): - Hashtbl with type 'a t = 'a H.t and type key = H.key and module Key = Key - - module type Sub_caml_weak_hashtbl = sig ---- ./src/type/datatype.ml.orig 2011-10-10 02:38:09.000000000 -0600 -+++ ./src/type/datatype.ml 2012-07-30 16:02:06.952251779 -0600 -@@ -306,8 +306,25 @@ module type Map = sig - module Make(Data: S) : S with type t = Data.t t - end - -+module type Hashtbl_S = sig -+ type key -+ type 'a t -+ val create : int -> 'a t -+ val clear : 'a t -> unit -+ val copy : 'a t -> 'a t -+ val add : 'a t -> key -> 'a -> unit -+ val remove : 'a t -> key -> unit -+ val find : 'a t -> key -> 'a -+ val find_all : 'a t -> key -> 'a list -+ val replace : 'a t -> key -> 'a -> unit -+ val mem : 'a t -> key -> bool -+ val iter : (key -> 'a -> unit) -> 'a t -> unit -+ val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b -+ val length : 'a t -> int -+end + let copy h = + { size = h.size; + data = Array.copy h.data } +@@ -228,3 +234,7 @@ let memoize (h: 'a t) (key: int) (f: int + + let tolist (h: 'a t) : (int * 'a) list = + fold (fun k d acc -> (k, d) :: acc) h [] + - module type Hashtbl = sig -- include Hashtbl.S -+ include Hashtbl_S - val memo: 'a t -> key -> (key -> 'a) -> 'a - module Key: S with type t = key - module Make(Data: S) : S with type t = Data.t t -@@ -970,7 +987,7 @@ end - module Initial_caml_hashtbl = Hashtbl - - (* ocaml functors are generative *) --module Hashtbl(H: Hashtbl.S)(Key: S with type t = H.key)(Info : Functor_info) = -+module Hashtbl(H: Hashtbl_S)(Key: S with type t = H.key)(Info : Functor_info) = - struct - - let () = check Key.equal "equal" Key.name Info.module_name ---- ./src/wp/fol_formula.ml.orig 2011-10-10 02:38:21.000000000 -0600 -+++ ./src/wp/fol_formula.ml 2012-07-30 15:58:42.512246809 -0600 -@@ -389,7 +389,7 @@ let iter_all section f = - module type Identifiable = - sig - type t -- module H : Hashtbl.S -+ module H : Datatype.Hashtbl_S - val index : t -> H.key - val prefix : string - val basename : t -> string ---- ./src/wp/formula.mli.orig 2011-10-10 02:38:21.000000000 -0600 -+++ ./src/wp/formula.mli 2012-07-30 15:59:14.902247733 -0600 -@@ -147,7 +147,7 @@ sig - module type Identifiable = - sig - type t -- module H : Hashtbl.S -+ module H : Datatype.Hashtbl_S - val index : t -> H.key - val prefix : string - val basename : t -> string ---- ./src/wp/LogicId.mli.orig 2011-10-10 02:38:21.000000000 -0600 -+++ ./src/wp/LogicId.mli 2012-07-30 15:58:16.654245955 -0600 -@@ -40,7 +40,7 @@ val dummy : id (** Only usable for repre - - module Iset : Set.S with type elt = t - module Imap : Map.S with type key = t --module Ihmap : Hashtbl.S with type key = t -+module Ihmap : Datatype.Hashtbl_S with type key = t - - (** {3 Name Spaces} *) ++let stats h = ++ { Hashtbl.num_bindings = h.size; Hashtbl.num_buckets = Array.length h.data; ++ Hashtbl.max_bucket_length = 1; Hashtbl.bucket_histogram = Array.make 2 0 } +--- ./cil/ocamlutil/inthash.mli.orig 2011-10-10 02:40:09.000000000 -0600 ++++ ./cil/ocamlutil/inthash.mli 2012-08-27 14:54:00.594502979 -0600 +@@ -50,6 +50,7 @@ type 'a t + + val create: int -> 'a t + val clear: 'a t -> unit ++val reset: 'a t -> unit + val length : 'a t -> int + + val copy: 'a t -> 'a t +@@ -67,6 +68,8 @@ val find_all: 'a t -> int -> 'a list + val iter: (int -> 'a -> unit) -> 'a t -> unit + val fold: (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + ++val stats: 'a t -> Hashtbl.statistics ++ + val memoize: 'a t -> int -> (int -> 'a) -> 'a + val tolist: 'a t -> (int * 'a) list diff --git a/frama-c.spec b/frama-c.spec index 2cec4e4..d0abeb0 100644 --- a/frama-c.spec +++ b/frama-c.spec @@ -20,7 +20,7 @@ Name: frama-c Version: 1.7 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Framework for source code analysis of C software Group: Development/Libraries @@ -148,8 +148,12 @@ touch -r man/frama-c.1 man/frama-c.1.conv mv -f man/frama-c.1.conv man/frama-c.1 # Version 1.8 of ocamlgraph is good, therefore 1.8.X is good, too. -# Also adapt to OCaml 4.00.0. -sed -e 's|1\.8)|1.8*)|' -e 's/3\.1\*/3.1*|4*/' -i configure +# Also adapt to OCaml 4.00.0 and alt-ergo 0.94 +sed -e 's|1\.8)|1.8*)|' \ + -e 's/3\.1\*/3.1*|4*/' \ + -e 's/0\.92\.2/0.94/' \ + -i configure +sed -i 's/0\.92\.2/0.94/' src/wp/configure %build # This option prints the actual make commands so we can see what's @@ -255,6 +259,9 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \ %{_xemacs_sitelispdir}/acsl.el %changelog +* Mon Aug 27 2012 Jerry James - 1.7-8 +- Use a vastly simpler patch for OCaml 4 that fixes the native build. + * Fri Aug 3 2012 Jerry James - 1.7-7 - Shipping the bytecode version works better if it isn't stripped.