remove obsolete occurrences of Transitioning due to migration towards 4.08.1

Makefile

@@ -1575,10 +1575,6 @@ STDLIB_FILES:=\
 	weak \
 	ephemeron
 
-ifeq ($(HAS_OCAML407),no)
-  STDLIB_FILES+=pervasives
-endif
-
 STDLIB_FILES:=$(patsubst %,$(OCAMLLIB)/%.mli,$(STDLIB_FILES))
 
 .PHONY: doc-kernel

Makefile.generating

@@ -126,56 +126,12 @@ endif
 
 GENERATED+= src/libraries/utils/json.ml src/libraries/stdlib/transitioning.ml
 
-ifeq ($(HAS_OCAML408),yes)
-  DYNLINK_INIT=fun () -> ()
-  FORMAT_STAG=stag
-  FORMAT_STRING_OF_STAG=match s with \
-        Format.String_tag str -> str \
-      | _ -> raise (Invalid_argument "unsupported tag extension")
-  FORMAT_STAG_OF_STRING=Format.String_tag s
-  FORMAT_PP_OPT=Format.pp_print_option
-  HAS_OCAML407_OR_408=yes
-else
-  DYNLINK_INIT=Dynlink.init
-  FORMAT_STAG=tag
-  FORMAT_STRING_OF_STAG=s
-  FORMAT_STAG_OF_STRING=s
-  ifeq ($(HAS_OCAML407),yes)
-    HAS_OCAML407_OR_408=yes
-  else
-    HAS_OCAML407_OR_408=no
-  endif
-  FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \
-    match o with \
-    | None -> none fmt () \
-    | Some v -> pp fmt v
-endif
-
-ifeq ($(HAS_OCAML407_OR_408),yes)
-  FLOAT_MAX_FLOAT=Float.max_float
-else
-  FLOAT_MAX_FLOAT=Pervasives.max_float
-endif
-
 src/libraries/stdlib/transitioning.ml: \
   src/libraries/stdlib/transitioning.ml.in \
   Makefile.generating share/Makefile.config
 	$(PRINT_MAKING) $@
 	rm -f $@
-	sed \
-         -e 's/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g' \
-         -e 's/@STACK_FOLD@/$(STACK_FOLD)/g' \
-         -e 's/@NTH_OPT@/$(NTH_OPT)/g' \
-         -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/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/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' \
-         -e 's/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g' \
-        $< > $@
+	cat $< > $@
 	$(CHMOD_RO) $@
 
 ##################

configure.in

@@ -108,8 +108,8 @@ AC_MSG_CHECKING(version of OCaml)
 OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
 AC_MSG_RESULT($OCAMLVERSION)
 case $OCAMLVERSION in
-  0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*)
-     AC_MSG_ERROR(Incompatible OCaml version; use 4.05+.);;
+  0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*|4.05.*|4.06.*|4.07.*|4.08.0)
+     AC_MSG_ERROR(Incompatible OCaml version; use 4.08.1+.);;
    *)
      OCAML_ANNOT_OPTION="-bin-annot";;
 esac
@@ -118,24 +118,24 @@ AC_SUBST(OCAMLMAJORNB)
 AC_SUBST(OCAMLMINORNB)
 AC_SUBST(OCAMLPATCHNB)
 
-AC_SUBST(HAS_OCAML407)
-AC_SUBST(HAS_OCAML408)
+AC_SUBST(HAS_OCAML409)
+AC_SUBST(HAS_OCAML410)
 
 OCAMLMAJORNB=$(echo $OCAMLVERSION | cut -f 1 -d .)
 OCAMLMINORNB=$(echo $OCAMLVERSION | cut -f 2 -d .)
 OCAMLPATCHNB=$(echo $OCAMLVERSION | cut -f 3 -d .)
 
 if test $OCAMLMAJORNB -gt 4; then
-  HAS_OCAML407=yes;
-  HAS_OCAML408=yes;
+  HAS_OCAML409=yes;
+  HAS_OCAML410=yes;
 else
-  HAS_OCAML407=no;
-  HAS_OCAML408=no;
-  if test $OCAMLMINORNB -ge 7; then
-    HAS_OCAML407=yes;
+  HAS_OCAML409=no;
+  HAS_OCAML410=no;
+  if test $OCAMLMINORNB -ge 9; then
+    HAS_OCAML409=yes;
   fi;
-  if test $OCAMLMINORNB -ge 8; then
-    HAS_OCAML408=yes;
+  if test $OCAMLMINORNB -ge 10; then
+    HAS_OCAML410=yes;
   fi;
 fi;   # MAJORNB -gt 4
 
@@ -300,10 +300,14 @@ AC_MSG_CHECKING(for zarith)
 
 ZARITH=$($OCAMLFIND query zarith -format %v)
 if test -z "$ZARITH" ; then
-  AC_MSG_ERROR(Cannot find zarith via ocamlfind.)
-else
-  AC_MSG_RESULT(found $ZARITH)
+  AC_MSG_ERROR(Cannot find zarith via ocamlfind (requires zarith 1.5 or higher).)
 fi
+case ZARITH in
+      1.[[01234]].*)
+        AC_MSG_ERROR(found $ZARITH: requires 1.5 or higher.);;
+      *)
+        AC_MSG_RESULT(found $ZARITH);;
+esac
 
 # yojson
 ########
@@ -839,7 +843,7 @@ AC_ARG_ENABLE(external,
 ])
 
 AC_FOREACH([__plugin],m4_esyscmd([ls src/plugins]),
-  [ m4_if(m4_regexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1],
+  [ m4_if(m4_bregexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1],
       [
         m4_define([plugin_dir],[src/plugins/__plugin])
         m4_syscmd(test -r plugin_dir/configure.in)

share/Makefile.config.in

@@ -85,8 +85,8 @@ OCAMLMAJORNB    ?=@OCAMLMAJORNB@
 OCAMLMINORNB    ?=@OCAMLMINORNB@
 OCAMLPATCHNB    ?=@OCAMLPATCHNB@
 
-HAS_OCAML407    ?=@HAS_OCAML407@
-HAS_OCAML408    ?=@HAS_OCAML408@
+HAS_OCAML409    ?=@HAS_OCAML409@
+HAS_OCAML410    ?=@HAS_OCAML410@
 
 PLATFORM	?=@PLATFORM@
 OCAMLWIN32	?=@OCAMLWIN32@

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) = Transitioning.Stdlib.compare b1 b2
+  let compare (b1 : t) (b2 : t) = Stdlib.compare b1 b2
   let pretty fmt = function
     | Top -> Format.fprintf fmt "Top"
     | True -> Format.fprintf fmt "True"

src/kernel_services/abstract_interp/float_interval.ml

@@ -172,7 +172,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 = Transitioning.Stdlib.compare n1 n2 in
+      let c = 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

src/kernel_services/abstract_interp/offsetmap.ml

@@ -307,7 +307,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 := Transitioning.Stdlib.succ current_counter;
+         counter := Stdlib.succ current_counter;
       end;
       hashed_node
 

src/kernel_services/ast_data/alarms.ml

@@ -134,7 +134,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 = Transitioning.Stdlib.compare access_kind1 access_kind2 in
+          let n = 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
@@ -147,11 +147,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 = Transitioning.Stdlib.compare s1 s2 in
+          let n = Stdlib.compare s1 s2 in
           if n = 0 then
             let n = Exp.compare e1 e2 in
             if n = 0 then
-              let n = Transitioning.Stdlib.compare b1 b2 in
+              let n = Stdlib.compare b1 b2 in
               if n = 0 then Integer.compare n1 n2 else n
             else
               n
@@ -160,7 +160,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 = Transitioning.Stdlib.compare b1 b2 in
+            let n = Stdlib.compare b1 b2 in
             if n = 0 then Integer.compare n1 n2 else n
           else
             n

src/kernel_services/ast_data/annotations.ml

@@ -285,7 +285,7 @@ let merge_funspec s1 s2 =
 (** {2 Getting annotations} *)
 (**************************************************************************)
 
-module Behavior_set_map = Transitioning.Stdlib.Map.Make(Datatype.String.Set)
+module Behavior_set_map = Stdlib.Map.Make(Datatype.String.Set)
 
 let is_same_behavior_set l1 l2 =
   Datatype.String.Set.(equal (of_list l1) (of_list l2))

src/kernel_services/ast_data/property.ml

@@ -658,7 +658,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 Transitioning.Stdlib.compare ba1 ba2 else n
+            if n = 0 then Stdlib.compare ba1 ba2 else n
           else
             n
         | IPAxiom {il_name=s1}, IPAxiom {il_name=s2}

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 = Transitioning.Stdlib.compare s1 s2
+      let compare (s1:t) s2 = Stdlib.compare s1 s2
       let equal (s1:t) s2 = s1 = s2
       let hash (s:t) = Caml_hashtbl.hash s
     end)

src/kernel_services/ast_printing/cabs_debug.ml

@@ -251,11 +251,11 @@ and pp_raw_stmt fmt = function
       pp_block bl1 pp_block bl2 pp_cabsloc loc
   |     THROW(e,loc) ->
     fprintf fmt "@[<hov 2>THROW %a, loc(%a)@]"
-      (Transitioning.Format.pp_print_option pp_exp) e pp_cabsloc loc
+      (Format.pp_print_option pp_exp) e pp_cabsloc loc
   |     TRY_CATCH(s,l,loc) ->
     let print_one_catch fmt (v,s) =
       fprintf fmt "@[<v 2>@[CATCH %a {@]@;%a@]@;}"
-        (Transitioning.Format.pp_print_option pp_single_name) v
+        (Format.pp_print_option pp_single_name) v
         pp_stmt s
     in
     fprintf fmt "@[<v 2>@[TRY %a (loc %a) {@]@;%a@]@;}"

src/kernel_services/ast_printing/description.ml

@@ -424,7 +424,7 @@ type order =
   | A of Datatype.String.Set.t
 
 let cmp_order a b = match a , b with
-  | I a , I b -> Transitioning.Stdlib.compare a b
+  | I a , I b -> Stdlib.compare a b
   | I _ , _ -> (-1)
   | _ , I _ -> 1
   | S a , S b -> String.compare a b

src/kernel_services/ast_queries/cil_datatype.ml

@@ -1639,7 +1639,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 -> Transitioning.Stdlib.compare l1 l2
+  | BuiltinLabel l1, BuiltinLabel l2 -> Stdlib.compare l1 l2
   | (StmtLabel _ | FormalLabel _), (FormalLabel _ | BuiltinLabel _) -> -1
   | (BuiltinLabel _ | FormalLabel _), (StmtLabel _ | FormalLabel _) -> 1
 

src/kernel_services/ast_queries/file.ml

@@ -303,7 +303,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 = Transitioning.Stdlib.compare
+    let compare : t -> t -> int = Stdlib.compare
     let equal : t -> t -> bool = (=)
     let hash : t -> int = Hashtbl.hash
     let copy = Datatype.identity

src/kernel_services/ast_queries/logic_typing.ml

@@ -478,7 +478,7 @@ module Type_namespace =
     let reprs = [Typedef]
     let name = "Logic_typing.type_namespace"
     type t = type_namespace
-    let compare : t -> t -> int = Transitioning.Stdlib.compare
+    let compare : t -> t -> int = Stdlib.compare
     let equal : t -> t -> bool = (=)
     let hash : t -> int = Hashtbl.hash
   end)
@@ -3614,7 +3614,7 @@ struct
     struct
       type t = string list
       let compare s1 s2 =
-        Transitioning.Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
+        Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
     end)
 
   let type_spec old_behaviors loc is_stmt_contract result env s =

