From 5a9c1e8c23db2a3e12db1340ddad7e3406914fa2 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 12 Jun 2023 11:29:06 +0200
Subject: [PATCH] prefer OCaml 4.13 new String functions over Extlib's
---
src/kernel_internals/parsing/logic_preprocess.mll | 9 +++++----
src/kernel_internals/typing/cabs2cil.ml | 4 ++--
src/kernel_services/ast_queries/ast_info.ml | 12 ++++++------
src/libraries/utils/filepath.ml | 9 +++++----
src/plugins/gui/pretty_source.ml | 4 ++--
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/variadic/classify.ml | 4 ++--
src/plugins/wp/ProofStrategy.ml | 2 +-
tests/libc/check_compliance.ml | 8 ++++----
9 files changed, 28 insertions(+), 26 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index cd002187e43..02ed925af56 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -122,14 +122,15 @@
let content = Buffer.create 80 in
let rec ignore_content () =
let s = input_line file in
- if not (Extlib.string_prefix annot_beg s) then ignore_content ()
+ if not (String.starts_with ~prefix:annot_beg s) then ignore_content ()
in
let rec get_annot first =
let s = input_line file in
- if Extlib.string_prefix annot_end s then false, Buffer.contents content
- else if Extlib.string_prefix annot_end_nl s then
+ if String.starts_with ~prefix:annot_end s then
+ false, Buffer.contents content
+ else if String.starts_with ~prefix:annot_end_nl s then
true, Buffer.contents content
- else if Extlib.string_prefix annot_end_comment s then begin
+ else if String.starts_with ~prefix:annot_end_comment s then begin
Buffer.add_char content '\n';
false, Buffer.contents content
end else begin
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a2393c647bb..5b5ee4a03c0 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -333,7 +333,7 @@ let get_current_stdheader () =
let rec aux = function
| [] -> ""
| [ s ] -> s
- | s :: l when Extlib.string_prefix ~strict:true "__fc_" s -> aux l
+ | s :: l when String.starts_with ~prefix:"__fc_" s -> aux l
| s :: _ -> s
in
aux !current_stdheader
@@ -9103,7 +9103,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let full_name =
(* Mangled symbols (that is, starting with '_Z') are unique by
construction. No need to add current function name as prefix. *)
- if Extlib.string_prefix ~strict:true "_Z" n
+ if String.starts_with ~prefix:"_Z" n && n <> "_Z"
then n
else !currentFunctionFDEC.svar.vname ^ "_" ^ n
in
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index e6976f6deb8..2c9418a9254 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -450,22 +450,22 @@ let pointed_type ty =
(* ************************************************************************** *)
let can_be_cea_function name =
- Extlib.string_prefix "Frama_" name
+ String.starts_with ~prefix:"Frama_" name
let is_cea_function name =
- Extlib.string_prefix "Frama_C_show_each" name
+ String.starts_with ~prefix:"Frama_C_show_each" name
let is_cea_domain_function name =
- Extlib.string_prefix "Frama_C_domain_show_each" name
+ String.starts_with ~prefix:"Frama_C_domain_show_each" name
let is_cea_dump_function name =
- Extlib.string_prefix "Frama_C_dump_each" name
+ String.starts_with ~prefix:"Frama_C_dump_each" name
let is_cea_dump_file_function name =
- Extlib.string_prefix "Frama_C_dump_each_file" name
+ String.starts_with ~prefix:"Frama_C_dump_each_file" name
let is_cea_builtin name =
- Extlib.string_prefix "Frama_C_builtin" name
+ String.starts_with ~prefix:"Frama_C_builtin" name
let is_frama_c_builtin n =
can_be_cea_function n &&
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 6292a93db46..b2ea6e9bf6e 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -226,7 +226,7 @@ let add_path path =
| Some symb -> symb ^ Buffer.contents buf
let rec skip_dot file_name =
- if Extlib.string_prefix "./" file_name then
+ if String.starts_with ~prefix:"./" file_name then
skip_dot (String.sub file_name 2 (String.length file_name - 2))
else file_name
@@ -237,7 +237,8 @@ let pretty file_name =
let path = insert cwd file_name in
let file_name = path.path_name in
let cwd_name = cwd.path_name in
- if Extlib.string_prefix ~strict:true cwd_name file_name then
+ if String.starts_with ~prefix:cwd_name file_name && cwd_name <> file_name
+ then
let n = 1 + String.length cwd_name in
String.sub file_name n (String.length file_name - n)
else
@@ -255,7 +256,7 @@ let relativize ?base_name file_name =
in
if base_name = file_name then "." else
let base_name = base_name ^ Filename.dir_sep in
- if Extlib.string_prefix base_name file_name then
+ if String.starts_with ~prefix:base_name file_name then
let n = String.length base_name in
let file_name = String.sub file_name n (String.length file_name - n) in
if file_name = "" then "." else file_name
@@ -268,7 +269,7 @@ let is_relative ?base_name file_name =
| Some b -> (insert cwd b).path_name
in
base_name = file_name
- || Extlib.string_prefix (base_name ^ Filename.dir_sep) file_name
+ || String.starts_with ~prefix:(base_name ^ Filename.dir_sep) file_name
(* -------------------------------------------------------------------------- *)
(* --- Normalized Typed Module --- *)
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index b2d1ddff1c5..60293a2379d 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -260,14 +260,14 @@ let buffer_formatter state source =
let emit_open_tag s =
let s = Extlib.format_string_of_stag s in
(* Ignore tags that are not ours *)
- if Extlib.string_prefix "guitag:" s then
+ if String.starts_with ~prefix:"guitag:" s then
Stack.push (source#end_iter#offset, Tag.find s) starts ;
""
in
let emit_close_tag s =
let s = Extlib.format_string_of_stag s in
(try
- if Extlib.string_prefix "guitag:" s then
+ if String.starts_with ~prefix:"guitag:" s then
let (p,sid) = Stack.pop starts in
Locs.add state (p, source#end_iter#offset) sid
with Stack.Empty -> (* This should probably be a hard error *)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 1fdd721413c..85d0d947a81 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -512,7 +512,7 @@ let pretty_used_files used_files =
let used_included_c_files =
Datatype.Filepath.Set.filter
(fun f ->
- Extlib.string_suffix ~strict:true ".c"
+ String.ends_with ~suffix:".c"
(f : Filepath.Normalized.t :> string))
used_included_files
in
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 053d1b52b0e..32d4c8c2c36 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -113,7 +113,7 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
let is_frama_c_builtin name =
Ast_info.is_frama_c_builtin name ||
Cil_builtins.Builtin_functions.mem name ||
- Extlib.string_prefix "__FRAMAC_" name (* Mthread prefixes *)
+ String.starts_with ~prefix:"__FRAMAC_" name (* Mthread prefixes *)
let va_builtins = [
"__builtin_va_start";
@@ -162,7 +162,7 @@ let classify_std env vi = match vi.vname with
(* stropts.h *)
| "ioctl" -> mk_overload env ["__va_ioctl_void" ; "__va_ioctl_int" ; "__va_ioctl_ptr"]
- | n when Extlib.string_prefix "__sync_" n -> Misc
+ | n when String.starts_with ~prefix:"__sync_" n -> Misc
| n when is_va_builtin n -> Misc
| n when is_frama_c_builtin n -> Builtin
(* Anything else *)
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 4440b768d7b..89f52477deb 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -546,7 +546,7 @@ let configure tactic sigma (a,v) =
let subgoal (children : (string loc * string loc) list)
(default : string loc option) (goal,node) =
let hint = List.find_map (fun (g,s) ->
- if Extlib.string_prefix g.value goal then Some s else None
+ if String.starts_with ~prefix:g.value goal then Some s else None
) children in
begin
match hint, default with
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 63485ebba93..7a13be06edf 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -19,7 +19,7 @@ class stdlib_visitor = object
Cil.SkipChildren
| attrparams ->
let when_header = function
- | AStr s when Extlib.string_suffix ".h" s -> Some s
+ | AStr s when String.ends_with ~suffix:".h" s -> Some s
| _ -> None
in
let headers = List.filter_map when_header attrparams
@@ -81,9 +81,9 @@ struct
end
let ident_to_be_ignored id headers =
- Extlib.string_prefix "__" id ||
- Extlib.string_prefix "Frama_C" id ||
- List.filter (fun h -> not (Extlib.string_prefix "__fc" h)) headers = []
+ String.starts_with ~prefix:"__" id ||
+ String.starts_with ~prefix:"Frama_C" id ||
+ List.filter (fun h -> not (String.starts_with ~prefix:"__fc" h)) headers = []
let check_ident c11 posix glibc nonstandard c11_headers id headers =
if ident_to_be_ignored id headers then (* nothing to check *) ()
--
GitLab