On 2025-08-24 16:56, Dmytro Prokopchuk1 wrote:
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 specific
build
configurations due to call to '__builtin_unreachable()' in the
expansion
of the macro 'BUG()':
- functions 'gicv3_do_LPI()' and 'gicv3_its_setup_collection()' when
the
config CONFIG_HAS_ITS is not defined, it is intentionally used to catch
and prevent any unintended execution of code that should only run when
ITS is available;
- function 'prepare_acpi()' when the config CONFIG_ACPI is not
defined,
to trigger an error if ACPI-related features are used incorrectly.
To account for that in specific builds, update the ECLAIR configuration
to deviate these violations. Update deviations.rst file accordingly.
No functional changes.
Signed-off-by: Dmytro Prokopchuk <dmytro_prokopch...@epam.com>
---
Test CI pipeline:
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/pipelines/2000738682
---
https://gitlab.com/xen-project/people/dimaprkp4k/xen/-/jobs/11119212994
Build failure here
automation/eclair_analysis/ECLAIR/deviations.ecl | 11 +++++++++++
docs/misra/deviations.rst | 13 +++++++++++++
2 files changed, 24 insertions(+)
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 7f3fd35a33..336aec58c2 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -41,6 +41,17 @@ not executable, and therefore it is safe for them to
be unreachable."
-call_properties+={"name(__builtin_unreachable)&&stmt(begin(any_exp(macro(name(ASSERT_UNREACHABLE)))))",
{"noreturn(false)"}}
-doc_end
+-doc_begin="The 'BUG()' macro is intentionally used in the
'prepare_acpi()' function in specific build configuration
+(when the config CONFIG_ACPI is not defined) to trigger an error if
ACPI-related features are used incorrectly."
+-config=MC3A2.R2.1,reports+={deliberate,
"any_area(any_loc(file(^xen/arch/arm/include/asm/domain_build\\.h$))&&context(name(prepare_acpi)))"}
+-doc_end
+
+-doc_begin="The 'BUG()' macro is intentionally used in
'gicv3_do_LPI'() and 'gicv3_its_setup_collection()' functions
+in specific build configuration (when the config CONFIG_HAS_ITS is not
defined) to catch and prevent any unintended
+execution of code that should only run when ITS is available."
+-config=MC3A2.R2.1,reports+={deliberate,
"any_area(any_loc(file(^xen/arch/arm/include/asm/gic_v3_its\\.h$))&&context(name(gicv3_do_LPI||gicv3_its_setup_collection)))"}
+-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 2119066531..96eb202502 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -97,6 +97,19 @@ Deviations related to MISRA C:2012 Rules:
Xen expects developers to ensure code remains safe and reliable
in builds,
even when debug-only assertions like `ASSERT_UNREACHABLE() are
removed.
+ * - R2.1
+ - The 'BUG()' macro is intentionally used in the 'prepare_acpi()'
function
+ in specific build configuration (when the config CONFIG_ACPI is
not
+ defined) to trigger an error if ACPI-related features are used
incorrectly.
+ - Tagged as `deliberate` for ECLAIR.
+
+ * - R2.1
+ - The 'BUG()' macro is intentionally used in 'gicv3_do_LPI'() and
+ 'gicv3_its_setup_collection()' functions in specific build
configuration
+ (when the config CONFIG_HAS_ITS is not defined) to catch and
prevent any
+ unintended execution of code that should only run when ITS is
available.
+ - Tagged as `deliberate` for ECLAIR.
+
* - R2.2
- Proving compliance with respect to Rule 2.2 is generally
impossible:
see `<https://arxiv.org/abs/2212.13933>`_ for details.
Moreover, peer
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253
