diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl index 483507e7b9..ceecd0093b 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..af7a17f96c 100644 --- a/docs/misra/deviations.rst +++ b/docs/misra/deviations.rst @@ -86,6 +86,17 @@ 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. This behavior occurs only in configurations where + assertions are enabled. To address this, 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. + Xen expects developers to ensure code remains safe and reliable in builds, + even when debug-only assertions like `ASSERT_UNREACHABLE() are removed. + * - R2.2 - Proving compliance with respect to Rule 2.2 is generally impossible: see ``_ for details. Moreover, peer diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst index 3e014a6298..d9fd92160b 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 no-return due to calls to the `ASSERT_UNREACHABLE()' + macro in debug build configurations are not considered violations:: + + static inline bool + arch_vcpu_ioreq_completion(enum vio_completion completion) + { + ASSERT_UNREACHABLE(); + return false; + } * - `Rule 2.6 `_ - Advisory