Rename NonTerminating -> Termination

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
 

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 ->

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))

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
         },

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

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);