Move warnings from file to file+out

GillianPlatform · May 9, 2024 · 87a896e · 87a896e
1 parent dd2838c
commit 87a896e
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 17 deletions.
diff --git 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
@@ -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
@@ -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 =