From 5eeeff9d266e4d31d020ab864dcaccd58573e8ab Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Wed, 22 Jan 2025 11:21:43 +0100 Subject: [PATCH] [Kernel] minor Filepath-related refactoring --- src/kernel_internals/runtime/special_hooks.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml index 1949120e83..9f6972f462 100644 --- a/src/kernel_internals/runtime/special_hooks.ml +++ b/src/kernel_internals/runtime/special_hooks.ml @@ -149,24 +149,23 @@ let () = Extlib.safe_at_exit time (* Save Frama-c on disk if required *) let save_binary error_extension = if not (Kernel.SaveState.is_empty ()) then begin - let filename = Kernel.SaveState.get () in + let path = Kernel.SaveState.get () in Kernel.SaveState.clear (); - let realname = + let realpath = match error_extension with - | None -> filename + | None -> path | Some err_ext -> - let s = (filename:>string) ^ err_ext in - let path = Filepath.Normalized.of_string s in + let err_path = Filepath.Normalized.extend path err_ext in Kernel.warning "attempting to save on non-zero exit code: \ - modifying filename into `%s'." (Filepath.relativize s); - path + modifying filename into `%a'." Filepath.Normalized.pretty err_path; + err_path in try - Project.save_all realname + Project.save_all realpath with Project.IOError s -> Kernel.error "problem while saving to file %a (%s)." - Filepath.Normalized.pretty realname s + Filepath.Normalized.pretty realpath s end let () = (* implement a refinement of the behavior described in BTS #1388: -- GitLab