diff --git a/Makefile.generating b/Makefile.generating
index 58a6083f7db6c804da63afc6a845f00b1c25e652..568a02af72e64b3b4a4a3dc5eb59f60f86d3aa3f 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -151,6 +151,20 @@ else
ASSQ_OPT=assq_opt
endif
+ifeq ($(HAS_OCAML408),yes)
+ DYNLINK_INIT=fun () -> ()
+ FORMAT_STAG=stag
+ FORMAT_STRING_OF_STAG=match s with\n\
+ | Format.String_tag str -> str\n\
+ | _ -> raise (Invalid_argument "unsupported tag extension")
+ FORMAT_STAG_OF_STRING=Format.String_tag s
+else
+ DYNLINK_INIT=Dynlink.init
+ FORMAT_STAG=tag
+ FORMAT_STRING_OF_STAG=s
+ FORMAT_STAG_OF_STRING=s
+endif
+
src/libraries/stdlib/transitioning.ml: \
src/libraries/stdlib/transitioning.ml.in \
Makefile.generating share/Makefile.config
@@ -163,6 +177,10 @@ src/libraries/stdlib/transitioning.ml: \
-e 's/@FIND_OPT@/$(FIND_OPT)/g' \
-e 's/@ASSOC_OPT@/$(ASSOC_OPT)/g' \
-e 's/@ASSQ_OPT@/$(ASSQ_OPT)/g' \
+ -e 's/@DYNLINK_INIT@/$(DYNLINK_INIT)/g' \
+ -e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
+ -e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
+ -e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
$< > $@
$(CHMOD_RO) $@
diff --git a/configure.in b/configure.in
index 988da1a7b0cada6cc5de981f4e790bc82aafdcb4..f3c6e60e52c09bc7de449dd31069df7925c7a240 100644
--- a/configure.in
+++ b/configure.in
@@ -121,6 +121,7 @@ AC_SUBST(HAS_OCAML403)
AC_SUBST(HAS_OCAML404)
AC_SUBST(HAS_OCAML405)
AC_SUBST(HAS_OCAML407)
+AC_SUBST(HAS_OCAML408)
OCAMLMAJORNB=$(echo $OCAMLVERSION | cut -f 1 -d .)
OCAMLMINORNB=$(echo $OCAMLVERSION | cut -f 2 -d .)
@@ -131,11 +132,13 @@ if test $OCAMLMAJORNB -gt 4; then
HAS_OCAML404=yes;
HAS_OCAML405=yes;
HAS_OCAML407=yes;
+ HAS_OCAML408=yes;
else
HAS_OCAML403=no;
HAS_OCAML404=no;
HAS_OCAML405=no;
HAS_OCAML407=no;
+ HAS_OCAML408=no;
if test $OCAMLMINORNB -ge 3; then
HAS_OCAML403=yes;
fi;
@@ -148,6 +151,9 @@ else
if test $OCAMLMINORNB -ge 7; then
HAS_OCAML407=yes;
fi;
+ if test $OCAMLMINORNB -ge 8; then
+ HAS_OCAML408=yes;
+ fi;
fi; # MAJORNB -gt 4
# Ocaml library path
diff --git a/devel_tools/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml
index 3e3290c2246a174c62821a701e6b2c25d5b6fa79..c14aace6a12959ce4b475e66999282221541bd9d 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/opam/opam b/opam/opam
index caef4a4893ad8ec34c890f659daddaaa9bc5a594..1a4556250e9963f74ffb6b7628b918b2a527b501 100644
--- a/opam/opam
+++ b/opam/opam
@@ -96,7 +96,7 @@ depends: [
]
depopts: [
- "yojson" { build }
+ "yojson" { build & >= "1.6.0" }
"coq" { build }
"why3" { build }
"mlgmpidl" { build }
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index ef9497abebbceba829913c2c4cf56847fd4b08ca..61d3b38decb7b848f2810cfc9d23433148f28fe0 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/share/Makefile.config.in b/share/Makefile.config.in
index 9d321679ed94e0bd3c09e788c50172408cd44421..38ae166ad906647076df7b1d402102b1697f5dc4 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -89,6 +89,7 @@ HAS_OCAML403 ?=@HAS_OCAML403@
HAS_OCAML404 ?=@HAS_OCAML404@
HAS_OCAML405 ?=@HAS_OCAML405@
HAS_OCAML407 ?=@HAS_OCAML407@
+HAS_OCAML408 ?=@HAS_OCAML408@
NATIVE_THREADS ?=@HAS_NATIVE_THREADS@
OCAMLWIN32 ?=@OCAMLWIN32@
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 3d2f1fdd6bff8e142fb2dcfdea076c3b91522f73..655ce87541875983b1a94f8a057f6633241f54c5 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 719eaa98d82b78b55698343539bd1a6351e3cf5b..89c49bcc1665585e90cd3eb29bd1c4fd622e20d0 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/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 01dba5d8ede8bb1189928451d76109ba3d3f0bfb..82625312c80d8735bfe1fd1c54330127ec4987a0 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -22,6 +22,7 @@
open Abstract_interp
+let pervasives_succ = succ
(* This module uses Bigints everywhere. Set up some notations *)
let pretty_int = Int.pretty
let ( =~ ) = Integer.equal
@@ -308,7 +309,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
then begin
if current_counter = max_int
then Kernel.fatal "Offsetmap(%s): internal maximum exeeded" V.name;
- counter := Pervasives.succ current_counter;
+ counter := Transitioning.Stdlib.succ current_counter;
end;
hashed_node
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ff279b93cf08519395f6ef3652339a5a93912ccf..a33a5047ef460dc233a85e1afa1a0b4ffc6131f5 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 d61e7eec939bc5495e058724901f21d606f8bf2e..ccba7c4f34b98bd4947c104ab47e58a8c5c390d9 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 10e25594bfed19cfedf49dca7ae9938475b680cf..4842bcdeb30cff1a9acb5f5cdca88897ed7a8894 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 6544c2ba0cbb5055d14e179024bd7821292d189b..ade7c65cc86b8c94b7cacbb38c36a9cc19367c00 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 3c944847e4e219637f04ad1d2ab481d3c32ea781..17b141196aacedcb19746db9f02ac4d65c8a38aa 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1443,7 +1443,7 @@ end
(* @return [true] is the given logic real represents an exact float *)
let is_exact_float r =
- Pervasives.classify_float r.r_upper = FP_normal &&
+ classify_float r.r_upper = FP_normal &&
Datatype.Float.equal r.r_upper r.r_lower
let compare_logic_constant c1 c2 = match c1,c2 with
@@ -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 0632240c7cabaf813a28d995b8a73d938b2bdb40..7621c2488ce42a79de03329e5905cd99326104b1 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/json_compilation_database.ok.ml b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
index 851ddde5a87304e73ed6dd7c9e94d552b24a7132..2442e726b6a3dd8583bed2415b238e1fd64af819 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ok.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
@@ -127,7 +127,7 @@ let split_command_args s =
never need quotes. *)
let quote_define_argument arg = Format.sprintf "%S" arg
-let parse_entry ?(cwd=Sys.getcwd()) (r : Yojson.Basic.json) =
+let parse_entry ?(cwd=Sys.getcwd()) (r : Yojson.Basic.t) =
let open Yojson.Basic.Util in
let filename = r |> member "file" |> to_string in
let dirname = r |> member "directory" |> to_string_option |> Extlib.opt_conv "" in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 918ca0447b734454367bde0b04082b03bec3ff96..3696935c9266797f8316aa6d5b0fedc9d83bedd0 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 9ad4de7713352889d31e310614767229efa173fa..352824e171c1585f0746e879da519a37f82c871a 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/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index d74c0ed2086143d36929e877277bd6d6557b9ebb..b49b856b2cdae25c02ad46673bb4a6f67705c47a 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -230,8 +230,8 @@ let catch_toplevel_run ~f ~at_normal_exit ~on_error =
(* write again on stdout *)
Log.set_output
~isatty:(Unix.isatty Unix.stdout)
- (Pervasives.output_substring stdout)
- (fun () -> Pervasives.flush stdout);
+ (output_substring stdout)
+ (fun () -> flush stdout);
cleanup ();
with
| Exit ->
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 5666e51558b4c86c74e925a73b5c5f36d71bb469..0ad27f1c620c9e031ffb609d6aef8137b112b343 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -46,7 +46,7 @@ let dynlib_init () =
if not !dynlib_init then
begin
dynlib_init := true ;
- Dynlink.init () ;
+ Transitioning.Dynlink.init () ;
Dynlink.allow_unsafe_modules true ;
end
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index be6d501cfc71e95f795400fbbd97ead1fa8e7257..da8b3426d7743580f633840a8657d6120fabeeb6 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -120,8 +120,8 @@ let stdout = {
clean = true ;
delayed = [] ;
isatty = Unix.isatty Unix.stdout ;
- output = Pervasives.output_substring Pervasives.stdout ;
- flush = (fun () -> Pervasives.flush Pervasives.stdout);
+ output = output_substring stdout ;
+ flush = (fun () -> flush stdout);
}
let clean () = term_clean stdout
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index fa721f6e1140c36d876d99914e4838afc7fcd0f3..bd956deba6cd929e018b78d2348da570c48357dd 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -166,7 +166,7 @@ struct
let oc = open_out normalized_filename in
let fmt = Format.formatter_of_out_channel oc in
Hashtbl.add file_formatters normalized_filename fmt;
- Extlib.safe_at_exit (fun () -> Pervasives.close_out oc);
+ Extlib.safe_at_exit (fun () -> close_out oc);
fmt
end
@@ -627,8 +627,8 @@ struct
(fun old n ->
(* the level of verbose is at least the level of debug *)
if n > Verbose.get () then Verbose.set n;
- if n = 0 then Pervasives.decr positive_debug_ref
- else if old = 0 then Pervasives.incr positive_debug_ref);
+ if n = 0 then decr positive_debug_ref
+ else if old = 0 then Transitioning.Stdlib.incr positive_debug_ref);
if is_kernel () then begin
Cmdline.kernel_debug_atleast_ref := (fun n -> get () >= n);
match !Cmdline.Kernel_debug_level.value_if_set with
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 9752b11209c61111831cfa57d7b0ce6dfea3e5a9..328b9e1a1e39b56e6dc0ed6d23b889c58749eadc 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 4e84f1b3ced33540d4cb72ff7b1f797937ef2bfe..a19c31b59965524a171ab964b38ff6c8e7bc7e02 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/extlib.ml b/src/libraries/stdlib/extlib.ml
index 6ec413e5c12a3a40379b4c3d3e786609b54915e0..c24744c1154b1a4eb1ec89cd2197443026f7d6e6 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -341,11 +341,11 @@ let try_finally ~finally f x =
The alternative, such as registering an daemon that raises an exception,
hence interrupting the process, might not work: child processes still need to
- run some daemons, such as [Pervasives.flush_all] which is registered by default. *)
+ run some daemons, such as [flush_all] which is registered by default. *)
let pid = Unix.getpid ()
let safe_at_exit f =
- Pervasives.at_exit
+ at_exit
begin fun () ->
let child = Unix.getpid () in
if child = pid then f ()
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 053b4627244c1fcbc7e79231494b20f7747b7d9c..f96a0faf050cbec8204b9422f3e8598e8c50fafe 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -57,6 +57,15 @@ 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
+module Stdlib = struct
+ (* Pervasives/Stdlib functions *)
+ let compare = compare
+ let succ = succ
+ let incr = incr
+ let min = min
+ let max = max
+end
+
[@@@ warning "-3"]
module String = struct
@@ -83,6 +92,46 @@ module List = struct
let assq_opt = @ASSQ_OPT@
end
+module Dynlink = struct
+ let init = @DYNLINK_INIT@
+end
+
+module Format = struct
+ type stag = Format.@FORMAT_STAG@
+ let string_of_stag s = @FORMAT_STRING_OF_STAG@
+ let stag_of_string s = @FORMAT_STAG_OF_STRING@
+ type formatter_stag_functions = {
+ mark_open_stag : stag -> string;
+ mark_close_stag : stag -> string;
+ print_open_stag : stag -> unit;
+ print_close_stag : stag -> unit;
+ }
+ let pp_set_formatter_stag_functions fmt set_formatter_stag_functions =
+ Format.pp_set_formatter_@FORMAT_STAG@_functions fmt
+ {
+ Format.mark_open_@FORMAT_STAG@ =
+ set_formatter_stag_functions.mark_open_stag;
+ Format.mark_close_@FORMAT_STAG@ =
+ set_formatter_stag_functions.mark_close_stag;
+ Format.print_open_@FORMAT_STAG@ =
+ set_formatter_stag_functions.print_open_stag;
+ Format.print_close_@FORMAT_STAG@ =
+ set_formatter_stag_functions.print_close_stag;
+ }
+ let pp_get_formatter_stag_functions fmt () =
+ let st = Format.pp_get_formatter_@FORMAT_STAG@_functions fmt () in
+ {
+ mark_open_stag = st.Format.mark_open_@FORMAT_STAG@;
+ mark_close_stag = st.Format.mark_close_@FORMAT_STAG@;
+ print_open_stag = st.Format.print_open_@FORMAT_STAG@;
+ print_close_stag = st.Format.print_close_@FORMAT_STAG@;
+ }
+ let pp_open_stag fmt s =
+ Format.pp_open_@FORMAT_STAG@ fmt s
+ let pp_close_stag fmt () =
+ Format.pp_close_@FORMAT_STAG@ fmt ()
+end
+
module Q = struct
let round_to_float x exact =
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index c138f09e9b9b1daa70928d14d302664d2875b73f..2da86f65736949cb7611be416a5288ee5b1f054b 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -65,6 +65,39 @@ module List: sig
val assq_opt: 'a -> ('a * 'b) list -> 'b option (** 4.05 *)
end
+(** 4.08 *)
+module Stdlib: sig
+ val compare: 'a -> 'a -> int
+ val succ: int -> int
+ val incr: int ref -> unit
+ val min: 'a -> 'a -> 'a
+ val max: 'a -> 'a -> 'a
+end
+
+(** 4.08 *)
+module Dynlink: sig
+ val init: unit -> unit
+end
+
+(** 4.08 *)
+module Format: sig
+ type stag
+ val string_of_stag: stag -> string
+ val stag_of_string: string -> stag
+ type formatter_stag_functions = {
+ mark_open_stag : stag -> string;
+ mark_close_stag : stag -> string;
+ print_open_stag : stag -> unit;
+ print_close_stag : stag -> unit;
+ }
+ val pp_set_formatter_stag_functions:
+ Format.formatter -> formatter_stag_functions -> unit
+ val pp_get_formatter_stag_functions:
+ Format.formatter -> unit -> formatter_stag_functions
+ val pp_open_stag : Format.formatter -> stag -> unit
+ val pp_close_stag : Format.formatter -> unit -> unit
+end
+
(** {1 Zarith} *)
(** Function [Q.to_float] was introduced in Zarith 1.5 *)
diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml
index a1dfcfa38a4fedeaedb472bed9e4da705168d501..36657b9600b294c8aafb2391f85cc6c3de3e41b9 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/command.ml b/src/libraries/utils/command.ml
index 3e08c8037a6c31de22960dd26f2553b9e6d9e8dd..f11b1065d5e4a0b1eb3d41f9fb4ab6398219c0b4 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -59,9 +59,9 @@ let pp_from_file fmt file =
let rec bincopy buffer cin cout =
let s = Bytes.length buffer in
- let n = Pervasives.input cin buffer 0 s in
+ let n = input cin buffer 0 s in
if n > 0 then
- ( Pervasives.output cout buffer 0 n ; bincopy buffer cin cout )
+ ( output cout buffer 0 n ; bincopy buffer cin cout )
else
( flush cout )
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index 8444a4bc8ed32eb86fd517fedf9d7fd74143df47..a2123702f152a5d6611126dae17f60572843f638 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 3ecc2ed1913e5f0d15842863071b9cd74435c621..dc501dd587ba902d57e046638053815069774ce7 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
@@ -184,7 +184,7 @@ 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 = Transitioning.Stdlib.min max (Transitioning.Stdlib.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 c0cfa39b1b6543cf0fc3e5d46704bb93846ed55b..416e56e9d08e548fc15a276239e0d5ae7fcb8a12 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 054bb4b9cfac56c9129dd6daf04d862a9df3feed..d1c4fd78aee633698806adde8331fae90c5311b6 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/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index 3a15771b965c85bb62c45878e0e82a8d9cdfc76c..cfba39cf308cdc83bd4ac1147c409caf48e75042 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -27,7 +27,7 @@
type tag = {
p : int ; (* first position *)
q : int ; (* last position (excluded) *)
- tag : Format.tag ;
+ tag : Transitioning.Format.stag ;
children : tag list ;
}
@@ -50,8 +50,8 @@ let tags_at (_,tags) k = lookup [] k tags
type env = {
text : string ;
output : (string -> int -> int -> unit) option ;
- open_tag : (Format.tag -> int -> int -> unit) option ;
- close_tag : (Format.tag -> int -> int -> unit) option ;
+ open_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
+ close_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
}
let signal f tag p q =
@@ -86,8 +86,8 @@ let rec output_vbox fmt text k n =
end
let output_fmt fmt text k n = Format.pp_print_string fmt (String.sub text k n)
-let open_tag fmt tag _k _n = Format.pp_open_tag fmt tag
-let close_tag fmt _tag _k _n = Format.pp_close_tag fmt ()
+let open_tag fmt tag _k _n = Transitioning.Format.pp_open_stag fmt tag
+let close_tag fmt _tag _k _n = Transitioning.Format.pp_close_stag fmt ()
let pretty ?vbox fmt message =
let open_tag = open_tag fmt in
@@ -209,11 +209,11 @@ let create ?indent ?margin () =
Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
end ;
let open Format in
- pp_set_formatter_tag_functions fmt {
- print_open_tag = push_tag buffer ;
- print_close_tag = pop_tag buffer ;
- mark_open_tag = no_mark ;
- mark_close_tag = no_mark ;
+ Transitioning.Format.pp_set_formatter_stag_functions fmt {
+ Transitioning.Format.print_open_stag = push_tag buffer ;
+ print_close_stag = pop_tag buffer ;
+ mark_open_stag = no_mark ;
+ mark_close_stag = no_mark ;
} ;
pp_set_print_tags fmt true ;
pp_set_mark_tags fmt false ;
diff --git a/src/libraries/utils/rich_text.mli b/src/libraries/utils/rich_text.mli
index 415d3e3ef32a1a708b89b5606c1104812786e13f..172a9dd3513b02aadb4ea64e21ec57b3eb8a55f1 100644
--- a/src/libraries/utils/rich_text.mli
+++ b/src/libraries/utils/rich_text.mli
@@ -31,14 +31,14 @@ val char_at : message -> int -> char
val string : message -> string
val substring : message -> int -> int -> string
-val tags_at : message -> int -> (Format.tag * int * int) list
+val tags_at : message -> int -> (Transitioning.Format.stag * int * int) list
(** Returns the list of tags at the given position.
Inner tags come first, outer tags last. *)
val visit :
?output:(string -> int -> int -> unit) ->
- ?open_tag:(Format.tag -> int -> int -> unit) ->
- ?close_tag:(Format.tag -> int -> int -> unit) ->
+ ?open_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
+ ?close_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
message -> unit
(** Visit the message, with depth-first recursion on tags.
All methods are called with text or tag, position and length. *)
diff --git a/src/plugins/aorai/ltl_output.ml b/src/plugins/aorai/ltl_output.ml
index ae142d75373dd60d85bac9cd2727b94b0fd75fb3..53e63d359f69192dbf43197a9028b52f2180c6bd 100644
--- a/src/plugins/aorai/ltl_output.ml
+++ b/src/plugins/aorai/ltl_output.ml
@@ -23,7 +23,7 @@
(* *)
(**************************************************************************)
-open Format open Pervasives
+open Format
open Ltlast
let out_fmt=ref (formatter_of_out_channel stdout)
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 5a1f810e04f26cce0e71f89a660a2a358325d27e..d7fb0efbdcd99194ec3005eb963ad86b9fdc77eb 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
@@ -274,12 +274,14 @@ let localizable_from_locs state ~file ~line =
let buffer_formatter state source =
let starts = Stack.create () in
let emit_open_tag s =
+ let s = Transitioning.Format.string_of_stag s in
(* Ignore tags that are not ours *)
if Extlib.string_prefix "guitag:" s then
Stack.push (source#end_iter#offset, Tag.get s) starts ;
""
in
let emit_close_tag s =
+ let s = Transitioning.Format.string_of_stag s in
(try
if Extlib.string_prefix "guitag:" s then
let (p,sid) = Stack.pop starts in
@@ -292,10 +294,12 @@ let buffer_formatter state source =
Format.pp_set_tags gtk_fmt true;
Format.pp_set_print_tags gtk_fmt false;
Format.pp_set_mark_tags gtk_fmt true;
- Format.pp_set_formatter_tag_functions
- gtk_fmt {(Format.pp_get_formatter_tag_functions gtk_fmt ()) with
- Format.mark_open_tag = emit_open_tag;
- Format.mark_close_tag = emit_close_tag;};
+ let open Transitioning.Format in
+ pp_set_formatter_stag_functions
+ gtk_fmt {(pp_get_formatter_stag_functions gtk_fmt ())
+ with
+ mark_open_stag = emit_open_tag;
+ mark_close_stag = emit_close_tag;};
Format.pp_set_margin gtk_fmt 79;
gtk_fmt
diff --git a/src/plugins/gui/warning_manager.ml b/src/plugins/gui/warning_manager.ml
index c27f8f1070dd489bb877a35ee0597d8e7755f003..bac5362ceb8b11063002fc26cef28d0e1a55a861 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/gui/wtext.ml b/src/plugins/gui/wtext.ml
index 53537274b92620d81cca223a4145bb68aaf8c66d..e87caf583e28717555dbfc1f7d23bbefa7837d6d 100644
--- a/src/plugins/gui/wtext.ml
+++ b/src/plugins/gui/wtext.ml
@@ -244,6 +244,7 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
end
method private open_tag name =
+ let name = Transitioning.Format.string_of_stag name in
self#flush () ; style <- self#tag name :: style ; ""
method private close_tag _name =
@@ -254,13 +255,14 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
| (TAG _ | PLAIN) :: sty -> style <- sty ; ""
method fmt = match fmtref with Some fmt -> fmt | None ->
+ let open Transitioning.Format in
let output_string s a b = if b > 0 then Buffer.add_substring text s a b in
let fmt = Format.make_formatter output_string self#flush in
- let tagger = Format.pp_get_formatter_tag_functions fmt () in
- Format.pp_set_formatter_tag_functions fmt
+ let tagger = pp_get_formatter_stag_functions fmt () in
+ pp_set_formatter_stag_functions fmt
{ tagger with
- Format.mark_open_tag = self#open_tag ;
- Format.mark_close_tag = self#close_tag ;
+ mark_open_stag = self#open_tag;
+ mark_close_stag = self#close_tag ;
} ;
Format.pp_set_print_tags fmt false ;
Format.pp_set_mark_tags fmt true ;
@@ -306,9 +308,10 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
begin
let sid = hid <- succ hid ; Printf.sprintf ">%X" hid in
Hashtbl.add marks sid (fun p q -> Hashtbl.remove marks sid ; f p q) ;
- Format.pp_open_tag fmt sid ;
+ Transitioning.Format.pp_open_stag fmt
+ (Transitioning.Format.stag_of_string sid) ;
let () = pp fmt in
- Format.pp_close_tag fmt () ;
+ Transitioning.Format.pp_close_stag fmt () ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index ebba36bb4033ebaf551f4c050edcbbd8174ce1c5..0e107134a784d1f7a3c16b7cd547882865513f9d 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -284,7 +284,7 @@ let dump_acsl_stats fmt =
let dump_acsl_stats_html fmt =
- Format.pp_set_formatter_tag_functions fmt Metrics_base.html_tag_functions;
+ Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.fprintf fmt
"@[<v 0> <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
\"http://www.w3.org/TR/html4/strict.dtd\">@ \
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index 9eb22f91a2d9727170f3ed7feb4acca0819f6c86..b55a6772f17b53bf04d984bce393b164d1e52edf 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -24,22 +24,22 @@ open Cil_types (* vname, vaddrof *)
;;
(* Formatting html with Format.formatters *)
-let html_tag_functions =
- let mark_open_tag t = Format.sprintf "<%s>" t
- and mark_close_tag t =
+let html_stag_functions =
+ let mark_open_stag t =
+ let t = Transitioning.Format.string_of_stag t in
+ Format.sprintf "<%s>" t
+ and mark_close_stag t =
+ let t = Transitioning.Format.string_of_stag t in
try
let index = String.index t ' ' in
Format.sprintf "</%s>" (String.sub t 0 index)
with
| Not_found -> Format.sprintf "</%s>" t
- and print_open_tag _ = ()
- and print_close_tag _ = ()
+ and print_open_stag _ = ()
+ and print_close_stag _ = ()
in
- { Format.mark_open_tag = mark_open_tag;
- Format.mark_close_tag = mark_close_tag;
- Format.print_open_tag = print_open_tag;
- Format.print_close_tag = print_close_tag;
- }
+ { Transitioning.Format.mark_open_stag; mark_close_stag;
+ print_open_stag; print_close_stag; }
;;
(* Utility function to have underlines the same length as the title.
@@ -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/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index 6976f2c9c73fae948a022030d2ad5d2c0ac439ae..9ff77090ef5cd259d487cb74769de152e8424113 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Tag functions handling html tags for Format *)
-val html_tag_functions : Format.formatter_tag_functions;;
+val html_stag_functions : Transitioning.Format.formatter_stag_functions;;
(** mk_hdr [level] [ppf] [hdr_strg] produces a title from [hdr_strg] with an
underline of the same length.
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 8b46580b8dde6c35a78ace8a40a456a403455382..884e81054ac694d053918430ce4da92034ce72e5 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -520,7 +520,7 @@ let get_metrics cabs_visitor =
and distinct_operands, total_operands = compute_operands operand_tbl in
let program_length = total_operands +. total_operators in
let vocabulary_size = distinct_operands +. distinct_operators in
- let log2 x = (Pervasives.log x) /. (Pervasives.log 2.0) in
+ let log2 x = (log x) /. (log 2.0) in
let program_volume = program_length *. (log2 vocabulary_size) in
let difficulty_level =
(distinct_operators /. 2.) *. (total_operands /. distinct_operands) in
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 6474c0e06191a96073c31f18f4a0a7047b69f939..9ccc80eb23103cbb27441673f342fe6a8687730f 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -135,7 +135,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
Format.fprintf fmt "%a" self#pp_file_metrics filename) metrics_map
method print_stats fmt =
- Format.pp_set_formatter_tag_functions fmt Metrics_base.html_tag_functions;
+ Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.pp_set_tags fmt true;
let pr_hdr fmt hdr_name =
Format.fprintf fmt "@{<th>%s@}" hdr_name in
@@ -547,7 +547,7 @@ let pretty_used_files used_files =
let dump_html fmt cil_visitor =
(* Activate tagging for html *)
- Format.pp_set_formatter_tag_functions fmt html_tag_functions;
+ Transitioning.Format.pp_set_formatter_stag_functions fmt html_stag_functions;
Format.pp_set_tags fmt true;
let pr_row s fmt n =
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index f16d7007a7d889cf4c4682d7dc563ca724b6de87..38cb84cfccddc2cbce8c2403160e29125ae652e8 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -347,10 +347,11 @@ module ValueCoverageGUI = struct
~markup:(Format.sprintf "%s%% functions reached"
(Metrics_base.float_to_string pcent))
~justify:`LEFT ~packing:box#pack ());
- let _ = Gtk_helper.on_bool box "Highlight results" (fun () -> !highlight)
- (fun b -> highlight := b; main_ui#rehighlight ())
+ let _ignore = Gtk_helper.on_bool box "Highlight results"
+ (fun () -> !highlight)
+ (fun b -> highlight := b; main_ui#rehighlight ())
in
- let _ = Gtk_helper.on_bool box "Show columns"
+ let _ignore = Gtk_helper.on_bool box "Show columns"
~tooltip:"Shows the columns related to dead code in the filetree."
(fun () -> !filetree_enabled)
(fun b -> filetree_enabled := b; !update_filetree `Visibility)
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 216651aca09b951745e6b6639b3be7cbf2f14f8f..f4f1fb22e5b396056789b6d543d1b17e1283e04a 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/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index 9fbba556725d43f3660638f10b1a9d21e4f993fd..3df2230eeaced7a4cf838505650b702a581205fc 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -71,7 +71,7 @@ let filter_accesses l =
let f = consider_access () in
List.filter (fun access -> f (Register.classify_accesses access)) l
-let _ =
+let _ignore =
Dynamic.register
~plugin:"Occurrence"
~journalize:false
@@ -79,7 +79,7 @@ let _ =
(Datatype.func Datatype.bool Datatype.unit)
Enabled.set
-let _ =
+let _ignore =
Dynamic.register
~plugin:"Occurrence"
~journalize:false
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index b36fca33b8152f2f7dcba4a777d08de35fdf37f7..8f7d667899f2fa0b28b3496fffc9ecc3457c4b98 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 70ded406022bd1b52ee7eedd9236f579e9f76dd3..e6b77689d3a68bf9708da7390cab08c23d11fef4 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 93d8d7fae87f4b8c513545a64548ea6273696858..e9207939eb1d3e238e6c3dc4810ab93ca36a0c77 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 868e99b8a5791a5c5ac6e8a43aba25690daf7a51..bdb043a9aadbd75edf4d6c3312fbb346da6263da 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 0c05374f3a184680de0625a57c77d8cbced021aa..fa6e17a4ddec2150f394086d0898031297e621f6 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 f14ae80130e34ff8adf403f3605582636f5ad075..1d3a931ccf0f44484a297421ac1b53e8b7d59f5f 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 643168a388f3184f1ae4eea2a25a6995aa887656..7064555e9a0077894970da26a11b6673232a94fc 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/rte/register.ml b/src/plugins/rte/register.ml
index ab0d3111c0a0da3d7e9c6b7e1777e17659c14c57..99e58a483d2556e4764d4e538a57dacac76ac0b1 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -63,7 +63,7 @@ let journal_register ?comment is_dyn name ty_arg fctref fct =
let ty = Datatype.func ty_arg Datatype.unit in
Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
if is_dyn then
- let _ =
+ let _ignore =
Dynamic.register ?comment ~plugin:"RteGen" name ty ~journalize:true fct
in
()
@@ -111,7 +111,7 @@ let _ =
(* retrieve list of generated rte annotations (not precond) for
a given stmt *)
-let _ =
+let _ignore =
Dynamic.register
~comment:"Get the list of annotations previously emitted by RTE for the \
given statement."
@@ -123,7 +123,7 @@ let _ =
~journalize:true
Generator.get_registered_annotations
-let _ =
+let _ignore =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given stmt of \
the given function."
@@ -134,7 +134,7 @@ let _ =
~journalize:false
Visit.get_annotations_stmt
-let _ =
+let _ignore =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given exp \
of the given stmt in the given function."
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 41f597a4fc075a37c252d2f6f2634c8d1842b0e6..33aeb7f6e7ddefbf1c12b08819c420c089b2fb48 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -315,7 +315,7 @@ class annot_visitor kf flags on_alarm = object (self)
self#generate_assertion Rte.finite_float_assertion (to_fkind,exp)
| _ -> ());
| Const (CReal(f,fkind,_)) when self#do_finite_float () ->
- begin match Pervasives.classify_float f with
+ begin match classify_float f with
| FP_normal
| FP_subnormal
| FP_zero -> ()
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 062f57f05174f880780c1207d6b44d8f42d9f9ec..58e5b96280fd67851df297755143e0bfd2c0bd0e 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 ce361f8068a847ba4c0735e85ecc16a3cebad1e3..78284d2e1d4a394ff72b29b142cf3d7e439d4830 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/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index c385ee3a1f37c30e99efc18590ee2ddb462048fe..763a8209f237c083cd3c77bf5f37ce73ca902487 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
@@ -153,7 +153,7 @@ module Domain = struct
let log = Pervasives.open_out s in
let fmt = Format.formatter_of_out_channel log in
List.iter (fun f -> f fmt ()) !Numerors_Value.dprint_callstack ;
- Pervasives.close_out log
+ close_out log
| _, _ -> ()
end
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index d75eefad24279240861c589c4aa2a7199f74d8a5..18098708557657587fb0f99f93a7702e3e9ca292 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 03929af50d5f22280fc3dec000de633004b5d86e..4b807209ea73577e1a3e4bdd3e65cfab925630f6 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 af63dc0f92d72a2a76c7fa92211b4802e02d1cc5..30f4b3c38637a85fc888f4e7541ed9cf7b89f51d 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 9476dbbb11f8dd59b13b986fb989f0bb918a95a2..7015fc9e3f38dcadffcadeba2e489920bf3226b2 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 bb9f4c20a7d2b931b41a6d160b0bc5c07bc3191e..114b2fba184e2676e35ae1068c1c032193442e4b 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 b456540037a4cf3864cdd94c2955030e80216a6a..dd45d7afeb77a4a803d64a81cd9d25cc61c9c44c 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 2a6908fcf334bc60a6ace07bf11fbdeeb28be111..211ce3cd5b2891d14d9a44a6e6f5862aed9eb762 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/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index f6306e870ba5213e56daa45aca32fe0682244f44..7ee4502377bd972fd87abfb20e44dc853af3e12d 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -32,7 +32,7 @@ module CardinalEstimate = struct
let zero = None
let one = Some 0.0
- let of_integer x = Some(Pervasives.log10 (Integer.to_float x))
+ let of_integer x = Some(log10 (Integer.to_float x))
let infinite = Some(infinity)
let mul a b = match (a,b) with
| None, _ | _, None -> None
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index 88e5892d9bd0b61e6faa5341bb51aeaba0c6621a..6109ac2d892a28f893ed5805e24735bdc900c479 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 1fac69012b52aeae87e0b8ee5df50b9315ac4c54..3362fc39f4d25f1e4e29eea574d771ba64ce37a0 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 66f3ab3afb6e32672107fa09484c648640827026..f678abdd424048e1d6069157c3806b0302707a52 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 bc0f3667d600ba5553a818df622c507c70a01f48..bc76ceb0d8180a2944f420e6fe6386235ca401c4 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 a34105fae018047c8194da662cbf79aa356b8e41..7e0b7b17c2b8a2a4fbe785bf7110f4950f15e443 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 410076e90d5b76643c128246e264f40d836807d6..6de0a92ea470f46ac2559dbef0a92a60dd5edc15 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 3ccf4f59b6873a055a172ced0622f3e5ae6cfbbf..e628fe6a352255bf984f4f6aaa120c148e7226e3 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 4480ea68e99f8fb138ab27deed9f3208e2ce5a04..56cbd3f35d0ef00ad13a1781a3a94ceee09e6b34 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 9ac78de77206ef6f1c7f1dc2d95e54cb5865706c..c7afbd32731372465883e617ebeaa5026cbac0da 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 968c460cb2b5941bbe21304fc8ea819281bf9330..1a9c9791b6c6305bf21a1717d8009696620cba8f 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 b6073824dd1f12a63fc3e91e3d40f4575334e0c1..38f0f7f81414abd86eb784b79f6855821e19581b 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/TacShift.ml b/src/plugins/wp/TacShift.ml
index fff37a69094cfad98a268ab90100b7834634d576..4a1d714fa8c4f7331890a171b3ffa156a6d1289a 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -84,7 +84,7 @@ let is_shift e =
let open Qed.Logic in
match F.repr e with
| Fun( f , [_;n] ) ->
- let _ = select_op f in
+ let _ignore = select_op f in
let _ = select_int n in
true
| _ -> false
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index a38694fad5d63641e00d86ef41b2af6b27f9ff8e..a06e4d093ddddfbe589c8c1c73955f0f2611cf8f 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 56ea8e88b484eef4da87686ebfc3bd2894cf8b5d..e9bc3d515bf18c680d5b8f834b195f12f1ca1e71 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 34c76d1ff2e5b49184aab55d7def49df1df0ab4d..04cd9701c91426a98d40259689f9c518e9d46d0a 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 129c0aad1eef0dae724859a24e95067287cecfc3..5a314f37dd03e886b58b0e872d5b864f447586f9 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/register.ml b/src/plugins/wp/register.ml
index b8bbb65f08b7cb52a063fced89af61b765c89ddc..33157b918215fb24c5a52cb16d0560e5a13744be 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -732,7 +732,7 @@ let deprecated name =
"Dynamic '%s' now is deprecated. Use `Wp.VC` api instead." name
let register name ty code =
- let _ =
+ let _ignore =
Dynamic.register ~plugin:"Wp" name ty
~journalize:false (*LC: Because of Property is not journalizable. *)
(fun x -> deprecated name ; code x)
diff --git a/src/plugins/wp/share/install.ml b/src/plugins/wp/share/install.ml
index 334e78760b39c685fd9e32b3ce9abe9e40e9de56..bb0ee0a194cece3b8fc548b37236ee8cd01bfba0 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 7c2583caaf67aabc0f6133d09e4cb50880a1c166..7e3009c53bb7fe0117b0c4850da8094daff69536 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(
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index b4ff5124a5c54d708891290a466c0566b4c08f0f..782b9a5425dfb48bfc7d165900d6733b75a2b27b 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -965,7 +965,7 @@ let get_logfile w prover result =
let model = get_model w in
DISK.cache_log ~pid:w.po_pid ~model ~prover ~result
-let _ =
+let _ignore =
Dynamic.register ~plugin:"Wp" "Wpo.file_for_log_proof" ~journalize:false
(Datatype.func2
WpoType.ty ProverType.ty