From 87a896e5869b61ccfe6f1cc3ef8f9dc23481e1ad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oscar=20Sj=C3=B6stedt?= <n1ark.officiel@gmail.com>
Date: Thu, 9 May 2024 17:15:24 +0100
Subject: [PATCH] Move warnings from file to file+out

---
 .../engine/Abstraction/LogicPreprocessing.ml  | 20 ++++++++++++-------
 GillianCore/engine/Abstraction/Verifier.ml    | 10 +++++-----
 .../general/g_interpreter.ml                  |  8 +++-----
 3 files changed, 21 insertions(+), 17 deletions(-)

diff --git a/GillianCore/engine/Abstraction/LogicPreprocessing.ml b/GillianCore/engine/Abstraction/LogicPreprocessing.ml
index e03e2cb0..1fa0882e 100644
--- a/GillianCore/engine/Abstraction/LogicPreprocessing.ml
+++ b/GillianCore/engine/Abstraction/LogicPreprocessing.ml
@@ -260,19 +260,25 @@ let unfold_spec
     let posts : Asrt.t list =
       List.concat_map (auto_unfold preds rec_info) sspec.ss_posts
     in
+    let posts_base = posts in
     let posts = List.map Reduction.reduce_assertion posts in
     L.verbose (fun fmt -> fmt "Post admissibility: %s" spec_name);
     L.tmi (fun fmt ->
         fmt "@[<hov 2>Testing admissibility for assertions:@.%a@]"
           (Fmt.list Asrt.pp) posts);
     let posts = List.filter Simplifications.admissible_assertion posts in
-    if posts = [] then
-      Logging.print_to_all
-        Fmt.(
-          str
-            "Unfolding: Postcondition of %s seems invalid, it has been reduced \
-             to no postcondition"
-            spec_name);
+    let posts =
+      match posts with
+      | [] ->
+          Logging.print_to_all
+            Fmt.(
+              str
+                "Unfolding: Postcondition of %s seems invalid, it has been \
+                 reduced to no postcondition - unsing non-simplified form."
+                spec_name);
+          posts_base
+      | posts -> posts
+    in
     List.map
       (fun pre -> Spec.{ sspec with ss_pre = pre; ss_posts = posts })
       pres
diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml
index 49ba3a4d..514bd710 100644
--- a/GillianCore/engine/Abstraction/Verifier.ml
+++ b/GillianCore/engine/Abstraction/Verifier.ml
@@ -316,9 +316,9 @@ struct
         List.iter
           (fun (sspec : Spec.st) ->
             if sspec.ss_posts = [] then
-              Logging.normal (fun m ->
-                  m "Specification without post-condition for function %s"
-                    spec.spec_name))
+              Logging.print_to_all
+                ("Specification without post-condition for function "
+               ^ spec.spec_name))
           spec.spec_sspecs
       in
       L.verbose (fun m ->
@@ -519,8 +519,8 @@ struct
       (rets : SAInterpreter.result_t list) : bool =
     (if rets = [] then
      L.(
-       normal (fun m ->
-           m "WARNING: Function %s evaluates to 0 results." test.name)));
+       print_to_all
+         ("WARNING: Function " ^ test.name ^ " evaluates to 0 results.")));
     let success = List.for_all (analyse_proc_result test flag) rets in
     print_success_or_failure success;
     success
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index 6fd3b65e..8202be65 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -818,11 +818,9 @@ struct
               else
                 let () =
                   if ret = [] && not spec.data.spec_incomplete then
-                    L.normal (fun m ->
-                        m
-                          "Specification of function %s is empty, proceeding \
-                           anyway."
-                          spec.data.spec_name)
+                    L.print_to_all
+                      ("Specification of function " ^ spec.data.spec_name
+                     ^ " is empty, proceeding anyway.")
                 in
 
                 let successes, errors =