diff --git a/bin/migration_scripts/potassium2calcium.sh b/bin/migration_scripts/potassium2calcium.sh
new file mode 100644
index 0000000000000000000000000000000000000000..b927f2094eee56786f785f1bdd81bae323ab9dfe
--- /dev/null
+++ b/bin/migration_scripts/potassium2calcium.sh
@@ -0,0 +1,159 @@
+#! /bin/sh
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 19 Potassium to Frama-C 20 Calcium,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't work if a directory name contains spaces
+# - doesn't follow symbolic links to directories
+
+ARGS=$@
+
+DIR=
+
+# verbosing on by default
+VERBOSE="v"
+
+sedi ()
+{
+ if [ -n "`sed --help 2> /dev/null | grep \"\\-i\" 2> /dev/null`" ]; then
+ sed -i "$@"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" > $new_temp
+ eval last=\${$#}
+ mv $new_temp $last
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+safe_goto ()
+{
+ dir=$1
+ cd $dir
+ $3
+ cd $2
+}
+
+goto ()
+{
+ if [ -d $1 ]; then
+ safe_goto $1 $2 $3
+ else
+ echo "Directory '$1' does not exist. Omitted."
+ fi
+}
+
+process_file ()
+{
+ file=$1
+ if [ "$VERBOSE" ]; then
+ echo "Processing file $file"
+ fi
+ sedi \
+ -e "s/Transitioning\.Char\./Char./g" \
+ -e "s/Transitioning\.List\./List./g" \
+ -e "s/Transitioning\.Stack\./Stack./g" \
+ -e "s/Transitioning\.String\./String./g" \
+ $file
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in `ls -p1 *.ml* 2> /dev/null`; do
+ process_file $f
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ for d in `ls -p1 | grep \/`; do
+ safe_goto $d .. apply_recursively
+ done
+}
+
+applying_to_list ()
+{
+ dirs
+ tmpdir=`pwd`
+ for d in $DIR; do
+ goto $d $tmpdir $1
+ done
+}
+
+help ()
+{
+ echo "Usage: $0 [options | directories]
+
+Options are:
+ -r | --recursive Check subdirectories recursively
+ -h | --help Display help message
+ -q | --quiet Quiet mode (i.e. non-verbose mode)
+ -v | --verbose Verbose mode (default)"
+ exit 0
+}
+
+error ()
+{
+ echo "$1.
+Do \"$0 -h\" for help."
+ exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+ case $1 in
+ -r | --recursive) FN="apply_recursively";;
+ -h | -help ) help; exit 0;;
+ -q | --quiet ) VERBOSE=;;
+ -v | --verbose ) VERBOSE="v";;
+ -* ) error "Invalid option $1";;
+ * ) DIR="$DIR $1";;
+ esac
+}
+
+cmd_line ()
+{
+ for s in $ARGS; do
+ parse_arg $s
+ done
+ applying_to_list $FN
+}
+
+cmd_line
+exit 0
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 9980f89dcdfe404757752447e6b72dde4359b3ad..3122754828ca3e15fde4e1639383cf1020d7e878 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -39,6 +39,7 @@ bin/migration_scripts/silicon2phosphorus.sh: CEA_LGPL
bin/migration_scripts/sodium2magnesium.sh: CEA_LGPL
bin/migration_scripts/sulfur2chlorine.sh: CEA_LGPL
bin/migration_scripts/chlorine2argon.sh: CEA_LGPL
+bin/migration_scripts/potassium2calcium.sh: CEA_LGPL
bin/sed_get_binutils_version: .ignore
bin/sed_get_make_major: .ignore
bin/sed_get_make_minor: .ignore
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 248d57078c094a74bcb2b58d5e0e205361a7d307..eaa9455b742e798965fc88a2a3a954ae384b7378 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -267,7 +267,7 @@ module D =
Printer.pp_exp e1 Printer.pp_exp e2
| Overflow(s, e, n, b) ->
Format.fprintf fmt "%s(@[%a@]@ %s@ @[%a@])"
- (Transitioning.String.capitalize_ascii (string_of_overflow_kind s))
+ (String.capitalize_ascii (string_of_overflow_kind s))
Printer.pp_exp e
(match b with Lower_bound -> ">=" | Upper_bound -> "<=")
Datatype.Integer.pretty n
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 89aa33d86d8b8a8a3a4f54683bd4f00bb9cb8e63..5a6609bd9286495e50cc7fd494fb58ace0d14c7d 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -210,7 +210,7 @@ let pp_active fmt active =
(Datatype.String.Set.elements active)
let pp_capitalize fmt s =
- Format.pp_print_string fmt (Transitioning.String.capitalize_ascii s)
+ Format.pp_print_string fmt (String.capitalize_ascii s)
let pp_acsl_extension fmt {ext_name} = pp_capitalize fmt ext_name
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 3336c5689deedb7cdd84be114b579018336b20f0..186a56d4cdde06ea54acfab703738e1d4f71616e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4149,7 +4149,7 @@ let parseIntAux (str:string) =
fun s ->
let ls = String.length s in
l >= ls &&
- s = Transitioning.String.uppercase_ascii (String.sub str (l - ls) ls)
+ s = String.uppercase_ascii (String.sub str (l - ls) ls)
in
let l = String.length str in
(* See if it is octal or hex or binary *)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index d285dd4aad183f31f097f26137385be5372262b7..9fd8da5e14f15e9d52bee6b56c65cc7952b1058a 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -320,7 +320,7 @@ let machdep_macro = function
| "ppc_32" -> "__FC_MACHDEP_PPC_32"
| "msvc_x86_64" -> "__FC_MACHDEP_MSVC_X86_64"
| s ->
- let res = "__FC_MACHDEP_" ^ (Transitioning.String.uppercase_ascii s) in
+ let res = "__FC_MACHDEP_" ^ (String.uppercase_ascii s) in
Kernel.warning ~once:true
"machdep %s has no registered macro. Using %s for pre-processing" s res;
res
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 80d58f94a723675aa5ed962b95db0e2df9f41cfa..a0e404dd1c1e4b9dbb93575eed84077c85fd176d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -339,7 +339,7 @@ module Lenv = struct
| BuiltinLabel LoopEntry -> Some "LoopEntry"
| StmtLabel s ->
(match
- Transitioning.List.find_opt
+ List.find_opt
(function Label (_,_,b) -> b | _ -> false) !s.labels
with
| None -> None
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 5c66aa85fed221f13978b198d373ee386d6115ea..ff499c760d6de4c292557b209eddd1709cacca0b 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -288,7 +288,7 @@ let string_to_float_lconstant string =
constant and the nearest parsed float is exact. Otherwise, use the upper
and lower float computed by [parse]. *)
let l = String.length string - 1 in
- let last = Transitioning.Char.uppercase_ascii string.[l] in
+ let last = Char.uppercase_ascii string.[l] in
let exact = last = 'F' || last = 'D' in
if exact
then LReal (real_of_float string f.Floating_point.f_nearest)
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index ea63e968b7c1392aa4b18bf91fb9aecf8db1d505..cb00a64b313a8dc77930c56db256653944770fa7 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -190,7 +190,7 @@ let inliner functions_to_inline = object (self)
method private recursive_call_limit kf =
let nb_calls =
- Transitioning.Stack.fold
+ 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/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index b49b856b2cdae25c02ad46673bb4a6f67705c47a..4ce267fa0fa69bdbe8ea3b5e0002d9756c714c09 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -972,7 +972,7 @@ let plugin_help shortname =
if newline then Format.pp_print_newline fmt ();
if s <> "" then
Format.fprintf fmt "@[*** %s@]@\n@\n"
- (Transitioning.String.uppercase_ascii s);
+ (String.uppercase_ascii s);
ignore (print_options !o)
in
print_group false g;
@@ -1012,7 +1012,7 @@ let list_plugins () =
(fun p ->
if p.Plugin.name <> "" then
print_helpline fmt
- (Transitioning.String.capitalize_ascii p.Plugin.name)
+ (String.capitalize_ascii p.Plugin.name)
(Printf.sprintf "%s (-%s-h)" p.Plugin.help p.Plugin.short)
"")
(Plugin.all_plugins ()) ;
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 0ad27f1c620c9e031ffb609d6aef8137b112b343..10241320736c4495275430db1a8a6ac2bbecc563 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -329,7 +329,7 @@ let load_module m =
if is_package m && mem_package m then load_packages [m]
else
let fc =
- "frama-c-" ^ Transitioning.String.lowercase_ascii m
+ "frama-c-" ^ String.lowercase_ascii m
in
if mem_package fc then load_packages [fc]
else Klog.error "package or module '%s' not found" m
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
index cec362c256961bb8d530fbf329aad550db0f70cf..c7ad5bf6e4dbc4124a8ce4adbb265e21ba5d0996 100644
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ b/src/kernel_services/plugin_entry_points/journal.ml
@@ -155,7 +155,7 @@ let print_trailer fmt =
Format.fprintf fmt "@[(* Registering *)@]@\n";
Format.fprintf fmt
"@[<hv 2>let main : unit -> unit =@;@[<hv 2>Dynamic.register@;~plugin:%S@;\"main\"@;"
- (Transitioning.String.capitalize_ascii (Filename.basename (get_name ())));
+ (String.capitalize_ascii (Filename.basename (get_name ())));
Format.fprintf fmt
"@[<hv 2>(Datatype.func@;Datatype.unit@;Datatype.unit)@]@;";
Format.fprintf fmt "~journalize:false@;main@]@]@\n@\n";
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index da8b3426d7743580f633840a8657d6120fabeeb6..fc75685ce07eb58dc3edc72419e55ec23d16216b 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -718,7 +718,7 @@ let rec split_joker = function
| ""::w -> split_joker w
| a::w -> a::split_joker w
-let split_category s = split_joker (Transitioning.String.split_on_char ':' s)
+let split_category s = split_joker (String.split_on_char ':' s)
let evt_category = function
| { evt_category = None } -> []
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 1ba3d14939cbf54d60a458a8055c5add286e537a..f24bdbcfb2680fd819c456b99b0c6d7ca87c8dd9 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -519,7 +519,7 @@ struct
else
let str = if str = "" then default_kinds_str else str in
let has_ch c =
- CamlString.contains str (Transitioning.Char.lowercase_ascii c)
+ CamlString.contains str (Char.lowercase_ascii c)
in
let list_of_bool b e = if b then [e] else [] in
let kinds =
@@ -657,7 +657,7 @@ struct
else
L.set_warn_status c s
in
- let directives = Transitioning.String.split_on_char ',' s in
+ let directives = CamlString.split_on_char ',' s in
if List.mem "help" directives then begin
match directives with
| [ "help" ] ->
@@ -666,7 +666,7 @@ struct
| _ -> L.abort "mixing help with warning categories in `%s'" s
end else begin
let parse_single s =
- match Transitioning.String.split_on_char '=' s with
+ match CamlString.split_on_char '=' s with
| [] -> assert false (* split_on_char should return at least an element
even if it is the empty string *)
| [ c ] -> set_status c Log.Wactive
@@ -678,7 +678,7 @@ struct
end
let parse_category s =
- let categories = Transitioning.String.split_on_char ',' s in
+ let categories = CamlString.split_on_char ',' s in
if List.mem "help" categories then Print_help
else begin
let parse_single s =
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 328b9e1a1e39b56e6dc0ed6d23b889c58749eadc..e2f6b9b2cee75b892f392c331698c4075ae3dff9 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -146,7 +146,7 @@ end
let valid_varname s =
let r = Str.regexp "[^A-Za-z0-9_]+" in
let s = Str.global_replace r "__" s in
- Transitioning.String.uncapitalize_ascii s
+ String.uncapitalize_ascii s
let check f fname tname fstr =
assert
@@ -272,7 +272,7 @@ let is_module_name s =
List.for_all
(fun x ->
String.length x > 0 &&
- x.[0] = Transitioning.Char.uppercase_ascii x.[0]) l
+ x.[0] = Char.uppercase_ascii x.[0]) l
module Make(X: Make_input) = struct
@@ -1711,7 +1711,7 @@ end
module Make_with_collections(X: Make_input) =
With_collections
(Make(X))
- (struct let module_name = Transitioning.String.capitalize_ascii X.name end)
+ (struct let module_name = String.capitalize_ascii X.name end)
(* ****************************************************************************)
(** {2 Predefined datatype} *)
@@ -1730,7 +1730,7 @@ module Simple_type
end) =
struct
- let module_name = "Datatype." ^ Transitioning.String.capitalize_ascii X.name
+ let module_name = "Datatype." ^ String.capitalize_ascii X.name
include With_collections
(Make(struct
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index f815f104a071411a50b6eb1501f1b29853fe773e..e14bbd2582c262fe2697232b580f53b8b0bb0465 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -158,18 +158,7 @@ let mapi f l =
snd (List.fold_left (fun (i,acc) x -> (i+1,f i x :: acc)) (0,[]) l)
in List.rev res
-(* Remove duplicates from a sorted list *)
-let list_unique cmp l =
- let rec aux acc = function
- | [] -> acc
- | [e] -> e :: acc
- | e1 :: (e2 :: _ as q) ->
- if cmp e1 e2 = 0 then aux acc q else aux (e1 :: acc) q
- in
- List.rev (aux [] l)
-
-(* Remove once OCaml 4.02 is mandatory *)
-let sort_unique cmp l = list_unique cmp (List.sort cmp l)
+let sort_unique cmp l = List.sort_uniq cmp l
let subsets k l =
let rec aux k l len =
@@ -510,8 +499,8 @@ external compare_basic: 'a -> 'a -> int = "%compare"
let compare_ignore_case s1 s2 =
String.compare
- (Transitioning.String.lowercase_ascii s1)
- (Transitioning.String.lowercase_ascii s2)
+ (String.lowercase_ascii s1)
+ (String.lowercase_ascii s2)
(*
Local Variables:
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 86d7bec02790d0ec2ced3af931ab3c239910cc0f..c39327e3e31709ee0ffb0546bcdc13d6f12080f5 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -154,7 +154,9 @@ val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list
@since Oxygen-20120901 *)
val sort_unique: ('a -> 'a -> int) -> 'a list -> 'a list
- (** Same as List.sort , but also remove duplicates. *)
+ (** Same as List.sort , but also remove duplicates.
+ @deprecated use List.sort_uniq instead
+ *)
val subsets: int -> 'a list -> 'a list list
(** [subsets k l] computes the combinations of [k] elements from list [l].
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 8d6603d83658cb5332f9581f468cf998355b61f2..de6215991de78ead186f5deb8cca34095989fb99 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -20,43 +20,6 @@
(* *)
(**************************************************************************)
-let split_on_char c s =
- let rec aux res s =
- if String.contains s c then begin
- let i = String.rindex s c in
- let prefix = String.sub s 0 i in
- let suf = String.sub s (i+1) (String.length s - i - 1) in
- aux (suf::res) prefix
- end else s :: res
- in
- aux [] s
-
-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
-
-let nth_opt l n =
- try Some (List.nth l n)
- with Failure _ when n >= 0 -> None
-(* OCaml manual states that a negative argument still raises a Failure. *)
-
-let find_opt f l = try Some (List.find f l) with Not_found -> None
-
-let assoc_opt x l = try Some (List.assoc x l) with Not_found -> None
-
-let assq_opt x l = try Some (List.assq x l) with Not_found -> None
-
-(* the implementations above are only used in case we compile against an
- old OCaml version. Avoid unused warning in other cases. *)
-let _: char -> string -> string list = split_on_char
-let _: ('a -> 'b -> 'a) -> 'a -> 'b Stack.t -> 'a = stack_fold
-let _: 'a list -> int -> 'a option = nth_opt
-let _: ('a -> bool) -> 'a list -> 'a option = find_opt
-let _: 'a -> ('a * 'b) list -> 'b option = assoc_opt
-let _: 'a -> ('a * 'b) list -> 'b option = assq_opt
-
module Stdlib = struct
(* Pervasives/Stdlib functions *)
let compare = compare
@@ -70,30 +33,6 @@ end
[@@@ warning "-3"]
-module String = struct
- let uppercase_ascii = String.uppercase
- let capitalize_ascii = String.capitalize
- let uncapitalize_ascii = String.uncapitalize
- let lowercase_ascii = String.lowercase
- let split_on_char = @SPLIT_ON_CHAR@
-end
-
-module Char = struct
- let uppercase_ascii = Char.uppercase
- let lowercase_ascii = Char.lowercase
-end
-
-module Stack = struct
- let fold = @STACK_FOLD@
-end
-
-module List = struct
- let nth_opt = @NTH_OPT@
- let find_opt = @FIND_OPT@
- let assoc_opt = @ASSOC_OPT@
- let assq_opt = @ASSQ_OPT@
-end
-
module Dynlink = struct
let init = @DYNLINK_INIT@
end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index ce5dcb612e5176b44181a7ecece45b8413500e53..521cf30c013bf939d5bbecc4444a682620267319 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -33,38 +33,6 @@
(** {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
- the deprecated [f] knew about iso-8859-1.
- We use the new names here, so that when support of 4.02.3 is dropped,
- client code will just have to erase [Transitioning.] to use directly
- the stdlib version
-*)
-module String: sig
- 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 (** 4.03 *)
- val lowercase_ascii: char -> char (** 4.03 *)
-end
-
-module Stack: sig
- val fold: ('a -> 'b -> 'a) -> 'a -> 'b Stack.t -> 'a (** 4.03 *)
-end
-
-module List: sig
- val nth_opt: 'a list -> int -> 'a option (** 4.05 *)
- val find_opt: ('a -> bool) -> 'a list -> 'a option (** 4.05 *)
- val assoc_opt: 'a -> ('a * 'b) list -> 'b option (** 4.05 *)
- val assq_opt: 'a -> ('a * 'b) list -> 'b option (** 4.05 *)
-end
-
(** 4.08 *)
module Stdlib: sig
val compare: 'a -> 'a -> int
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index bc487fe40a9b9459227ff24ded4103019849720f..9d5399133a88d812663316acd729259e4f6585f3 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -258,7 +258,7 @@ let parse string =
then Kernel.fatal ~current:true
"Parsing an empty string as a floating-point constant."
else
- let last = Transitioning.Char.uppercase_ascii string.[l] in
+ let last = Char.uppercase_ascii string.[l] in
let suffix, kind =
match last with
| 'F' -> true, Cil_types.FFloat
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 4edc958567c6e270a7c08fdbf2aa0687b5ac1588..cec5d5568bcd4f32b511967fce6ddd4cba9d595a 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -146,7 +146,7 @@ let preferences (host_window: Design.main_window_extension_points) =
in
let theme_group = new Widget.group "" in
let build_theme_button name =
- let label = Transitioning.String.capitalize_ascii name in
+ let label = String.capitalize_ascii name in
let widget = theme_group#add_radio ~label ~value:name () in
theme_box#add widget#coerce
in
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index 2ca7d6662843869e27bad911ff855e3cba0354ce..94dcf83f767f76631987f681faddc6378c8f3c47 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -149,7 +149,7 @@ let box_plugin p =
let vbox = GPack.vbox ~packing:frame#add () in
let markup =
"<span font_weight=\"bold\">" ^
- Transitioning.String.capitalize_ascii p.Plugin.p_help ^
+ String.capitalize_ascii p.Plugin.p_help ^
"</span>"
in
ignore (GMisc.label ~markup ~packing:(vbox#pack ~padding:15) ());
@@ -159,7 +159,7 @@ let box_plugin p =
(Hashtbl.fold
(fun l g acc ->
if g = [] then acc
- else (Transitioning.String.capitalize_ascii l, g) :: acc)
+ else (String.capitalize_ascii l, g) :: acc)
p.Plugin.p_parameters
[])
in
@@ -287,7 +287,7 @@ let show ?height ?width ~(host:basic_main) () =
Plugin.iter_on_plugins
(fun p ->
plugins :=
- (Transitioning.String.capitalize_ascii p.Plugin.p_name, p)
+ (String.capitalize_ascii p.Plugin.p_name, p)
:: !plugins);
plugins :=
List.sort (fun (n1, _) (n2, _) -> compare_plugin_name n1 n2)!plugins;
diff --git a/src/plugins/print_api/print_interface.ml b/src/plugins/print_api/print_interface.ml
index 4d5c5e934406baa2c8eb7deb0290b75d25463e33..1299cd4a1f7492f3667e0ae4043dd7256da68a60 100644
--- a/src/plugins/print_api/print_interface.ml
+++ b/src/plugins/print_api/print_interface.ml
@@ -60,7 +60,7 @@ let clash_with_compilation_unit =
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ()) Config.compilation_unit_names;
fun s ->
- Hashtbl.mem h s || Hashtbl.mem h (Transitioning.String.lowercase_ascii s)
+ Hashtbl.mem h s || Hashtbl.mem h (String.lowercase_ascii s)
(** Modules can depend on each other, when a value of a given module depend
on a type of another. It is then important to print them in an appropriate
@@ -292,7 +292,7 @@ let print_plugin fmt =
let extern, sub_modules = List.partition (is_submodule key1) deps in
List.iter (print_one_plugin fmt i) extern;
let short_module_name =
- Transitioning.String.capitalize_ascii (get_name i key1)
+ String.capitalize_ascii (get_name i key1)
in
let space_i = space i in
Format.fprintf fmt "\n \n%smodule %s:\n%ssig "
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index 8f7d667899f2fa0b28b3496fffc9ecc3457c4b98..b3d64a8089d95a506170e8d26934969f96338108 100644
--- a/src/plugins/qed/export.ml
+++ b/src/plugins/qed/export.ml
@@ -91,7 +91,7 @@ let sanitize ~to_lowercase base =
Buffer.add_char p c
| 'A' .. 'Z' ->
Buffer.add_char p
- (if to_lowercase then Transitioning.Char.lowercase_ascii c else c)
+ (if to_lowercase then Char.lowercase_ascii c else c)
| _ -> ()
done ;
Buffer.contents p
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index cbb3903021323c0a5452117d0f9228ec2cc81a9a..e7339901ac211f55104164531057580fc1c3e37d 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -21,12 +21,11 @@
(**************************************************************************)
module R = Report_parameters
-module T = Transitioning
type action = SKIP | INFO | ERROR | REVIEW
let action s =
- match T.String.uppercase_ascii s with
+ match String.uppercase_ascii s with
| "INFO" -> INFO
| "ERROR" -> ERROR
| "REVIEW" -> REVIEW
@@ -358,7 +357,7 @@ let monitor_log_event (evt : Log.event) =
Printf.sprintf "%s.unclassified.%s" evt.evt_plugin env.rs_name in
let e_title =
Printf.sprintf "Unclassified %s (Plugin '%s')"
- (T.String.capitalize_ascii env.rs_name) evt.evt_plugin in
+ (String.capitalize_ascii env.rs_name) evt.evt_plugin in
let e_action = action (env.rs_action ()) in
{ unclassified with e_id ; e_title ; e_action } in
monitor ~lookup ~category ~msg ~source unclassified
@@ -449,7 +448,7 @@ let monitor_status properties ip =
let e_id = "unclassified." ^ properties.ps_name in
let e_title = name in
let e_action = properties.ps_action () |> action in
- let e_descr = T.String.capitalize_ascii properties.ps_name ^ " status" in
+ let e_descr = String.capitalize_ascii properties.ps_name ^ " status" in
{ unclassified with e_id ; e_action ; e_title ; e_descr }
in monitor ~lookup ~category:[] ~msg:name ~source unclassified
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index fcf0088095c21fb077679931087e2acb8fae0f9b..68686f72d14cc2cfa28af182e0714db28e980b5b 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -335,7 +335,7 @@ struct
| `Bottom -> None
| `Value (_cache, value) ->
let is_included (_, _, v) = Abstract.Val.is_included v value in
- match Transitioning.List.find_opt is_included expected_values with
+ match List.find_opt is_included expected_values with
| None -> None
| Some (stamp, i, _) ->
if Cvalue.V.cardinal_zero_or_one (get value)
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index a5d78c61b30a2e722f05c9d077547d68858f8b32..83b2a1ea896d0f24bb83a400efe57d02ddf40dff 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -43,7 +43,7 @@ let all_alarms () =
all_red_statuses
in
let kf_name_compare kfname =
- Transitioning.String.uncapitalize_ascii kfname
+ String.uncapitalize_ascii kfname
in
(* Sort by function names, then stmt, then alarms *)
let cmp (k1, ki1, ap1, _) (k2, ki2, ap2, _) =
@@ -82,7 +82,7 @@ let make_red_alarm function_name ki alarm callstacks =
in
let ca, _ = Alarms.to_annot (Kstmt stmt) alarm in
let ip = Property.ip_of_code_annot_single kf stmt ca in
- let kind = Transitioning.String.capitalize_ascii (Alarms.get_name alarm) in
+ let kind = String.capitalize_ascii (Alarms.get_name alarm) in
let p = get_predicate ca in
let acsl = Format.asprintf "@[<hov>%a@]" Cil_datatype.Predicate.pretty p in
let alarm_or_prop = Red_statuses.Alarm alarm in
diff --git a/src/plugins/value/values/numerors/numerors_float.ml b/src/plugins/value/values/numerors/numerors_float.ml
index a080a79ed23030f7fee606fc0868747c9226e17d..9100f86425bfa2d17ac047aea38a3f655111af64 100644
--- a/src/plugins/value/values/numerors/numerors_float.ml
+++ b/src/plugins/value/values/numerors/numerors_float.ml
@@ -101,7 +101,7 @@ let of_float ?(rnd = Rounding.Near) ?(prec = P.Real) f =
let of_string ?(rnd = Rounding.Near) ?(prec = P.Real) str =
prec >>- fun () ->
let l = String.length str - 1 in
- let last = Transitioning.Char.lowercase_ascii str.[l] in
+ let last = Char.lowercase_ascii str.[l] in
let str =
if last = 'f' || last = 'd' || last = 'l'
then String.sub str 0 l
diff --git a/src/plugins/variadic/format_pprint.ml b/src/plugins/variadic/format_pprint.ml
index 7951ada686cc750a931ec160a75b68739e1f567e..b5647efb4456238ee6a5c782a8d0d3e00737dfd1 100644
--- a/src/plugins/variadic/format_pprint.ml
+++ b/src/plugins/variadic/format_pprint.ml
@@ -81,7 +81,7 @@ let string_of_cs = function
let pp_cs ff (cs,capitalize) =
let s = string_of_cs cs in
- let s = if capitalize then Transitioning.String.capitalize_ascii s else s in
+ let s = if capitalize then String.capitalize_ascii s else s in
Format.fprintf ff "%s" s
let string_of_option ?pre:(pre="") ?suf:(suf="") f = function
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index bc76ceb0d8180a2944f420e6fe6386235ca401c4..bb84db892d8f2acec500e3b62b1a5df2a9e36232 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -45,7 +45,7 @@ type driver = LogicBuiltins.driver
let main (i,t) name =
begin
Buffer.add_string i name ;
- Buffer.add_string t (Transitioning.String.capitalize_ascii name) ;
+ Buffer.add_string t (String.capitalize_ascii name) ;
end
let add (i,t) part =
@@ -54,7 +54,7 @@ let add (i,t) part =
Buffer.add_string i part ;
Buffer.add_char t ' ' ;
Buffer.add_char t '(' ;
- Buffer.add_string t (Transitioning.String.capitalize_ascii part) ;
+ Buffer.add_string t (String.capitalize_ascii part) ;
Buffer.add_char t ')' ;
end
@@ -317,7 +317,7 @@ let split ~warning (m:string) : string list =
| _ -> warning (Printf.sprintf
"In model spec %S : unexpected character '%c'" m c)
)
- (Transitioning.String.uppercase_ascii m) ;
+ (String.uppercase_ascii m) ;
flush () ; !tk
let update_config ~warning m s = function
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index daf7778bd2526da530e71141ca830e25b7e56b51..9ad41b022be9291a141253e9c9c0188dbd64da25 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -93,7 +93,7 @@ let parse_c_option opt =
let coqid = Filename.chop_extension (Filename.basename c_file) in
let c_module =
Printf.sprintf "%s.%s" c_name
- (Transitioning.String.capitalize_ascii coqid)
+ (String.capitalize_ascii coqid)
in
{ c_id = opt ; c_source ; c_file ; c_path ; c_name ; c_module }
with Not_found ->
@@ -101,7 +101,7 @@ let parse_c_option opt =
let c_source = Filename.dirname opt in
let c_file = Filename.basename opt in
let c_module =
- Transitioning.String.capitalize_ascii (Filename.chop_extension c_file)
+ String.capitalize_ascii (Filename.chop_extension c_file)
in
{ c_id = opt ; c_source ; c_file ; c_path = "." ; c_name = "" ; c_module }
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index bcad8955a4bf993fb94deaf010e7812c01dc43f6..600dcc6aa68c9ceee193a916fda9a6da8a1f1a1f 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -52,7 +52,7 @@ let cluster_file c =
let theory_name_of_cluster c =
let base = cluster_id c in
- Transitioning.String.capitalize_ascii base
+ String.capitalize_ascii base
let theory_name_of_pid pid = "VC" ^ WpPropId.get_propid pid
@@ -148,13 +148,13 @@ class visitor fmt c =
self#lines ;
let name = (cluster_id c) in
Format.fprintf fmt "use %s.%s@\n"
- name (Transitioning.String.capitalize_ascii name) ;
+ name (String.capitalize_ascii name) ;
deps <- (D_cluster c) :: deps
method add_extlib file =
let thy = filenoext file in
let path = LogicBuiltins.find_lib file in
- self#add_import2 thy (Transitioning.String.capitalize_ascii thy) ;
+ self#add_import2 thy (String.capitalize_ascii thy) ;
self#add_dfile path
method on_library thy =
@@ -163,7 +163,7 @@ class visitor fmt c =
| [file] ->
let filenoext = filenoext file in
self#add_import2 filenoext
- (Transitioning.String.capitalize_ascii filenoext) ;
+ (String.capitalize_ascii filenoext) ;
self#add_dfile file
| [file;lib] ->
self#add_import2 (filenoext file) lib ;
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 254ce3968bef3866356da7b2a2a00c86025aa16e..0c2117f250be3f3a6002cd0087ea63702c5a7883 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -145,7 +145,7 @@ let do_wp_report () =
begin
let stats = WpReport.fcstat () in
begin
- match Transitioning.String.split_on_char ':' jreport with
+ match String.split_on_char ':' jreport with
| [] | [""] -> ()
| [joutput] ->
WpReport.export_json stats ~joutput () ;
diff --git a/src/plugins/wp/why3_api.ml b/src/plugins/wp/why3_api.ml
index 1287186af6f4c34a75f4e4aa8e612e2516ce2291..1d4c70adb6379fd1630c89b060cfdb0c7adf4d44 100644
--- a/src/plugins/wp/why3_api.ml
+++ b/src/plugins/wp/why3_api.ml
@@ -639,7 +639,7 @@ class visitor (ctx:context) c =
method on_cluster c =
let name = Definitions.cluster_id c in
Wp_parameters.debug ~dkey:dkey_api "Start on_cluster %s@." name;
- let th_name = Transitioning.String.capitalize_ascii name in
+ let th_name = String.capitalize_ascii name in
let thy =
let age = try fst (CLUSTERS.find c) with Not_found -> (-1) in
if age < Definitions.cluster_age c then
@@ -714,7 +714,7 @@ class visitor (ctx:context) c =
let filenoext = filenoext file in
copy_file file;
self#add_import2 [filenoext]
- (Transitioning.String.capitalize_ascii filenoext);
+ (String.capitalize_ascii filenoext);
| [file;lib] ->
copy_file file;
self#add_import2 [filenoext file] lib;