From e58920f9bc7a326a99734566e3feafe53e222ef4 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 6 May 2021 17:29:47 +0200
Subject: [PATCH] Remove temporary files only in app mode (keep them with
verbosity activated).
---
config.ml | 4 ++--
engine.ml | 8 ++++----
marabou.ml | 2 +-
utils.ml | 14 ++++++++++++++
utils.mli | 9 +++++++++
5 files changed, 30 insertions(+), 7 deletions(-)
create mode 100644 utils.ml
create mode 100644 utils.mli
diff --git a/config.ml b/config.ml
index cad1681..16631e3 100644
--- a/config.ml
+++ b/config.ml
@@ -41,7 +41,7 @@ let exe_path_of_solver solver =
with End_of_file -> false, S.exe_name
in
Stdlib.close_in in_channel;
- Sys.remove tmp;
+ Utils.remove_on_app_mode tmp;
if found
then Ok exe
else begin
@@ -167,7 +167,7 @@ let detect_default_solvers () =
Stdlib.close_in in_channel;
Buffer.contents buf
in
- Sys.remove tmp;
+ Utils.remove_on_app_mode tmp;
if retcode <> 0
then begin
Logs.info (fun m -> m "No solver `%s' found." S.name);
diff --git a/engine.ml b/engine.ml
index f871123..b95cab0 100644
--- a/engine.ml
+++ b/engine.ml
@@ -45,7 +45,7 @@ let check_availability solver config =
let retcode = Sys.command cmd in
let in_channel = Stdlib.open_in tmp in
Stdlib.close_in in_channel;
- Sys.remove tmp;
+ Utils.remove_on_app_mode tmp;
if retcode = 0
then
Ok ()
@@ -199,7 +199,7 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
Logs.info (fun m -> m "Executing command `%s'." cmd);
try
let retcode = Sys.command cmd in
- Sys.remove prop;
+ Utils.remove_on_app_mode prop;
if retcode <> 0
then Error (Format.sprintf "Command `%s' has failed." cmd)
else begin
@@ -207,14 +207,14 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
let result = extract_result solver ~log ~output in
Logs.app (fun m -> m "Result of `%s': %a."
task.id Solver.Result.pretty result);
- Sys.remove output;
+ Utils.remove_on_app_mode output;
if Solver.Result.equal result Solver.Result.Failure
then
Logs.app (fun m ->
m "See error messages in `%s' for more information."
log)
else
- Sys.remove log;
+ Utils.remove_on_app_mode log;
Ok result
end
with _ ->
diff --git a/marabou.ml b/marabou.ml
index 1fbe98f..d39ba2d 100644
--- a/marabou.ml
+++ b/marabou.ml
@@ -33,7 +33,7 @@ let options ~model ~property ~output =
| Some Info -> 1
| Some Debug -> 2
in
- [ "--property"; property;
+ [ "--property"; property;
"--input"; model;
"--verbosity"; Int.to_string verbosity_level;
"--summary-file"; output ]
diff --git a/utils.ml b/utils.ml
new file mode 100644
index 0000000..b3de56d
--- /dev/null
+++ b/utils.ml
@@ -0,0 +1,14 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+let remove_on_app_mode filename =
+ let is_app =
+ match Logs.level () with
+ | Some App -> true
+ | _ -> false
+ in
+ if is_app
+ then Sys.remove filename
diff --git a/utils.mli b/utils.mli
new file mode 100644
index 0000000..be657a8
--- /dev/null
+++ b/utils.mli
@@ -0,0 +1,9 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+(** [remove_on_app_mode filename] removes the given file from the file system
+ when caisar is run in application mode only. *)
+val remove_on_app_mode: string -> unit
--
GitLab