Simplify warning

goblint · Nov 1, 2023 · a7d02c4 · a7d02c4
1 parent 268d86d
commit a7d02c4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 23 deletions.
diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
@@ -64,12 +64,8 @@ struct
            ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.global ()));
            (* In case the loop is not bounded, a warning is created. *)
            if not (is_bounded) then (
-             let msgs =
-               [(Pretty.dprintf
-                   "The program might not terminate! (Loop analysis)",
-                 Some (M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement))
-                );] in
-             M.msg_group Warning ~category:NonTerminating "Possibly non terminating loops" msgs);
+             M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:NonTerminating "The program might not terminate! (Loop analysis)"
+           );
            ()
          with Not_found ->
            failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable.")

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -1688,12 +1688,7 @@ struct
       List.iter handle_path (S.paths_as_set conv_ctx);
       if !AnalysisState.should_warn && List.mem "termination" @@ get_string_list "ana.activated" then (
         AnalysisState.svcomp_may_not_terminate := true;
-        let msgs =
-          [(Pretty.dprintf
-              "The program might not terminate! (Longjmp)",
-            None
-           );] in
-        M.msg_group Warning ~category:NonTerminating "Possibly non terminating loops" msgs
+        M.warn ~category:NonTerminating "The program might not terminate! (Longjmp)"
       );
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
@@ -1777,11 +1772,8 @@ struct
       if LS.mem call path_visited_calls then (
         AnalysisState.svcomp_may_not_terminate := true; (*set the indicator for a non-terminating program for the sv comp*)
         (*Cycle found*)
-        let msgs =
-          [
-            (Pretty.dprintf "The program might not terminate! (Fundec %a is contained in a call graph cycle)" CilType.Fundec.pretty fundec, Some (M.Location.CilLocation fundec.svar.vdecl));
-          ] in
-        M.msg_group Warning ~category:NonTerminating "Recursion cycle" msgs) (* output a warning for non-termination*)
+        let loc = M.Location.CilLocation fundec.svar.vdecl in
+        M.warn ~loc ~category:NonTerminating "The program might not terminate! (Fundec %a is contained in a call graph cycle)" CilType.Fundec.pretty fundec) (* output a warning for non-termination*)
       else if not (LH.mem global_visited_calls call) then begin
         LH.replace global_visited_calls call ();
         let new_path_visited_calls = LS.add call path_visited_calls in

diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -146,12 +146,7 @@ struct
           let fundec_live = live fi fname in
           if ( not (BatISet.is_empty fundec_live)) then (
             AnalysisState.svcomp_may_not_terminate := true;
-            let msgs =
-              [(Pretty.dprintf
-                  "The program might not terminate! (Upjumping Goto)",
-                Some (M.Location.CilLocation l)
-              );] in
-            M.msg_group Warning ~category:NonTerminating "Possibly non terminating loops" msgs);
+            M.warn ~loc:(M.Location.CilLocation l) ~category:NonTerminating "The program might not terminate! (Upjumping Goto)");
           )
         (!live_lines))
     (!Cilfacade.upjumping_gotos);