diff --git a/Makefile.generating b/Makefile.generating index cf8a8c5d903a178d1f0156172b4bd7a183861a26..d123d7d505a7d07b91986efb572be57f37bf83ee 100644 --- a/Makefile.generating +++ b/Makefile.generating @@ -126,7 +126,10 @@ src/libraries/stdlib/transitioning.ml: \ src/libraries/stdlib/transitioning.ml.in \ Makefile.generating share/Makefile.config rm -f $@ - sed -e 's/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g' $< > $@ + sed \ + -e 's/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g' \ + -e 's/@STACK_FOLD@/$(STACK_FOLD)/g' \ + $< > $@ $(CHMOD_RO) $@ ################## diff --git a/configure.in b/configure.in index dc1373cb62ea412f59f68791654c8c1bc9e5155d..34ccef60b48a8baa3e646a4504142a5b580c92e2 100644 --- a/configure.in +++ b/configure.in @@ -114,10 +114,21 @@ case $OCAMLVERSION in esac AC_SUBST(SPLIT_ON_CHAR) +AC_SUBST(STACK_FOLD) case $OCAMLVERSION in - 4.02.*|4.03.*) SPLIT_ON_CHAR=split_on_char;; - *) SPLIT_ON_CHAR=String.split_on_char;; + 4.02.*) + SPLIT_ON_CHAR=split_on_char; + STACK_FOLD=stack_fold + ;; + 4.03.*) + SPLIT_ON_CHAR=split_on_char; + STACK_FOLD=Stack.fold + ;; + *) + SPLIT_ON_CHAR=String.split_on_char; + STACK_FOLD=Stack.fold + ;; esac # Ocaml library path diff --git a/share/Makefile.config.in b/share/Makefile.config.in index df7ad29fe55c68e9995ed17b7013fe50c247ad85..ca647d3ce136d06ba2b53171954c12e456350cc7 100644 --- a/share/Makefile.config.in +++ b/share/Makefile.config.in @@ -86,6 +86,7 @@ DEVELOPMENT ?=@DEVELOPMENT@ # Compatibility across OCaml versions SPLIT_ON_CHAR ?= @SPLIT_ON_CHAR@ +STACK_FOLD ?= @STACK_FOLD@ ############# # Libraries # diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml index 1f73a5603afeb0d970587fa152c8226bc393d54e..ea0d3451d59c3481a2597317f9a35e09799b75c6 100644 --- a/src/kernel_services/ast_transformations/inline.ml +++ b/src/kernel_services/ast_transformations/inline.ml @@ -115,7 +115,7 @@ let inliner functions_to_inline = object (self) method private recursive_call_limit kf = let nb_calls = - Stack.fold + Transitioning.Stack.fold (fun res kf' -> if Cil_datatype.Kf.equal kf kf' then res + 1 else res) 0 call_stack in diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in index 6d7815b5b3858d72bfb8da1973e318e3ffcc4e5c..147ffcf58cc62c126baa0f78bf37202063360052 100644 --- a/src/libraries/stdlib/transitioning.ml.in +++ b/src/libraries/stdlib/transitioning.ml.in @@ -31,9 +31,16 @@ let split_on_char c s = in aux [] s -(* the implementation above is only used in case we compile against an +let stack_fold f x s = + let res = ref x in + let do_it y = res := f !res y in + Stack.iter do_it s; + !res + +(* the implementations above are only used in case we compile against an old OCaml version. Avoid unused warning in other cases. *) -let _ = split_on_char +let _: char -> string -> string list = split_on_char +let _: ('a -> 'b -> 'a) -> 'a -> 'b Stack.t -> 'a = stack_fold [@@@ warning "-3"] @@ -50,6 +57,10 @@ module Char = struct let lowercase_ascii = Char.lowercase end +module Stack = struct + let fold = @STACK_FOLD@ +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 dc7314a0e342e4d0e12b66be80e399bd57736134..b2817c9bb4cc00ba8d6b937ed1e7fa602e48de80 100644 --- a/src/libraries/stdlib/transitioning.mli +++ b/src/libraries/stdlib/transitioning.mli @@ -25,11 +25,13 @@ the oldest OCaml version officially supported by Frama-C. Be sure to update it when support for a given version is dropped. - Functions are grouped according to the version in which the replacing - feature did appear. + Functions are grouped according to the module of the stdlib they + emulate. The mentioned OCaml version indicate when the function was + introduced in the stdlib (i.e. when Frama-C requires a version higher + than that, it can safely be removed from Transitioning). *) -(** {1 4.03.0} *) +(** {1 OCaml} *) (** In OCaml 4.03, many functions [f] from String have been deprecated in favor of [f_ascii], which operate only on the ASCII charset, while @@ -39,20 +41,24 @@ the stdlib version *) module String: sig - val uppercase_ascii: string -> string - val capitalize_ascii: string -> string - val uncapitalize_ascii: string -> string - val lowercase_ascii: string -> string - val split_on_char: char -> string -> string list + val uppercase_ascii: string -> string (** 4.03 *) + val capitalize_ascii: string -> string (** 4.03 *) + val uncapitalize_ascii: string -> string (** 4.03 *) + val lowercase_ascii: string -> string (** 4.03 *) + val split_on_char: char -> string -> string list (** 4.04 *) end (** See above documentation for [String] *) module Char: sig - val uppercase_ascii: char -> char - val lowercase_ascii: char -> char + val uppercase_ascii: char -> char (** 4.03 *) + val lowercase_ascii: char -> char (** 4.03 *) end -(** {1 Zarith 1.5} *) +module Stack: sig + val fold: ('a -> 'b -> 'a) -> 'a -> 'b Stack.t -> 'a (** 4.03 *) +end + +(** {1 Zarith} *) (** Function [Q.to_float] was introduced in Zarith 1.5 *) module Q: sig