src/kernel_services/ast_queries/logic_utils.ml

@@ -1657,12 +1657,12 @@ let rec compare_term t1 t2 =
   | TAlignOfE _, _ -> 1
   | _, TAlignOfE _ -> -1
   | TUnOp (o1,t1), TUnOp(o2,t2) ->
-    let res = Transitioning.Stdlib.compare o1 o2 in
+    let res = 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 = Transitioning.Stdlib.compare o1 o2 in
+    let res = 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
@@ -1852,7 +1852,7 @@ and compare_predicate_node p1 p2 =
   | Papp _, _ -> 1
   | _, Papp _ -> -1
   | Prel(r1,lt1,rt1), Prel(r2,lt2,rt2) ->
-    let res = Transitioning.Stdlib.compare r1 r2 in
+    let res = 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

src/kernel_services/plugin_entry_points/dynamic.ml

@@ -46,7 +46,6 @@ let dynlib_init () =
   if not !dynlib_init then
     begin
       dynlib_init := true ;
-      Transitioning.Dynlink.init () ;
       Dynlink.allow_unsafe_modules true ;
     end
 

src/kernel_services/plugin_entry_points/plugin.ml

@@ -679,7 +679,7 @@ struct
            (* the level of verbose is at least the level of debug *)
            if n > Verbose.get () then Verbose.set n;
            if n = 0 then decr positive_debug_ref
-           else if old = 0 then Transitioning.Stdlib.incr positive_debug_ref);
+           else if old = 0 then 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

src/libraries/datatype/datatype.ml

@@ -1676,13 +1676,13 @@ module With_collections(X: S)(Info: Functor_info) = struct
 
   module Set =
     Set
-      (Transitioning.Stdlib.Set.Make(D))
+      (Stdlib.Set.Make(D))
       (D)
       (struct let module_name = Info.module_name ^ ".Set" end)
 
   module Map =
     Map
-      (Transitioning.Stdlib.Map.Make(D))
+      (Stdlib.Map.Make(D))
       (D)
       (struct let module_name = Info.module_name ^ ".Map" end)
 
@@ -1781,7 +1781,7 @@ module Bool =
       let name = "bool"
       let reprs = [ true ]
       let copy = identity
-      let compare : bool -> bool -> int = Transitioning.Stdlib.compare
+      let compare : bool -> bool -> int = Stdlib.compare
       let equal : bool -> bool -> bool = (=)
       let pretty fmt b = Format.fprintf fmt "%B" b
       let varname _ = "b"
@@ -1795,12 +1795,12 @@ module Int = struct
       let name = "int"
       let reprs = [ 2 ]
       let copy = identity
-      let compare : int -> int -> int = Transitioning.Stdlib.compare
+      let compare : int -> int -> int = 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 = Transitioning.Stdlib.compare
+  let compare : int -> int -> int = Stdlib.compare
 end
 let int = Int.ty
 
@@ -1853,7 +1853,7 @@ module Float =
       let name = "float"
       let reprs = [ 0.1 ]
       let copy = identity
-      let compare : float -> float -> int = Transitioning.Stdlib.compare
+      let compare : float -> float -> int = Stdlib.compare
       let equal : float -> float -> bool = (=)
       let pretty fmt f = Format.fprintf fmt "%f" f
       let varname _ = "f"