From 7514d3c22bbf1131b0ab02547cb7798c4fea9a75 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 14 Feb 2019 17:23:35 +0100
Subject: [PATCH] [ocaml] improve compatibility with OCaml 4.08

---
 Makefile.generating                                       | 7 +++++++
 configure.in                                              | 6 ++++++
 opam/opam                                                 | 2 +-
 share/Makefile.config.in                                  | 1 +
 src/kernel_services/abstract_interp/offsetmap.ml          | 3 ++-
 src/kernel_services/ast_queries/cil_datatype.ml           | 2 +-
 .../ast_queries/json_compilation_database.ok.ml           | 2 +-
 src/kernel_services/cmdline_parameters/cmdline.ml         | 4 ++--
 src/kernel_services/plugin_entry_points/dynamic.ml        | 2 +-
 src/kernel_services/plugin_entry_points/log.ml            | 4 ++--
 src/kernel_services/plugin_entry_points/plugin.ml         | 7 ++++---
 src/libraries/stdlib/extlib.ml                            | 4 ++--
 src/libraries/stdlib/transitioning.ml.in                  | 4 ++++
 src/libraries/stdlib/transitioning.mli                    | 8 ++++++++
 src/libraries/utils/command.ml                            | 4 ++--
 src/plugins/aorai/ltl_output.ml                           | 2 +-
 src/plugins/metrics/metrics_cabs.ml                       | 2 +-
 src/plugins/rte/visit.ml                                  | 2 +-
 src/plugins/value/domains/numerors/numerors_domain.ok.ml  | 2 +-
 src/plugins/value_types/cvalue.ml                         | 2 +-
 20 files changed, 49 insertions(+), 21 deletions(-)

diff --git a/Makefile.generating b/Makefile.generating
index 58a6083f7db..a79f857a468 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -151,6 +151,12 @@ else
   ASSQ_OPT=assq_opt
 endif
 
+ifeq ($(HAS_OCAML408),yes)
+  DYNLINK_INIT=fun () -> ()
+else
+  DYNLINK_INIT=Dynlink.init
+endif
+
 src/libraries/stdlib/transitioning.ml: \
   src/libraries/stdlib/transitioning.ml.in \
   Makefile.generating share/Makefile.config
@@ -163,6 +169,7 @@ 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' \
         $< > $@
 	$(CHMOD_RO) $@
 
diff --git a/configure.in b/configure.in
index 988da1a7b0c..f3c6e60e52c 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/opam/opam b/opam/opam
index caef4a4893a..1a4556250e9 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/share/Makefile.config.in b/share/Makefile.config.in
index 9d321679ed9..38ae166ad90 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/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 01dba5d8ede..d605d48d9cc 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 := pervasives_succ current_counter;
       end;
       hashed_node
 
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 3c944847e4e..a4d1063fa01 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
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 851ddde5a87..2442e726b6a 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/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index d74c0ed2086..b49b856b2cd 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 5666e51558b..0ad27f1c620 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 be6d501cfc7..da8b3426d77 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 fa721f6e114..a5c3a0f2f72 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
 
@@ -608,6 +608,7 @@ struct
 
   let debug_optname = output_mode "Debug" "debug"
   module Debug = struct
+    let pervasives_incr = incr (* before 'incr' is shadowed by the one in Int *)
     include
       Int(struct
             let default = !debug_level ()
@@ -627,8 +628,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 pervasives_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/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 6ec413e5c12..c24744c1154 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 053b4627244..7848ea531cf 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -83,6 +83,10 @@ module List = struct
   let assq_opt = @ASSQ_OPT@
 end
 
+module Dynlink = struct
+  let init = @DYNLINK_INIT@
+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 c138f09e9b9..5b542fd7b9f 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -65,6 +65,14 @@ module List: sig
   val assq_opt: 'a -> ('a * 'b) list -> 'b option (** 4.05 *)
 end
 
+module Stdlib: sig
+  val compare: 'a -> 'a -> int
+end
+
+module Dynlink: sig
+  val init: unit -> unit
+end
+
 (** {1 Zarith} *)
 
 (** Function [Q.to_float] was introduced in Zarith 1.5 *)
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 3e08c8037a6..f11b1065d5e 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/plugins/aorai/ltl_output.ml b/src/plugins/aorai/ltl_output.ml
index ae142d75373..53e63d359f6 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/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 8b46580b8dd..884e81054ac 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/rte/visit.ml b/src/plugins/rte/visit.ml
index 41f597a4fc0..33aeb7f6e7d 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/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index c385ee3a1f3..763a8209f23 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_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index f6306e870ba..7ee4502377b 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
-- 
GitLab