From 0b15281c952a33c54df61d8f29cc806e619e363b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 6 Jan 2025 11:35:14 +0100
Subject: [PATCH] [Kernel] standardize conditions for keeping temporary files
---
src/kernel_internals/parsing/logic_preprocess.mll | 5 +----
src/kernel_services/ast_queries/file.ml | 11 +++++------
2 files changed, 6 insertions(+), 10 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index 110e2b9e04..343154fa50 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -165,10 +165,7 @@
let preprocess_annots suffix cpp outfile =
if !has_annot then begin
- let debug =
- Kernel.debug_atleast 3 ||
- Kernel.is_debug_key_enabled Kernel.dkey_pp_keep_temp_files
- in
+ let debug = Kernel.is_debug_key_enabled Kernel.dkey_pp_keep_temp_files in
let ppname =
try Extlib.temp_file_cleanup_at_exit ~debug "ppannot" suffix
with Extlib.Temp_file_error s ->
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 29627cbff6..48ed407469 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -373,9 +373,10 @@ let pretty_machdep ?fmt ?machdep () =
(** {2 Initializations} *)
(* ************************************************************************* *)
-let create_temp_file ?debug name suffix =
+let create_temp_file name suffix =
+ let debug = Kernel.is_debug_key_enabled Kernel.dkey_pp_keep_temp_files in
let of_string = Filepath.Normalized.of_string in
- try of_string (Extlib.temp_file_cleanup_at_exit ?debug name suffix)
+ try of_string (Extlib.temp_file_cleanup_at_exit ~debug name suffix)
with Extlib.Temp_file_error s ->
Kernel.abort "cannot create temporary file: %s" s
@@ -463,7 +464,6 @@ let build_cpp_cmd = function
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_pp_keep_temp_files in
let add_if_gnu opt =
match is_gnu_like with
| Gnu -> [opt]
@@ -479,7 +479,7 @@ let build_cpp_cmd = function
opt;
[opt]
in
- let ppf = create_temp_file ~debug (Filename.basename (f :> string)) ".i" in
+ let ppf = create_temp_file (Filename.basename (f :> string)) ".i" in
(* Hypothesis: the preprocessor is POSIX compliant,
hence understands -I and -D. *)
let fc_include_args =
@@ -1905,8 +1905,7 @@ let create_rebuilt_project_from_visitor
let f =
let name = "frama_c_project_" ^ prj_name ^ "_" in
let ext = if preprocess then ".c" else ".i" in
- let debug = Kernel.Debug.get () > 0 in
- create_temp_file ~debug name ext
+ create_temp_file name ext
in
let cout = open_out (f :> string) in
let fmt = Format.formatter_of_out_channel cout in
--
GitLab