Commit b2fa52ef authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/andre/transitioning-update-408' into 'master'

Feature/andre/transitioning update 408

See merge request frama-c/frama-c!2768
parents e5e493f1 3fcbc990
......@@ -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
......
......@@ -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) $@
##################
......
......@@ -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)
......
......@@ -1236,8 +1236,8 @@ and user-friendly way.
As a general rule, you should \emph{never} write to standard output
and error channels through \ocaml standard libraries. For instance,
you should never use \texttt{Pervasives.stdout} and
\texttt{Pervasives.stderr} channels, nor \texttt{Format.printf}-like
you should never use \texttt{Stdlib.stdout} and
\texttt{Stdlib.stderr} channels, nor \texttt{Format.printf}-like
routines.
Instead, you should use \texttt{Format.fprintf} to implement
......@@ -1616,7 +1616,7 @@ allows you to create such channels for your own purposes.
Basically, \emph{channels} ensure that no message emission interfere
with each others during echo on standard output. Hence the forbidden
direct access to \lstinline{Pervasives.stdout}. However,
direct access to \lstinline{Stdlib.stdout}. However,
\lstinline{Log} interface allows you to create such channels on your
own, in addition to the one automatically created for your plug-in.
......@@ -1666,7 +1666,7 @@ another channel:
\end{description}
It is also possible to have a momentary direct access to
\lstinline{Pervasives.stdout}, or whatever its redirection is:
\lstinline{Stdlib.stdout}, or whatever its redirection is:
\begin{description}
%%item
\logroutine{print\_on\_output}{ "..."}%
......@@ -1844,7 +1844,7 @@ module AB =
(Structural_desr.Sum [| [| Structural_descr.p_int |] |])
(* equality, compare and hash are the standard OCaml ones *)
let equal (x:t) y = x = y
let compare (x:t) y = Pervasives.compare x y
let compare (x:t) y = Stdlib.compare x y
let hash (x:t) = Hashtbl.hash x
(* the type ab is a standard functional type, thus copying and rehashing
are simply identity. Rehashing is used when marshaling. *)
......@@ -1968,7 +1968,7 @@ module Poly_ab =
| A _, B _ | B _, A _ -> false
let mk_compare f x y = match x, y with
| A x, A y -> f x y
| B x, B y -> Pervasives.compare x y
| B x, B y -> Stdlib.compare x y
| A _, B _ -> 1
| B _, A _ -> -1
let mk_hash f = function A x -> f x | B x -> 257 * x
......
......@@ -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@
......
......@@ -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"
......
......@@ -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
......
......@@ -306,8 +306,8 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
if hashed_node == tentative_new_node
then begin
if current_counter = max_int
then Kernel.fatal "Offsetmap(%s): internal maximum exeeded" V.name;
counter := Transitioning.Stdlib.succ current_counter;
then Kernel.fatal "Offsetmap(%s): internal maximum exceeded" V.name;
counter := Stdlib.succ current_counter;
end;
hashed_node
......
......@@ -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
......
......@@ -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))
......
......@@ -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}
......
......@@ -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)
......
......@@ -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@]@;}"
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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 =
......
......@@ -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
......
......@@ -338,8 +338,6 @@ struct
(** {3 String} *)
(* ************************************************************************ *)
module Pervasives_string = String
module String
(X: sig include Parameter_sig.Input_with_arg val default: string end) =
struct
......@@ -711,7 +709,7 @@ struct
(* return the list of tokens, in reverse order *)
let parse s =
let len = Pervasives_string.length s in
let len = Stdlib.String.length s in
let rec aux acc pos i s =
if i = len then acc
else
......@@ -730,7 +728,7 @@ struct
read_char_in_word
(fun acc -> add_char c (add_char '\\' acc)) (Word false)
in
match Pervasives_string.get s i, pos with
match Stdlib.String.get s i, pos with
| '+', Start when use_category ->
aux (add_action Add acc) (Word true) next s
| '-', Start when use_category ->
......@@ -1552,7 +1550,7 @@ struct
in
let r = Str.regexp "[^:]:[^:]" in
let split_delim d =
(Pervasives_string.sub d 0 1, Pervasives_string.sub d 2 1)
(Stdlib.String.sub d 0 1, Stdlib.String.sub d 2 1)
in
let remove_none_and_rev l =
List.fold_left
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment