On 15/12/23 10:26, Federico Serafini wrote:
MISRA C:2012 Rule 16.3 states that an unconditional break statement
shall terminate every switch-clause.
Update ECLAIR configuration to take into account:
- continue, goto, return statements;
- functions that do not give the control back;
- fallthrough pseudo-keyword;
- macro BUG();
- comments.
Update docs/misra/deviations.rst accordingly.
Signed-off-by: Federico Serafini <federico.seraf...@bugseng.com>
---
.../eclair_analysis/ECLAIR/deviations.ecl | 28 +++++++++++++++++++
docs/misra/deviations.rst | 28 +++++++++++++++++++
2 files changed, 56 insertions(+)
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 683f2bbfe8..e27d840fe4 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -327,6 +327,34 @@ therefore have the same behavior of a boolean"
-config=MC3R1.R14.4,etypes+={deliberate,
"stmt(child(cond,child(expr,ref(^<?domain>?::is_dying$))))","src_type(enum)"}
-doc_end
+#
+# Series 16.
+#
+
+-doc_begin="Switch clauses ending with continue, goto, return statements are
+safe."
+-config=MC3R1.R16.3,terminals+={safe,
"node(continue_stmt||goto_stmt||return_stmt)"}
+-doc_end
+
+-doc_begin="Switch clauses ending with a call to a function that does not give
+the control back are safe."
+-config=MC3R1.R16.3,terminals+={safe, "call(property(noreturn))"}
+-doc_end
+
+-doc_begin="Switch clauses ending with pseudo-keyword \"fallthrough\" are
+safe."
+-config=MC3R1.R16.3,reports+={safe,
"any_area(end_loc(any_exp(text(/fallthrough;/))))"}
+-doc_end
+
+-doc_begin="Switch clauses ending with failure method \"BUG()\" are safe."
+-config=MC3R1.R16.3,reports+={safe,
"any_area(end_loc(any_exp(text(/BUG\\(\\);/))))"}
+-doc_end
+
+-doc_begin="Switch clauses not ending with the break statement are safe if an
+explicit comment indicating the fallthrough intention is present."
+-config=MC3R1.R16.3,reports+={safe, "any_area(end_loc(any_exp(text(^(?s).*/\\*
[fF]all ?through.? \\*/.*$,0..1))))"}
+-doc_end
+
#
# Series 20.
#
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index eda3c8100c..d593be81b9 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -276,6 +276,34 @@ Deviations related to MISRA C:2012 Rules:
therefore have the same behavior of a boolean.
- Project-wide deviation; tagged as `deliberate` for ECLAIR.
+ * - R16.3
+ - Switch clauses ending with continue, goto, return statements are safe.
+ - Tagged as `safe` for ECLAIR.
+
+ * - R16.3
+ - Switch clauses ending with a call to a function that does not give
+ the control back are safe.
+ - Tagged as `safe` for ECLAIR.
+
+ * - R16.3
+ - Switch clauses ending with failure method \"BUG()\" are safe.
+ - Tagged as `safe` for ECLAIR.
+
+ * - R16.3
+ - Existing switch clauses not ending with the break statement are safe if
+ an explicit comment indicating the fallthrough intention is present.
+ However, the use of such comments in new code is deprecated:
+ pseudo-keyword "fallthrough" shall be used.
+ - Tagged as `safe` for ECLAIR. The accepted comments are:
+ - /\* fall through \*/
+ - /\* fall through. \*/
+ - /\* fallthrough \*/
+ - /\* fallthrough. \*/
+ - /\* Fall through \*/
+ - /\* Fall through. \*/
+ - /\* Fallthrough \*/
+ - /\* Fallthrough. \*/
+
* - R20.7
- Code violating Rule 20.7 is safe when macro parameters are used:
(1) as function arguments;
I forgot to mention that this is a V2.
The older version and the discussion can be found at:
https://lists.xenproject.org/archives/html/xen-devel/2023-12/msg00957.html
--
Federico Serafini, M.Sc.
Software Engineer, BUGSENG (http://bugseng.com)