diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index cd002187e43431277bc588b19294850edaff5c0e..02ed925af56edaf6bd9f2d163523963be355960a 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 a2393c647bb38c8130bafe1cb5283debbb3de66a..5b5ee4a03c0a0fc79671c094b9f2b0df526bdf1e 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 e6976f6deb8a82305b05bfc2df29708236dc5595..2c9418a9254db980617627f9859d20796f8a47db 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 6292a93db464c60761f6981912fdac4a949eebd8..b2ea6e9bf6e0db85d1e1970015e9133a92dccf73 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 b2d1ddff1c55e1e828fe2b87a59df5a4a9676fbc..60293a2379d7727fc783a6061b85c4e5ebc778ed 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 1fdd721413c96da3ddae333ab3014616b02c2e39..85d0d947a81aab89f84bd51736f0198135496186 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 053d1b52b0ea3ec8f3a385482576e20868bb2daa..32d4c8c2c3690afd523cc768515874f2ba7813f3 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 4440b768d7be65fc0ac0278face838658303715e..89f52477debc6c2502dcfc24eb776637a148724e 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 63485ebba93189813c0dfd40c83a2aea4d2c1e22..7a13be06edfa6eefa75872796092c46e78abe1f7 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 *) ()