diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml index a4f74bc205af61d14b74d1eb2858549055584bd5..121047197255d8f3498674f68d62758f69b0a4a9 100644 --- a/src/plugins/nonterm/nonterm_run.ml +++ b/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 diff --git a/src/plugins/nonterm/tests/nonterm/oracle/builtin_termination.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/builtin_termination.res.oracle index 3effbe4d066c62ee129194af9c2a28fd2f2ac30d..c6094d433be6a22ba0a726a907edfb32aca2f336 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/builtin_termination.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle index 93e52b1abcc2748f95222a8ff3613add99c96c80..047945a4f21d86ba5c7dc65baebd1a2dbb8448bf 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/callstacks.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/callstacks.res.oracle index 9a01fe807254cee654a6e998bc2e653d7b12e692..a5ab5b9714ab240b3f8b2ab473dc2117564240ec 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/callstacks.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n2.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n2.res.oracle index 7797397288f88f4d9aa29f330f4d245361a633c6..ce4cbfc9afe42e40b5a03448145b96148a882b5d 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n2.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle index 57e276f11f9467e0c4f5a33b49a071cdc76f2311..7b9e1bf31b5eda3d69ff4fe9ffa83ef84b4d56ee 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle index 49675ab4fccdb6e01ffacc1f686da9e2b97922c8..e9a783d35685e30928b1d5b8d0370455859ef39f 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n8.0.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n8.0.res.oracle index 4453db08d9a9bffda693c320c9bc85bfc86e7787..0833b2378663ce10410b692011ac6a4c80d37927 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n8.0.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n8.1.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n8.1.res.oracle index 7ee52d4f41fd5e63583581bf4b121a37350d4e15..84c5cfc9d017e899cf421c36b1a91ce03f60b65e 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n8.1.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n9.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n9.res.oracle index 953c368367b25393e3cfccc1d03af8f3fc451e07..b7c8d4b8ebc483ea74462d4bbb2692d1398ab7ec 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n9.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.res.oracle index 3909a9be3aa54c712a5918a0fc61ca99953eff8d..1cc9c3c067048bf58487640a9ed879261bf139c4 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.res.oracle +++ b/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. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.txt b/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.txt index 6dd97cd6bff2dbb61792a7ce65fd78fc724e8751..79d03dcb1a11b98ab4a2493468208709fd70b70e 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.txt +++ b/src/plugins/nonterm/tests/nonterm/oracle/output_to_file.txt @@ -1,3 +1,3 @@ -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