From a5f7ff08595681e0314063a6826e312f2c519dd9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 14 Feb 2019 17:29:04 +0100
Subject: [PATCH] [ocaml] improve compatibility with 4.08: Pervasives.compare
---
devel_tools/ocamldep_transitive_closure.ml | 2 +-
ptests/ptests.ml | 4 ++--
src/kernel_services/abstract_interp/abstract_interp.ml | 2 +-
src/kernel_services/abstract_interp/float_interval.ml | 2 +-
src/kernel_services/ast_data/alarms.ml | 8 ++++----
src/kernel_services/ast_data/property.ml | 2 +-
src/kernel_services/ast_data/property_status.ml | 2 +-
src/kernel_services/ast_printing/description.ml | 2 +-
src/kernel_services/ast_queries/cil_datatype.ml | 2 +-
src/kernel_services/ast_queries/file.ml | 2 +-
src/kernel_services/ast_queries/logic_typing.ml | 4 ++--
src/kernel_services/ast_queries/logic_utils.ml | 6 +++---
src/libraries/datatype/datatype.ml | 8 ++++----
src/libraries/stdlib/FCHashtbl.ml | 2 +-
src/libraries/stdlib/transitioning.ml.in | 6 ++++++
src/libraries/utils/bitvector.ml | 2 +-
src/libraries/utils/json.mll | 2 +-
src/libraries/utils/pretty_utils.ml | 7 +++++--
src/libraries/utils/pretty_utils.mli | 2 +-
src/libraries/utils/rgmap.ml | 2 +-
src/plugins/gui/pretty_source.ml | 4 ++--
src/plugins/gui/warning_manager.ml | 2 +-
src/plugins/metrics/metrics_base.ml | 2 +-
src/plugins/obfuscator/obfuscator_kind.ml | 2 +-
src/plugins/qed/export.ml | 2 +-
src/plugins/qed/intmap.ml | 4 ++--
src/plugins/qed/kind.ml | 2 +-
src/plugins/qed/pool.ml | 4 ++--
src/plugins/qed/term.ml | 4 ++--
src/plugins/report/classify.ml | 2 +-
src/plugins/report/csv.ml | 2 +-
src/plugins/value/alarmset.ml | 2 +-
src/plugins/value/domains/gauges/gauges_domain.ml | 2 +-
src/plugins/value/gui_files/gui_callstacks_manager.ml | 2 +-
src/plugins/value/gui_files/gui_red.ml | 2 +-
src/plugins/value/utils/structure.ml | 2 +-
src/plugins/value/utils/value_perf.ml | 2 +-
src/plugins/value/values/numerors/numerors_interval.ml | 2 +-
src/plugins/value/values/numerors/numerors_utils.ml | 2 +-
src/plugins/value/values/sign_value.ml | 2 +-
src/plugins/wp/CfgCompiler.ml | 2 +-
src/plugins/wp/Conditions.ml | 2 +-
src/plugins/wp/Cstring.ml | 2 +-
src/plugins/wp/Factory.ml | 2 +-
src/plugins/wp/LogicBuiltins.ml | 6 +++---
src/plugins/wp/MemTyped.ml | 2 +-
src/plugins/wp/ProverScript.ml | 2 +-
src/plugins/wp/ProverWhy3.ml | 2 +-
src/plugins/wp/Splitter.ml | 4 ++--
src/plugins/wp/StmtSemantics.ml | 2 +-
src/plugins/wp/Strategy.ml | 2 +-
src/plugins/wp/VCS.ml | 6 +++---
src/plugins/wp/Warning.ml | 2 +-
src/plugins/wp/ctypes.ml | 4 ++--
src/plugins/wp/proof.ml | 2 +-
src/plugins/wp/share/install.ml | 4 ++--
src/plugins/wp/wpPropId.ml | 4 ++--
57 files changed, 88 insertions(+), 79 deletions(-)
diff --git a/devel_tools/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml
index 3e3290c2246..c14aace6a12 100644
--- a/devel_tools/ocamldep_transitive_closure.ml
+++ b/devel_tools/ocamldep_transitive_closure.ml
@@ -7,7 +7,7 @@ let root = ref ""
module Dep_graph = Graph.Imperative.Digraph.Concrete(
struct
type t = string
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let hash = Hashtbl.hash
let equal = (=)
end)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index ef9497abebb..61d3b38decb 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -344,7 +344,7 @@ let () =
((Arg.align
(List.sort
(fun (optname1, _, _) (optname2, _, _) ->
- Pervasives.compare optname1 optname2
+ compare optname1 optname2
) argspec)
) @ ["", Arg.Unit (fun () -> ()), example_msg;])
make_test_suite umsg
@@ -1103,7 +1103,7 @@ module Make_Report(M:sig type t end)=struct
(struct
type t = toplevel_command
let project cmd = (cmd.directory,cmd.file,cmd.n)
- let compare c1 c2 = Pervasives.compare (project c1) (project c2)
+ let compare c1 c2 = compare (project c1) (project c2)
let equal c1 c2 = (project c1)=(project c2)
let hash c = Hashtbl.hash (project c)
end)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 3d2f1fdd6bf..655ce875418 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -432,7 +432,7 @@ module Bool = struct
type t = Top | True | False | Bottom
let hash (b : t) = Hashtbl.hash b
let equal (b1 : t) (b2 : t) = b1 = b2
- let compare (b1 : t) (b2 : t) = Pervasives.compare b1 b2
+ let compare (b1 : t) (b2 : t) = Transitioning.Stdlib.compare b1 b2
let pretty fmt = function
| Top -> Format.fprintf fmt "Top"
| True -> Format.fprintf fmt "True"
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 719eaa98d82..89c49bcc166 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -171,7 +171,7 @@ module Make (F: Float_sig.S) = struct
let compare x y =
match x, y with
| FRange.Itv (b1, e1, n1), FRange.Itv (b2, e2, n2) ->
- let c = Pervasives.compare n1 n2 in
+ let c = Transitioning.Stdlib.compare n1 n2 in
if c <> 0 then c else
let r = F.compare b1 b2 in
if r <> 0 then r else F.compare e1 e2
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ff279b93cf0..a33a5047ef4 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -129,7 +129,7 @@ module D =
let n = Exp.compare e1 e2 in
if n = 0 then Extlib.compare_basic fk1 fk2 else n
| Memory_access(lv1, access_kind1), Memory_access(lv2, access_kind2) ->
- let n = Pervasives.compare access_kind1 access_kind2 in
+ let n = Transitioning.Stdlib.compare access_kind1 access_kind2 in
if n = 0 then Lval.compare lv1 lv2 else n
| Index_out_of_bound(e11, e12), Index_out_of_bound(e21, e22) ->
let n = Exp.compare e11 e21 in
@@ -141,11 +141,11 @@ module D =
let n = Extlib.opt_compare Exp.compare e11 e21 in
if n = 0 then Exp.compare e12 e22 else n
| Overflow(s1, e1, n1, b1), Overflow(s2, e2, n2, b2) ->
- let n = Pervasives.compare s1 s2 in
+ let n = Transitioning.Stdlib.compare s1 s2 in
if n = 0 then
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Pervasives.compare b1 b2 in
+ let n = Transitioning.Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
@@ -154,7 +154,7 @@ module D =
| Float_to_int(e1, n1, b1), Float_to_int(e2, n2, b2) ->
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Pervasives.compare b1 b2 in
+ let n = Transitioning.Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index d61e7eec939..ccba7c4f34b 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -562,7 +562,7 @@ include Datatype.Make_with_collections
let n = Extlib.opt_compare Kf.compare kf1 kf2 in
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
- if n = 0 then Pervasives.compare ba1 ba2 else n
+ if n = 0 then Transitioning.Stdlib.compare ba1 ba2 else n
else
n
| IPAxiom (s1,_,_,_,_), IPAxiom (s2,_,_,_,_)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 10e25594bfe..4842bcdeb30 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -47,7 +47,7 @@ module Emitted_status =
| True -> "VALID"
| False_if_reachable | False_and_reachable -> "**NOT** VALID"
| Dont_know -> "unknown")
- let compare (s1:t) s2 = Pervasives.compare s1 s2
+ let compare (s1:t) s2 = Transitioning.Stdlib.compare s1 s2
let equal (s1:t) s2 = s1 = s2
let hash (s:t) = Caml_hashtbl.hash s
end)
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 6544c2ba0cb..ade7c65cc86 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -409,7 +409,7 @@ type order =
| A of Datatype.String.Set.t
let cmp_order a b = match a , b with
- | I a , I b -> Pervasives.compare a b
+ | I a , I b -> Transitioning.Stdlib.compare a b
| I _ , _ -> (-1)
| _ , I _ -> 1
| S a , S b -> String.compare a b
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index a4d1063fa01..17b141196aa 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1584,7 +1584,7 @@ and compare_toffset off1 off2 =
and compare_logic_label l1 l2 = match l1, l2 with
| StmtLabel s1 , StmtLabel s2 -> Stmt.compare !s1 !s2
| FormalLabel s1, FormalLabel s2 -> String.compare s1 s2
- | BuiltinLabel l1, BuiltinLabel l2 -> Pervasives.compare l1 l2
+ | BuiltinLabel l1, BuiltinLabel l2 -> Transitioning.Stdlib.compare l1 l2
| (StmtLabel _ | FormalLabel _), (FormalLabel _ | BuiltinLabel _) -> -1
| (BuiltinLabel _ | FormalLabel _), (StmtLabel _ | FormalLabel _) -> 1
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 0632240c7ca..7621c2488ce 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -284,7 +284,7 @@ module DatatypeMachdep = Datatype.Make_with_collections(struct
let reprs = [Machdeps.x86_32]
let name = "File.Machdep"
type t = Cil_types.mach
- let compare : t -> t -> int = Pervasives.compare
+ let compare : t -> t -> int = Transitioning.Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
let copy = Datatype.identity
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 918ca0447b7..3696935c926 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -457,7 +457,7 @@ module Type_namespace =
let reprs = [Typedef]
let name = "Logic_typing.type_namespace"
type t = type_namespace
- let compare : t -> t -> int = Pervasives.compare
+ let compare : t -> t -> int = Transitioning.Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
end)
@@ -3593,7 +3593,7 @@ struct
struct
type t = string list
let compare s1 s2 =
- Pervasives.(compare (List.sort compare s1) (List.sort compare s2))
+ Transitioning.Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
end)
let type_spec old_behaviors loc is_stmt_contract result env s =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 9ad4de77133..352824e171c 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1544,12 +1544,12 @@ let rec compare_term t1 t2 =
| TAlignOfE _, _ -> 1
| _, TAlignOfE _ -> -1
| TUnOp (o1,t1), TUnOp(o2,t2) ->
- let res = Pervasives.compare o1 o2 in
+ let res = Transitioning.Stdlib.compare o1 o2 in
if res = 0 then compare_term t1 t2 else res
| TUnOp _, _ -> 1
| _, TUnOp _ -> -1
| TBinOp(o1,l1,r1), TBinOp(o2,l2,r2) ->
- let res = Pervasives.compare o1 o2 in
+ let res = Transitioning.Stdlib.compare o1 o2 in
if res = 0 then
let res = compare_term l1 l2 in
if res = 0 then compare_term r1 r2 else res
@@ -1749,7 +1749,7 @@ and compare_predicate_node p1 p2 =
| Papp _, _ -> 1
| _, Papp _ -> -1
| Prel(r1,lt1,rt1), Prel(r2,lt2,rt2) ->
- let res = Pervasives.compare r1 r2 in
+ let res = Transitioning.Stdlib.compare r1 r2 in
if res = 0 then
let res = compare_term lt1 lt2 in
if res = 0 then compare_term rt1 rt2 else res
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 9752b11209c..328b9e1a1e3 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -1776,7 +1776,7 @@ module Bool =
let name = "bool"
let reprs = [ true ]
let copy = identity
- let compare : bool -> bool -> int = Pervasives.compare
+ let compare : bool -> bool -> int = Transitioning.Stdlib.compare
let equal : bool -> bool -> bool = (=)
let pretty fmt b = Format.fprintf fmt "%B" b
let varname _ = "b"
@@ -1790,12 +1790,12 @@ module Int = struct
let name = "int"
let reprs = [ 2 ]
let copy = identity
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Transitioning.Stdlib.compare
let equal : int -> int -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%d" n
let varname _ = "n"
end)
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Transitioning.Stdlib.compare
end
let int = Int.ty
@@ -1848,7 +1848,7 @@ module Float =
let name = "float"
let reprs = [ 0.1 ]
let copy = identity
- let compare : float -> float -> int = Pervasives.compare
+ let compare : float -> float -> int = Transitioning.Stdlib.compare
let equal : float -> float -> bool = (=)
let pretty fmt f = Format.fprintf fmt "%f" f
let varname _ = "f"
diff --git a/src/libraries/stdlib/FCHashtbl.ml b/src/libraries/stdlib/FCHashtbl.ml
index 4e84f1b3ced..a19c31b5996 100644
--- a/src/libraries/stdlib/FCHashtbl.ml
+++ b/src/libraries/stdlib/FCHashtbl.ml
@@ -50,7 +50,7 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
include Hashtbl.Make(H)
- let fold_sorted ?(cmp=Pervasives.compare) f h acc =
+ let fold_sorted ?(cmp=Transitioning.Stdlib.compare) f h acc =
let module Aux = struct type t = key let compare = cmp end in
let module M = FCMap.Make(Aux) in
let add k v m =
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 7848ea531cf..5dac32656eb 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -57,6 +57,12 @@ let _: ('a -> bool) -> 'a list -> 'a option = find_opt
let _: 'a -> ('a * 'b) list -> 'b option = assoc_opt
let _: 'a -> ('a * 'b) list -> 'b option = assq_opt
+let stdlib_compare = compare (* Pervasives/Stdlib compare *)
+
+module Stdlib = struct
+ let compare = stdlib_compare
+end
+
[@@@ warning "-3"]
module String = struct
diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml
index a1dfcfa38a4..36657b9600b 100644
--- a/src/libraries/utils/bitvector.ml
+++ b/src/libraries/utils/bitvector.ml
@@ -223,7 +223,7 @@ let bitwise_op4 size op4 a b c d =
let equal = (=);; (* String equality. *)
-let compare = Pervasives.compare
+let compare = Transitioning.Stdlib.compare
let hash = Hashtbl.hash
let concat bv1 size1 bv2 size2 =
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index 8444a4bc8ed..a2123702f15 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -37,7 +37,7 @@ type json =
type t = json
let equal = (=)
-let compare = Pervasives.compare
+let compare = Transitioning.Stdlib.compare
type token = EOF | TRUE | FALSE | NULL | KEY of char
| STR of string | INT of string | DEC of string
diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index 3ecc2ed1913..f78f4da7009 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -48,7 +48,7 @@ let rec pp_print_string_fill out s =
Format.fprintf out "%s@ %a" s1 pp_print_string_fill s2
end else Format.pp_print_string out s
-type sformat = (unit,Format.formatter,unit) Pervasives.format
+type sformat = (unit,Format.formatter,unit) format
type 'a formatter = Format.formatter -> 'a -> unit
type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit
@@ -180,11 +180,14 @@ let pp_trail pp fmt x =
(* --- Margins --- *)
(* -------------------------------------------------------------------------- *)
+let pervasives_min = min
+let pervasives_max = max
+
type marger = int ref
let marger () = ref 0
let add_margin marger ?(margin=0) ?(min=0) ?(max=80) text =
let size = String.length text + margin in
- let n = Pervasives.min max (Pervasives.max min size) in
+ let n = pervasives_min max (pervasives_max min size) in
if n > !marger then marger := n
type align = [ `Center | `Left | `Right ]
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index c0cfa39b1b6..416e56e9d08 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -70,7 +70,7 @@ val escape_underscores : string -> string
(** {2 pretty printers for standard types} *)
(* ********************************************************************** *)
-type sformat = (unit,Format.formatter,unit) Pervasives.format
+type sformat = (unit,Format.formatter,unit) format
type 'a formatter = Format.formatter -> 'a -> unit
type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit
diff --git a/src/libraries/utils/rgmap.ml b/src/libraries/utils/rgmap.ml
index 054bb4b9cfa..d1c4fd78aee 100644
--- a/src/libraries/utils/rgmap.ml
+++ b/src/libraries/utils/rgmap.ml
@@ -42,7 +42,7 @@ type 'a entry = int * int * 'a
module Wmap = Map.Make
(struct
type t = int
- let compare (a:t) (b:t) = Pervasives.compare a b
+ let compare (a:t) (b:t) = Transitioning.Stdlib.compare a b
end)
module Rmap = Map.Make
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 5a1f810e04f..c17460dafd9 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -164,8 +164,8 @@ struct
if (pe1 = pe2) then 0
else
(* most englobing comes first *)
- Pervasives.compare pe2 pe1
- else Pervasives.compare pb1 pb2
+ Transitioning.Stdlib.compare pe2 pe1
+ else Transitioning.Stdlib.compare pb1 pb2
) arr
;
arr
diff --git a/src/plugins/gui/warning_manager.ml b/src/plugins/gui/warning_manager.ml
index c27f8f1070d..bac5362ceb8 100644
--- a/src/plugins/gui/warning_manager.ml
+++ b/src/plugins/gui/warning_manager.ml
@@ -34,7 +34,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
let make ~packing ~callback =
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index 9eb22f91a2d..f10bf8fd034 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -265,7 +265,7 @@ let get_file_type filename =
module VarinfoByName = struct
type t = Cil_types.varinfo
- let compare v1 v2 = Pervasives.compare v1.vname v2.vname
+ let compare v1 v2 = Transitioning.Stdlib.compare v1.vname v2.vname
end
(** Map and sets of varinfos sorted by name (and not by ids) *)
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 216651aca09..f4f1fb22e5b 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -69,7 +69,7 @@ include Datatype.Make_with_collections
let reprs = [ Global_var ]
let hash (k:k) = Hashtbl.hash k
let equal (k1:k) k2 = k1 = k2
- let compare (k1:k) k2 = Pervasives.compare k1 k2
+ let compare (k1:k) k2 = Transitioning.Stdlib.compare k1 k2
let varname _ = "k"
let internal_pretty_code = Datatype.undefined
let copy = Datatype.identity
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index b36fca33b81..8f7d667899f 100644
--- a/src/plugins/qed/export.ml
+++ b/src/plugins/qed/export.ml
@@ -828,7 +828,7 @@ struct
(fun (s1,e1) (s2,e2) ->
match s1,s2 with
| true,true | false,false ->
- Pervasives.compare (T.weigth e1) (T.weigth e2)
+ Transitioning.Stdlib.compare (T.weigth e1) (T.weigth e2)
| true,false -> (-1)
| false,true -> 1
) sxs in
diff --git a/src/plugins/qed/intmap.ml b/src/plugins/qed/intmap.ml
index 70ded406022..e6b77689d3a 100644
--- a/src/plugins/qed/intmap.ml
+++ b/src/plugins/qed/intmap.ml
@@ -211,12 +211,12 @@ let rec compare cmp s t =
| Empty , _ -> (-1)
| _ , Empty -> 1
| Lf(i,x) , Lf(j,y) ->
- let ck = Pervasives.compare i j in
+ let ck = Transitioning.Stdlib.compare i j in
if ck = 0 then cmp x y else ck
| Lf _ , _ -> (-1)
| _ , Lf _ -> 1
| Br(p,s0,s1) , Br(q,t0,t1) ->
- let cp = Pervasives.compare p q in
+ let cp = Transitioning.Stdlib.compare p q in
if cp <> 0 then cp else
let c0 = compare cmp s0 t0 in
if c0 <> 0 then c0 else
diff --git a/src/plugins/qed/kind.ml b/src/plugins/qed/kind.ml
index 93d8d7fae87..e9207939eb1 100644
--- a/src/plugins/qed/kind.ml
+++ b/src/plugins/qed/kind.ml
@@ -177,7 +177,7 @@ let rec compare_tau cfield cadt t1 t2 =
| Prop , Prop -> 0
| Prop , _ -> (-1)
| _ , Prop -> 1
- | Tvar k , Tvar k' -> Pervasives.compare k k'
+ | Tvar k , Tvar k' -> Transitioning.Stdlib.compare k k'
| Tvar _ , _ -> (-1)
| _ , Tvar _ -> 1
| Array(ta,tb) , Array(ta',tb') ->
diff --git a/src/plugins/qed/pool.ml b/src/plugins/qed/pool.ml
index 868e99b8a57..bdb043a9aad 100644
--- a/src/plugins/qed/pool.ml
+++ b/src/plugins/qed/pool.ml
@@ -77,9 +77,9 @@ struct
let compare x y =
let cmp = String.compare x.vbase y.vbase in
if cmp <> 0 then cmp else
- let cmp = Pervasives.compare x.vrank y.vrank in
+ let cmp = Transitioning.Stdlib.compare x.vrank y.vrank in
if cmp <> 0 then cmp else
- Pervasives.compare x.vid y.vid
+ Transitioning.Stdlib.compare x.vid y.vid
(* POOL *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 0c05374f3a1..fa6e17a4dde 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -379,7 +379,7 @@ struct
| Constructor -> 1
| Operator _ -> 0
- let cmp_size a b = Pervasives.compare a.size b.size
+ let cmp_size a b = Transitioning.Stdlib.compare a.size b.size
let rank_bind = function Forall -> 0 | Exists -> 1 | Lambda -> 2
let cmp_bind p q = rank_bind p - rank_bind q
let cmp_field phi (f,x) (g,y) =
@@ -1221,7 +1221,7 @@ struct
| _ -> (k,t) :: acc
(* sorts monoms by terms *)
- let compare_monoms (_,t1) (_,t2) = Pervasives.compare t1.id t2.id
+ let compare_monoms (_,t1) (_,t2) = Transitioning.Stdlib.compare t1.id t2.id
(* factorized monoms *)
let fold_monom ts k t =
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index f14ae80130e..1d3a931ccf0 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -242,7 +242,7 @@ let json_of_event e =
module EVENTS = Set.Make
(struct
type t = event
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
end)
let events_queue = Queue.create ()
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index 643168a388f..7064555e9a0 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -66,7 +66,7 @@ let lines () =
emitted on statements copied through loop unrolling. This is the desired
semantics for now. However, since we compare entire locations, textually
identical lines that refer to different expressions are kept separate *)
- Extlib.sort_unique Pervasives.compare l
+ Extlib.sort_unique Transitioning.Stdlib.compare l
let output file =
let ch = open_out file in
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 062f57f0517..58e5b96280f 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -48,7 +48,7 @@ module Status = struct
let reprs = [ True; False; False; Unknown ]
let mem_project = Datatype.never_any_project
let pretty = pretty_status
- let compare (s1:t) (s2:t) = Pervasives.compare s1 s2
+ let compare (s1:t) (s2:t) = Transitioning.Stdlib.compare s1 s2
let equal (s1:t) (s2:t) = s1 = s2
let hash (s:t) = Hashtbl.hash s
end)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index ce361f8068a..78284d2e1d4 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -502,7 +502,7 @@ module G = struct
let compare ii1 ii2 = match ii1, ii2 with
| PreciseIteration i1, PreciseIteration i2 ->
- Pervasives.compare i1 i2
+ Transitioning.Stdlib.compare i1 i2
| MultipleIterations i1, MultipleIterations i2 ->
MultipleIterations.compare i1 i2
| PreciseIteration _, MultipleIterations _ -> -1
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index d75eefad242..18098708557 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -261,7 +261,7 @@ module Make (Input: Input) = struct
module Data = Indexer.Make(
struct
type t = int * value row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
(* This function creates a single GTree that displays per-callstack
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index 03929af50d5..4b807209ea7 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -108,7 +108,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
let append t message = t.append message
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index af63dc0f92d..30f4b3c3863 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -62,7 +62,7 @@ module Make (X : sig end) = struct
then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
else None
- let compare x y = Pervasives.compare x.tag y.tag
+ let compare x y = Transitioning.Stdlib.compare x.tag y.tag
let hash x = x.tag
let tag x = x.tag
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index 9476dbbb11f..7015fc9e3f3 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -88,7 +88,7 @@ module Call_info = struct
(* Sorts call_infos by decreasing execution time. *)
let cmp current_time ci1 ci2 =
- - (Pervasives.compare (total_duration current_time ci1) (total_duration current_time ci2))
+ - (Transitioning.Stdlib.compare (total_duration current_time ci1) (total_duration current_time ci2))
;;
(* From an iteration, filter and sort by call_info, and returns the
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index bb9f4c20a7d..114b2fba184 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -171,7 +171,7 @@ let compare a b = (a, b) >>+ fun _ ->
match a, b with
| NaN _, NaN _ -> 0 | NaN _, _ -> 1 | _, NaN _ -> -1
| I (x, y, n), I (x', y', n') ->
- let c = Pervasives.compare n n' in
+ let c = Transitioning.Stdlib.compare n n' in
if c = 0 then
let c = F.compare x x' in
if c = 0 then F.compare y y'
diff --git a/src/plugins/value/values/numerors/numerors_utils.ml b/src/plugins/value/values/numerors/numerors_utils.ml
index b456540037a..dd45d7afeb7 100644
--- a/src/plugins/value/values/numerors/numerors_utils.ml
+++ b/src/plugins/value/values/numerors/numerors_utils.ml
@@ -59,7 +59,7 @@ module Precisions = struct
| Simple -> -149 | Double -> -1074
| Long_Double -> -16494 | Real -> Pervasives.min_int
- let compare a b = Pervasives.compare (get a) (get b)
+ let compare a b = Transitioning.Stdlib.compare (get a) (get b)
let eq a b = compare a b = 0
let max a b = if compare a b <= 0 then b else a
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 2a6908fcf33..211ce3cd5b2 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -54,7 +54,7 @@ let empty = { pos = false; zero = false; neg = false }
include Datatype.Make(struct
type t = signs
include Datatype.Serializable_undefined
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let equal = Datatype.from_compare
let hash = Hashtbl.hash
let reprs = [top]
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index 88e5892d9bd..6109ac2d892 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -440,7 +440,7 @@ struct
let pp fmt = function | Node i -> Node.pp fmt i | Assume (i,_) -> Format.fprintf fmt "ass%i" i
| Check (i,_) -> Format.fprintf fmt "chk%i" i
let equal x y = (tag x) = (tag y)
- let compare x y = Pervasives.compare (tag x) (tag y)
+ let compare x y = Transitioning.Stdlib.compare (tag x) (tag y)
let hash x = tag x
end in
let module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (V)(E) in
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1fac69012b5..3362fc39f4d 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -270,7 +270,7 @@ struct
| _ -> 2
in
let r = rank s1.condition - rank s2.condition in
- if r = 0 then Pervasives.compare k2 k1 else r
+ if r = 0 then Transitioning.Stdlib.compare k2 k1 else r
end)
type t = Vars.t * SEQ.t
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index 66f3ab3afb6..f678abdd424 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -35,7 +35,7 @@ type cst =
module STR =
struct
type t = cst
- let compare = Pervasives.compare (* only comparable types *)
+ let compare = Transitioning.Stdlib.compare (* only comparable types *)
let pretty fmt = function
| C_str s -> Format.fprintf fmt "%S" s
| W_str _ -> Format.fprintf fmt "\"L<...>\""
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index bc0f3667d60..bc76ceb0d81 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -274,7 +274,7 @@ module COMPILERS = FCMap.Make
(struct
type t = setup * driver
let compare (s,d) (s',d') =
- let cmp = Pervasives.compare s s' in
+ let cmp = Transitioning.Stdlib.compare s s' in
if cmp <> 0 then cmp else LogicBuiltins.compare d d'
end)
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index a34105fae01..7e0b7b17c2b 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -43,7 +43,7 @@ type kind =
| F of Ctypes.c_float
| A (* abstract data *)
-(* [LC] kinds can be compared by Pervasives.compare *)
+(* [LC] kinds can be compared by Stdlib.compare *)
let okind = function
| C_int i -> I i
@@ -157,14 +157,14 @@ let iter_table f =
Hashtbl.iter
(fun a sigs -> List.iter (fun (ks,lnk) -> items := (a,ks,lnk)::!items) sigs)
(cdriver ()).hlogic ;
- List.iter f (List.sort Pervasives.compare !items)
+ List.iter f (List.sort Transitioning.Stdlib.compare !items)
let iter_libs f =
let items = ref [] in
Hashtbl.iter
(fun a libs -> items := (a,libs) :: !items)
(cdriver ()).hdeps ;
- List.iter f (List.sort Pervasives.compare !items)
+ List.iter f (List.sort Transitioning.Stdlib.compare !items)
let dump () =
Log.print_on_output
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 410076e90d5..6de0a92ea47 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -651,7 +651,7 @@ let shift l obj k = e_fun (Shift.get obj) [l;k]
module LITERAL =
struct
type t = int * Cstring.cst
- let compare (a:t) (b:t) = Pervasives.compare (fst a) (fst b)
+ let compare (a:t) (b:t) = Transitioning.Stdlib.compare (fst a) (fst b)
let pretty fmt (eid,cst) = Format.fprintf fmt "%a@%d" Cstring.pretty cst eid
end
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 3ccf4f59b68..e628fe6a352 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -47,7 +47,7 @@ struct
let sa = stage a in
let sb = stage b in
if sa = sb
- then Pervasives.compare (time a) (time b)
+ then Transitioning.Stdlib.compare (time a) (time b)
else sa - sb
let sort script = List.stable_sort compare script
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 4480ea68e99..56cbd3f35d0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -314,7 +314,7 @@ type goal =
module Goal =
struct
type t = goal
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let pretty fmt g =
Format.fprintf fmt "[%s]%s.%s" g.file g.theory g.goal
end
diff --git a/src/plugins/wp/Splitter.ml b/src/plugins/wp/Splitter.ml
index 9ac78de7720..c7afbd32731 100644
--- a/src/plugins/wp/Splitter.ml
+++ b/src/plugins/wp/Splitter.ml
@@ -68,7 +68,7 @@ let compare p q =
| _ , ELSE _ -> 1
| CASE(s1,k1) , CASE(s2,k2) ->
let c = Stmt.compare s1 s2 in
- if c = 0 then Pervasives.compare k1 k2 else c
+ if c = 0 then Transitioning.Stdlib.compare k1 k2 else c
| CASE _ , _ -> (-1)
| _ , CASE _ -> 1
| DEFAULT s , DEFAULT t -> Stmt.compare s t
@@ -80,7 +80,7 @@ let compare p q =
| CALL _ , _ -> (-1)
| _ , CALL _ -> 1
| ASSERT(ip1,k1,_) , ASSERT(ip2,k2,_) ->
- let c = Pervasives.compare ip1.ip_id ip2.ip_id in
+ let c = Transitioning.Stdlib.compare ip1.ip_id ip2.ip_id in
if c = 0 then k1 - k2 else c
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 968c460cb2b..1a9c9791b6c 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -499,7 +499,7 @@ struct
| NoneInfo, NoneInfo -> 0
| NoneInfo, _ -> -1
| _ , NoneInfo -> 1
- | LoopHead i, LoopHead j -> Pervasives.compare j i
+ | LoopHead i, LoopHead j -> Transitioning.Stdlib.compare j i
module Automata = Interpreted_automata.UnrollUnnatural.Version
type nodes = {
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index b6073824dd1..38f0f7f8141 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -106,7 +106,7 @@ type strategy = {
arguments : argument list ;
} and t = strategy
-let highest a b = Pervasives.compare b.priority a.priority
+let highest a b = Transitioning.Stdlib.compare b.priority a.priority
class pool =
object
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index a38694fad5d..a06e4d093dd 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -366,11 +366,11 @@ let compare p q =
in
let r = rank q.verdict - rank p.verdict in
if r <> 0 then r else
- let s = Pervasives.compare p.prover_steps q.prover_steps in
+ let s = Transitioning.Stdlib.compare p.prover_steps q.prover_steps in
if s <> 0 then s else
- let t = Pervasives.compare p.prover_time q.prover_time in
+ let t = Transitioning.Stdlib.compare p.prover_time q.prover_time in
if t <> 0 then t else
- Pervasives.compare p.solver_time q.solver_time
+ Transitioning.Stdlib.compare p.solver_time q.solver_time
let combine v1 v2 =
match v1 , v2 with
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index 56ea8e88b48..e9bc3d515bf 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -48,7 +48,7 @@ struct
match w1.severe , w2.severe with
| true , false -> (-1)
| false , true -> 1
- | _ -> Pervasives.compare w1 w2
+ | _ -> Transitioning.Stdlib.compare w1 w2
end
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 34c76d1ff2e..04cd9701c91 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -317,7 +317,7 @@ module AinfoComparable = struct
let c = !cmp obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Pervasives.compare a.arr_size b.arr_size
+ | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
@@ -574,7 +574,7 @@ and compare_array_ptr_conflated a b =
let c = compare_ptr_conflated obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Pervasives.compare a.arr_size b.arr_size
+ | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
index 129c0aad1ee..5a314f37dd0 100644
--- a/src/plugins/wp/proof.ml
+++ b/src/plugins/wp/proof.ml
@@ -225,7 +225,7 @@ let update_hints_for_goal goal hints =
try
let old_hints,script,qed = Hashtbl.find scriptbase goal in
let new_hints = List.sort String.compare hints in
- if Pervasives.compare new_hints old_hints <> 0 then
+ if Transitioning.Stdlib.compare new_hints old_hints <> 0 then
begin
Hashtbl.replace scriptbase goal (new_hints,script,qed) ;
needsave := true ;
diff --git a/src/plugins/wp/share/install.ml b/src/plugins/wp/share/install.ml
index 334e78760b3..bb0ee0a194c 100644
--- a/src/plugins/wp/share/install.ml
+++ b/src/plugins/wp/share/install.ml
@@ -43,8 +43,8 @@ let hardcopy inc out =
begin
let buffer = Bytes.create 1024 in
let n = ref 0 in
- while (n := Pervasives.input inc buffer 0 1024 ; !n > 0) do
- Pervasives.output out buffer 0 !n
+ while (n := input inc buffer 0 1024 ; !n > 0) do
+ output out buffer 0 !n
done ;
flush out ;
end
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7c2583caaf6..7e3009c53bb 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -192,7 +192,7 @@ let compare_kind k1 k2 = match k1, k2 with
if cmp <> 0 then cmp
else
Property.compare p1 p2
- | _,_ -> Pervasives.compare (kind_order k1) (kind_order k2)
+ | _,_ -> Transitioning.Stdlib.compare (kind_order k1) (kind_order k2)
let compare_prop_id pid1 pid2 =
(* This order of comparison groups together prop_pids with same properties *)
@@ -204,7 +204,7 @@ let compare_prop_id pid1 pid2 =
let cmp = compare_kind pid2.p_kind pid1.p_kind in
if cmp <> 0 then cmp
else
- Pervasives.compare pid1.p_part pid2.p_part
+ Transitioning.Stdlib.compare pid1.p_part pid2.p_part
module PropId =
Datatype.Make_with_collections(
--
GitLab