Merge branch 'feature/andre/nonterm-warn-categories' into 'master'

[Nonterm] add warn categories

See merge request frama-c/frama-c!2998

src/plugins/nonterm/nonterm_run.ml

@@ -104,13 +104,17 @@ let pp_numbered_stacks fmt callstacks =
             Format.pp_print_int Value_types.Callstack.pretty))
       numbered_callstacks
 
+let wkey_stmt = Self.register_warn_category "stmt"
+
 let warn_nonterminating_statement stmt callstacks =
-  Self.warning ~source:(fst (Stmt.loc stmt))
+  Self.warning ~wkey:wkey_stmt ~source:(fst (Stmt.loc stmt))
     "non-terminating %a@\n%a"
     pretty_stmt_kind stmt pp_numbered_stacks callstacks
 
+let wkey_dead = Self.register_warn_category "dead-code"
+
 let warn_dead_code stmt =
-  Self.warning ~source:(fst (Stmt.loc stmt))
+  Self.warning ~wkey:wkey_dead ~source:(fst (Stmt.loc stmt))
     "%a is syntactically unreachable" pretty_stmt_kind stmt
 
 class dead_cc_collector kf = object
@@ -155,8 +159,10 @@ class dead_cc_collector kf = object
     Cil.DoChildren
 end
 
+let wkey_unreachable = Self.register_warn_category "unreachable"
+
 let warn_unreachable_statement stmt =
-  Self.warning ~source:(fst (Stmt.loc stmt))
+  Self.warning ~wkey:wkey_unreachable ~source:(fst (Stmt.loc stmt))
     "unreachable %a" pretty_stmt_kind stmt
 
 class unreachable_stmt_visitor kf to_ignore = object

src/plugins/nonterm/tests/nonterm/oracle/builtin_termination.res.oracle

@@ -25,7 +25,7 @@
   len1 ∈ {2} or UNINITIALIZED
   len2 ∈ UNINITIALIZED
   __retres ∈ {0}
-[nonterm] tests/nonterm/builtin_termination.c:16: Warning: 
+[nonterm:stmt] tests/nonterm/builtin_termination.c:16: Warning: 
   non-terminating function call
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle

@@ -21,13 +21,13 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/callstack.i:2: Warning: 
+[nonterm:stmt] tests/nonterm/callstack.i:2: Warning: 
   non-terminating loop
   stack: f :: tests/nonterm/callstack.i:7 <-
          g :: tests/nonterm/callstack.i:12 <-
          main
-[nonterm] tests/nonterm/callstack.i:7: Warning: unreachable return
-[nonterm] tests/nonterm/callstack.i:11: Warning: 
+[nonterm:unreachable] tests/nonterm/callstack.i:7: Warning: unreachable return
+[nonterm:stmt] tests/nonterm/callstack.i:11: Warning: 
   non-terminating loop
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/callstacks.res.oracle

@@ -37,15 +37,15 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/callstacks.i:4: Warning: 
+[nonterm:stmt] tests/nonterm/callstacks.i:4: Warning: 
   non-terminating loop
   stack: nt :: tests/nonterm/callstacks.i:8 <-
          f :: tests/nonterm/callstacks.i:13 <-
          g :: tests/nonterm/callstacks.i:18 <-
          h :: tests/nonterm/callstacks.i:23 <-
          main
-[nonterm] tests/nonterm/callstacks.i:8: Warning: unreachable return
-[nonterm] tests/nonterm/callstacks.i:13: Warning: unreachable return
-[nonterm] tests/nonterm/callstacks.i:18: Warning: unreachable return
-[nonterm] tests/nonterm/callstacks.i:23: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/callstacks.i:8: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/callstacks.i:13: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/callstacks.i:18: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/callstacks.i:23: Warning: unreachable return
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n2.res.oracle

@@ -10,7 +10,7 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/n2.i:6: Warning: 
+[nonterm:stmt] tests/nonterm/n2.i:6: Warning: 
   non-terminating loop
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle

@@ -30,10 +30,10 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/n5.i:12: Warning: 
+[nonterm:stmt] tests/nonterm/n5.i:12: Warning: 
   non-terminating function call
   stack: f :: tests/nonterm/n5.i:22 <- main
-[nonterm] tests/nonterm/n5.i:23: Warning: 
+[nonterm:stmt] tests/nonterm/n5.i:23: Warning: 
   non-terminating function call
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle

