From: Nicola Vetrini <nicola.vetr...@bugseng.com>
MISRA C Rule 2.1 states: "A project shall not contain unreachable code".
Functions that are non-returning and are not explicitly annotated with
the `noreturn' attribute are considered a violation of this rule.
In certain cases, some functions might be non-returning in debug build
configuration (when `NDEBUG' is not defined), due to calls to
`__builtin_unreachable' in the expansion of the macro `ASSERT_UNREACHABLE()'.
Conversely, in non-debug (release) builds (when `NDEBUG' is defined),
the macro `ASSERT_UNREACHABLE()' expands to an empty construct
(`do { } while (0)'), which does not affect the execution flow.
This allows such functions to return normally in release builds,
avoiding unreachable code.
To account for that in debug build, the `noreturn` property of
`__builtin_unreachable` is overridden in the ECLAIR configuration
to deviate these violations.
Signed-off-by: Nicola Vetrini <nicola.vetr...@bugseng.com>
Signed-off-by: Dmytro Prokopchuk <dmytro_prokopch...@epam.com>
---
Test CI pipeline:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/1957211653
---
automation/eclair_analysis/ECLAIR/deviations.ecl | 5 +++++
docs/misra/deviations.rst | 8 ++++++++
docs/misra/rules.rst | 9 +++++++++
3 files changed, 22 insertions(+)
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 483507e7b9..8a05e17dac 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -36,6 +36,11 @@ not executable, and therefore it is safe for them to be
unreachable."
-config=MC3A2.R2.1,reports+={deliberate,
"any_area(any_loc(file(C_runtime_failures)))"}
-doc_end
+-doc_begin="Calls to function `__builtin_unreachable' in the expansion of macro
+`ASSERT_UNREACHABLE()' are not considered to have the `noreturn' property."
+-call_properties+={"name(__builtin_unreachable)&&stmt(begin(any_exp(macro(name(ASSERT_UNREACHABLE)))))",
{"noreturn(false)"}}
+-doc_end
+
-doc_begin="Proving compliance with respect to Rule 2.2 is generally
impossible:
see https://arxiv.org/abs/2212.13933 for details. Moreover, peer review gives
us
confidence that no evidence of errors in the program's logic has been missed
due
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index e78179fcb8..fba75be2ee 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -86,6 +86,14 @@ Deviations related to MISRA C:2012 Rules:
generate definitions for asm modules.
- Tagged as `deliberate` for ECLAIR.
+ * - R2.1
+ - Calls to the `__builtin_unreachable` function inside the expansion of
+ the `ASSERT_UNREACHABLE()` macro may cause a function to be marked as
+ non-returning. Since this only happens in debug configurations,
+ the `noreturn` property for `__builtin_unreachable` is overridden in
+ these contexts, resulting in the absence of reports that do not have
+ an impact on safety, despite being true positives.
+
* - R2.2
- Proving compliance with respect to Rule 2.2 is generally impossible:
see `<https://arxiv.org/abs/2212.13933>`_ for details. Moreover, peer
diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
index 3e014a6298..74badcb616 100644
--- a/docs/misra/rules.rst
+++ b/docs/misra/rules.rst
@@ -124,6 +124,15 @@ maintainers if you want to suggest a change.
they are used to generate definitions for asm modules
- Declarations without initializer are safe, as they are not
executed
+ - Functions that are noreturn due to calls to `ASSERT_UNREACHABLE`
+ macro in debug build configurations are not reported as violations::
+
+ static inline bool
+ arch_vcpu_ioreq_completion(enum vio_completion completion)
+ {
+ ASSERT_UNREACHABLE();
+ return false;
+ }
* - `Rule 2.6
<https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/R_02_06.c>`_
- Advisory
--
2.43.0
