Merge branch 'fix/4.08' into 'master'

Removes compilation warnings with ocaml >= 4.08

See merge request frama-c/frama-c!2498

src/libraries/stdlib/transitioning.ml.in

@@ -29,6 +29,7 @@ module Stdlib = struct
   let max = max
   let min_int = min_int
   let max_int = max_int
+  let flush = flush
 end
 
 [@@@ warning "-3"]

src/libraries/stdlib/transitioning.mli

@@ -42,6 +42,7 @@ module Stdlib: sig
   val max: 'a -> 'a -> 'a
   val min_int: int
   val max_int: int
+  val flush: out_channel -> unit
 end
 
 (** 4.08 *)

src/libraries/utils/dotgraph.ml

@@ -128,7 +128,7 @@ let close dot =
     begin
       Format.fprintf dot.fmt "}@." ;
       dot.fmt <- Format.err_formatter ;
-      Pervasives.flush out ; close_out out ;
+      Transitioning.Stdlib.flush out ; close_out out ;
       dot.out <- None ;
     end
 

src/plugins/server/doc.ml

@@ -123,7 +123,7 @@ let table_of_contents () =
 module Cmap = Map.Make
     (struct
       type t = string list
-      let compare = Pervasives.compare
+      let compare = Transitioning.Stdlib.compare
     end)
 
 let index_entry (title,href) =

src/plugins/server/jbuffer.ml

@@ -40,7 +40,8 @@ let flush buffer () =
     buffer.rjson <- js :: buffer.rjson ;
     FCBuffer.clear t
 
-let push_tag buffer tag =
+let push_tag buffer stag =
+  let tag = Transitioning.Format.string_of_stag stag in
   flush buffer () ;
   buffer.stack <- ( tag , buffer.rjson ) :: buffer.stack ;
   buffer.rjson <- []
@@ -83,15 +84,15 @@ let create ?indent ?margin () =
       Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
   end ;
   begin
-    let open Format in
-    pp_set_formatter_tag_functions fmt {
-      print_open_tag = no_mark ;
-      print_close_tag = no_mark ;
-      mark_open_tag = mark_open_tag buffer ;
-      mark_close_tag = mark_close_tag buffer ;
+    let open Transitioning.Format in
+    pp_set_formatter_stag_functions fmt {
+      print_open_stag = no_mark ;
+      print_close_stag = no_mark ;
+      mark_open_stag = mark_open_tag buffer ;
+      mark_close_stag = mark_close_tag buffer ;
     } ;
-    pp_set_print_tags fmt false ;
-    pp_set_mark_tags fmt true ;
+    Format.pp_set_print_tags fmt false ;
+    Format.pp_set_mark_tags fmt true ;
   end ;
   buffer
 

src/plugins/server/jbuffer.mli

@@ -46,8 +46,8 @@ val bprintf : buffer -> ('a,Format.formatter,unit) format -> 'a
 
 val append : buffer -> string -> int -> int -> unit
 val flush : buffer -> unit -> unit
-val push_tag : buffer -> Format.tag -> unit
-val pop_tag : buffer -> Format.tag -> unit
+val push_tag : buffer -> Transitioning.Format.stag -> unit
+val pop_tag : buffer -> Transitioning.Format.stag -> unit
 
 (** Flushes the buffer and returns its JSON enoding. This pops all pending
     tags. *)

src/plugins/wp/Cfloat.ml

@@ -305,7 +305,7 @@ module Compute = WpContext.StaticGenerator
     (struct
       type t = model * c_float * op
 
-      let compare = Pervasives.compare
+      let compare = Transitioning.Stdlib.compare
 
       let pretty fmt (m, ft, op) =
         Format.fprintf fmt "%s_%a_%s" (model_name m) pp_suffix ft (op_name op)

src/plugins/wp/Layout.ml

@@ -52,7 +52,7 @@ struct
       | _ , Field _ -> 1
       | Index(ta,n) , Index(tb,m) ->
           let cmp = Typ.compare ta tb in
-          if cmp <> 0 then cmp else Pervasives.compare n m
+          if cmp <> 0 then cmp else Transitioning.Stdlib.compare n m
 
   let equal a b = (compare a b = 0)
 
@@ -175,7 +175,7 @@ struct
     Usage.pretty fmt usage
 
   let compare ((da,ta):t) ((db,tb):t) =
-    let cmp = Pervasives.compare da db in
+    let cmp = Transitioning.Stdlib.compare da db in
     if cmp <> 0 then cmp else Typ.compare ta tb
 
   let equal a b = (compare a b = 0)

src/plugins/wp/MemRegion.ml

@@ -234,7 +234,7 @@ struct
           Format.fprintf fmt "}@]" ;
         end
 
-  let compare = Pervasives.compare
+  let compare = Transitioning.Stdlib.compare
 
   (* Extract constant offset *)
   let offset k =
@@ -300,7 +300,7 @@ module ARRAY =
 struct
 
   type t = int * int list
-  let compare = Pervasives.compare
+  let compare = Transitioning.Stdlib.compare
   let pretty fmt (s,ds) = Format.fprintf fmt "%d%a" s Layout.Matrix.pretty ds
 
   (* Coefficient from Matrix dimensions: c_i = \Pi_{i<j} d_j *)
@@ -636,7 +636,8 @@ struct
     | Mu_alloc -> Region.noid
 
   let hash m = id m
-  let compare m m' = if m==m then 0 else Pervasives.compare (id m) (id m')
+  let compare m m' =
+    if m==m then 0 else Transitioning.Stdlib.compare (id m) (id m')
   let equal m m' = m==m' || (id m = id m')
 
   let tau_of_value = function

src/plugins/wp/Region.ml

@@ -128,7 +128,7 @@ struct
   type t = region
   let id a = a.id
   let equal a b = (a.id = b.id)
-  let compare a b = Pervasives.compare a.id b.id
+  let compare a b = Transitioning.Stdlib.compare a.id b.id
   let pp_rid fmt id = Format.fprintf fmt "R%03d" id
   let pretty fmt r = pp_rid fmt r.id
 end