diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index ebd8cc54651568285dd359589530d2f8236f8b3a..ec24f15d0b61f92f94f82aea6d843abaad8480d7 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -505,7 +505,7 @@ let silence_cpp_machdep_warnings cmdl = let build_cpp_cmd = function | NoCPP _ | External _ -> None | NeedCPP (f, cmdl, extra_for_this_file, is_gnu_like) -> - if not (Sys.file_exists (f :> string)) then + if not (Filepath.exists f) then Kernel.abort "source file %a does not exist" Filepath.Normalized.pretty f; let debug = Kernel.is_debug_key_enabled Kernel.dkey_parser in @@ -602,7 +602,7 @@ let abort_with_detailed_pp_message f cpp_command = let parse_cabs cpp_command = function | NoCPP f -> - if not (Sys.file_exists (f:>string)) then + if not (Filepath.exists f) then Kernel.abort "preprocessed file %a does not exist" Filepath.Normalized.pretty f; Kernel.feedback "Parsing %a (no preprocessing)" @@ -651,7 +651,7 @@ let parse_cabs cpp_command = function safe_remove_file ppf; (cil,(f,defs)) | External (f,suf) -> - if not (Sys.file_exists (f:>string)) then + if not (Filepath.exists f) then Kernel.abort "file %a does not exist." Filepath.Normalized.pretty f; Kernel.feedback "Parsing %a (external front-end)" diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml index 341b192f35c80ccb8f7b95976987bd2d6845327e..9524edda4888b72a0e631cef9dddcf5890d1bc57 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.ml +++ b/src/kernel_services/plugin_entry_points/dynamic.ml @@ -99,7 +99,7 @@ let is_package = let is_file base ext = let file = base ^ ext in - if Sys.file_exists file then Some file else None + if (Filepath.exists (Filepath.Normalized.of_string file)) then Some file else None let is_object base = if Dynlink.is_native then is_file base ".cmxs" else diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml index fa3be70c5d552d01d6cfbeeec4f3152412eceb93..1e416c731f672063479afa93e1f658c65d140410 100644 --- a/src/kernel_services/plugin_entry_points/plugin.ml +++ b/src/kernel_services/plugin_entry_points/plugin.ml @@ -362,7 +362,7 @@ struct List.fold_left (fun dummy d -> let name = Datatype.Filepath.concat d s in - if Sys.file_exists (name :> string) + if FramacFilepath.exists name then raise (Found name) else dummy) None @@ -424,7 +424,7 @@ struct let filepath = Datatype.Filepath.concat base_dir s_basename in match mode with | `Must_exist -> - if Sys.file_exists (filepath :> string) + if FramacFilepath.exists filepath then filepath else L.abort "there is no file %s in %s directories" (filepath :> string) O.option_name | `Normalize_only -> diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml index 25bce3d1966dfeb61e74aa7eee31ae11463da0ad..1e94eaa7fa1c13fe2e351075f8a71c4e16ebd6c7 100644 --- a/src/plugins/markdown-report/md_gen.ml +++ b/src/plugins/markdown-report/md_gen.ml @@ -562,7 +562,7 @@ let mk_remarks is_draft = Parse_remarks.get_remarks (Mdr_params.Remarks.get ()) else if is_draft then begin let f = Mdr_params.Output.get() in - if Sys.file_exists (f:>string) then begin + if Filepath.exists f then begin Mdr_params.feedback "Re-using pre-existing remarks in draft file %a" Filepath.Normalized.pretty f;