diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index 61034a57c0..077615ad10 100644 --- 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 index 963e6e4996..307f6d0260 100644 --- 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 index 65eda50f03..8768fa00c9 100644 --- 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);