@@ -10,7 +10,7 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/n7.i:4: Warning: 
+[nonterm:stmt] tests/nonterm/n7.i:4: Warning: 
   non-terminating loop
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n8.0.res.oracle

@@ -35,11 +35,13 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/n8.i:17: Warning: unreachable return
-[nonterm] tests/nonterm/n8.i:22: Warning: unreachable implicit return
-[nonterm] tests/nonterm/n8.i:31: Warning: unreachable implicit return
-[nonterm] tests/nonterm/n8.i:37: Warning: unreachable return
-[nonterm] tests/nonterm/n8.i:41: Warning: 
+[nonterm:unreachable] tests/nonterm/n8.i:17: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/n8.i:22: Warning: 
+  unreachable implicit return
+[nonterm:unreachable] tests/nonterm/n8.i:31: Warning: 
+  unreachable implicit return
+[nonterm:unreachable] tests/nonterm/n8.i:37: Warning: unreachable return
+[nonterm:stmt] tests/nonterm/n8.i:41: Warning: 
   non-terminating loop
   stack: main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n8.1.res.oracle

@@ -35,15 +35,17 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/n8.i:13: Warning: statement is syntactically unreachable
-[nonterm] tests/nonterm/n8.i:17: Warning: statement is syntactically unreachable
-[nonterm] tests/nonterm/n8.i:22: Warning: 
+[nonterm:dead-code] tests/nonterm/n8.i:13: Warning: 
+  statement is syntactically unreachable
+[nonterm:dead-code] tests/nonterm/n8.i:17: Warning: 
+  statement is syntactically unreachable
+[nonterm:dead-code] tests/nonterm/n8.i:22: Warning: 
   implicit return is syntactically unreachable
-[nonterm] tests/nonterm/n8.i:31: Warning: 
+[nonterm:dead-code] tests/nonterm/n8.i:31: Warning: 
   implicit return is syntactically unreachable
-[nonterm] tests/nonterm/n8.i:41: Warning: 
+[nonterm:stmt] tests/nonterm/n8.i:41: Warning: 
   non-terminating loop
   stack: main
-[nonterm] tests/nonterm/n8.i:41: Warning: 
+[nonterm:dead-code] tests/nonterm/n8.i:41: Warning: 
   implicit return is syntactically unreachable
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/n9.res.oracle

@@ -28,13 +28,13 @@
 [eva:final-states] Values at end of function main:
   res ∈ {0}
   __retres ∈ {0}
-[nonterm] tests/nonterm/n9.i:7: Warning: 
+[nonterm:stmt] tests/nonterm/n9.i:7: Warning: 
   non-terminating loop
   stack: f :: tests/nonterm/n9.i:41 <- main
-[nonterm] tests/nonterm/n9.i:19: Warning: 
+[nonterm:stmt] tests/nonterm/n9.i:19: Warning: 
   non-terminating loop
   stack: g :: tests/nonterm/n9.i:42 <- main
-[nonterm] tests/nonterm/n9.i:29: Warning: 
+[nonterm:stmt] tests/nonterm/n9.i:29: Warning: 
   non-terminating loop
   stack: f_explicit_break :: tests/nonterm/n9.i:43 <- main
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/output_to_file.res.oracle

@@ -15,8 +15,9 @@
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
-[nonterm] tests/nonterm/output_to_file.i:7: Warning: 
+[nonterm:stmt] tests/nonterm/output_to_file.i:7: Warning: 
   non-terminating loop
   stack: loop :: tests/nonterm/output_to_file.i:11 <- main
-[nonterm] tests/nonterm/output_to_file.i:12: Warning: unreachable return
+[nonterm:unreachable] tests/nonterm/output_to_file.i:12: Warning: 
+  unreachable return
 [nonterm] Analysis done.

src/plugins/nonterm/tests/nonterm/oracle/output_to_file.txt

-tests/nonterm/output_to_file.i:7:[nonterm] warning: non-terminating loop
+tests/nonterm/output_to_file.i:7:[nonterm:stmt] warning: non-terminating loop
 stack: loop :: tests/nonterm/output_to_file.i:11 <- main
-tests/nonterm/output_to_file.i:12:[nonterm] warning: unreachable return
+tests/nonterm/output_to_file.i:12:[nonterm:unreachable] warning: unreachable return