From fb92abc2904021e5ec3f7bf075b25bf305a97c14 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 10 Nov 2023 19:24:20 +0100 Subject: [PATCH] Rename NonTerminating -> Termination --- scripts/update_suite.rb | 2 +- src/analyses/loopTermination.ml | 4 ++-- src/common/util/messageCategory.ml | 10 +++++----- src/common/util/options.schema.json | 6 +++--- src/framework/constraints.ml | 4 ++-- src/framework/control.ml | 2 +- 6 files changed, 14 insertions(+), 14 deletions(-) diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index a7d60b5c21..bbf1a71a9d 100755 --- a/scripts/update_suite.rb +++ b/scripts/update_suite.rb @@ -145,7 +145,7 @@ def collect_warnings @vars = $1 @evals = $2 end - if l =~ /\[NonTerminating\]/ then warnings[-1] = "nonterm" end # Get NonTerminating warning + if l =~ /\[Termination\]/ then warnings[-1] = "nonterm" end # Get Termination warning next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?(?:-(?:\d+)(?:\:\d+)?)?\)/ obj,i = $1,$2.to_i diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index 077615ad10..f4db165795 100644 --- a/src/analyses/loopTermination.ml +++ b/src/analyses/loopTermination.ml @@ -49,7 +49,7 @@ struct let finalize () = (* Multithreaded *) if not (!single_thread) then ( - M.warn ~category:NonTerminating "The program might not terminate! (Multithreaded)\n" + M.warn ~category:Termination "The program might not terminate! (Multithreaded)\n" ) (** Recognizes a call of [__goblint_bounded] to check the EvalInt of the @@ -64,7 +64,7 @@ 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 ( - M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:NonTerminating "The program might not terminate! (Loop analysis)" + M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:Termination "The program might not terminate! (Loop analysis)" ); () with Not_found -> diff --git a/src/common/util/messageCategory.ml b/src/common/util/messageCategory.ml index ba589db8d0..41c9bc08e1 100644 --- a/src/common/util/messageCategory.ml +++ b/src/common/util/messageCategory.ml @@ -46,7 +46,7 @@ type category = | Imprecise | Witness | Program - | NonTerminating + | Termination [@@deriving eq, ord, hash] type t = category [@@deriving eq, ord, hash] @@ -205,7 +205,7 @@ let should_warn e = | Imprecise -> "imprecise" | Witness -> "witness" | Program -> "program" - | NonTerminating -> "nonTerminating" + | Termination -> "termination" (* Don't forget to add option to schema! *) in get_bool ("warn." ^ (to_string e)) @@ -226,7 +226,7 @@ let path_show e = | Imprecise -> ["Imprecise"] | Witness -> ["Witness"] | Program -> ["Program"] - | NonTerminating -> ["NonTerminating"] + | Termination -> ["Termination"] let show x = String.concat " > " (path_show x) @@ -266,7 +266,7 @@ let categoryName = function | Overflow -> "Overflow"; | DivByZero -> "DivByZero") | Float -> "Float" - | NonTerminating -> "NonTerminating" + | Termination -> "Termination" let from_string_list (s: string list) = @@ -287,7 +287,7 @@ let from_string_list (s: string list) = | "imprecise" -> Imprecise | "witness" -> Witness | "program" -> Program - | "nonTerminating" -> NonTerminating + | "termination" -> Termination | _ -> Unknown let to_yojson x = `List (List.map (fun x -> `String x) (path_show x)) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index c6e00d3da3..0b6f8b649f 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2105,9 +2105,9 @@ "type": "boolean", "default": true }, - "nonTerminating": { - "title": "warn.nonTerminating", - "description": "Non Termination warning", + "termination": { + "title": "warn.termination", + "description": "Non-Termination warning", "type": "boolean", "default": true }, diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 6ba31488de..b1bbc73660 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1689,7 +1689,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; - M.warn ~category:NonTerminating "The program might not terminate! (Longjmp)" + M.warn ~category:Termination "The program might not terminate! (Longjmp)" ); S.D.bot () | _ -> S.special conv_ctx lv f args @@ -1774,7 +1774,7 @@ struct AnalysisState.svcomp_may_not_terminate := true; (*set the indicator for a non-terminating program for the sv comp*) (*Cycle found*) 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*) + M.warn ~loc ~category:Termination "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 ae1cb3e2b3..a78f125eae 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -146,7 +146,7 @@ struct let fundec_live = live fi fname in if ( not (BatISet.is_empty fundec_live)) then ( AnalysisState.svcomp_may_not_terminate := true; - M.warn ~loc:(M.Location.CilLocation l) ~category:NonTerminating "The program might not terminate! (Upjumping Goto)"); + M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)"); ) (!live_lines)) (!Cilfacade.upjumping_gotos);