From 3039e7118f8e814f97ed45cb7b23941a4550ab69 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 15 Dec 2020 14:42:03 +0100
Subject: [PATCH] [Nonterm] add warn categories
---
src/plugins/nonterm/nonterm_run.ml | 12 +++++++++---
.../nonterm/oracle/builtin_termination.res.oracle | 2 +-
.../tests/nonterm/oracle/callstack.res.oracle | 6 +++---
.../tests/nonterm/oracle/callstacks.res.oracle | 10 +++++-----
.../nonterm/tests/nonterm/oracle/n2.res.oracle | 2 +-
.../nonterm/tests/nonterm/oracle/n5.res.oracle | 4 ++--
.../nonterm/tests/nonterm/oracle/n7.res.oracle | 2 +-
.../nonterm/tests/nonterm/oracle/n8.0.res.oracle | 12 +++++++-----
.../nonterm/tests/nonterm/oracle/n8.1.res.oracle | 14 ++++++++------
.../nonterm/tests/nonterm/oracle/n9.res.oracle | 6 +++---
.../tests/nonterm/oracle/output_to_file.res.oracle | 5 +++--
.../tests/nonterm/oracle/output_to_file.txt | 4 ++--
12 files changed, 45 insertions(+), 34 deletions(-)
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index a4f74bc205a..12104719725 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 3effbe4d066..c6094d433be 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 93e52b1abcc..047945a4f21 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 9a01fe80725..a5ab5b9714a 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 7797397288f..ce4cbfc9afe 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 57e276f11f9..7b9e1bf31b5 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 49675ab4fcc..e9a783d3568 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 4453db08d9a..0833b237866 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 7ee52d4f41f..84c5cfc9d01 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 953c368367b..b7c8d4b8ebc 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 3909a9be3aa..1cc9c3c0670 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 6dd97cd6bff..79d03dcb1a1 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
--
GitLab