| R2.1 |
The compiler implementation guarantees that the unreachable code is
removed. Constant expressions and unreachable branches of if and switch
statements are expected. |
Tagged as safe for ECLAIR. |
| R2.1 |
Unreachability caused by calls to the following functions or macros
is deliberate and there is no risk of code being unexpectedly left
out. |
- Tagged as deliberate for ECLAIR. Such
macros are:
-
- BUG
- assert_failed
- __builtin_unreachable
- ASSERT_UNREACHABLE
|
| R2.1 |
Pure declarations, that is, declarations without initializations are
not executable, and therefore it is safe for them to be unreachable. The
most notable example of such a pattern being used in the codebase is
that of a variable declaration that should be available in all the
clauses of a switch statement. |
ECLAIR has been configured to ignore those statements. |
| R2.2 |
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 to undetected
violations of Rule 2.2, if any. Testing on time behavior gives us
confidence on the fact that, should the program contain dead code that
is not removed by the compiler, the resulting slowdown is
negligible. |
Project-wide deviation, tagged as disapplied for ECLAIR. |
| R3.1 |
Comments starting with '/*' and containing hyperlinks are safe as
they are not instances of commented-out code. |
Tagged as safe for ECLAIR. |
| R5.3 |
As specified in rules.rst, shadowing due to macros being used as
macro arguments is allowed, as it's deemed not at risk of causing
developer confusion. |
- Tagged as safe for ECLAIR. So far,
the following macros are deviated:
-
- READ_SYSREG and WRITE_SYSREG
- max{t}? and min{t}?
- read[bwlq] and read[bwlq]relaxed
- per_cpu and this_cpu
- __emulate_2op and __emulate_2op_nobyte
- read_debugreg and write_debugreg
|
| R7.2 |
Violations caused by __HYPERVISOR_VIRT_START are related to the
particular use of it done in xen_mk_ulong. |
Tagged as deliberate for ECLAIR. |
| R7.4 |
Allow pointers of non-character type as long as the pointee is
const-qualified. |
ECLAIR has been configured to ignore these assignments. |
| R8.3 |
The type ret_t is deliberately used and defined as int or long
depending on the architecture. |
Tagged as deliberate for ECLAIR. |
| R8.3 |
Some files are not subject to respect MISRA rules at the moment, but
some entity from a file in scope is used; therefore ECLAIR does report a
violation, since not all the files involved in the violation are
excluded from the analysis. |
- Tagged as deliberate for ECLAIR. Such
excluded files are:
-
- xen/arch/x86/time.c
- xen/arch/x86/acpi/cpu_idle.c
- xen/arch/x86/mpparse.c
- xen/common/bunzip2.c
- xen/common/unlz4.c
- xen/common/unlzma.c
- xen/common/unlzo.c
- xen/common/unxz.c
- xen/common/unzstd.c
|
| R8.4 |
The definitions present in the files 'asm-offsets.c' for any
architecture are used to generate definitions for asm modules, and are
not called by C code. Therefore the absence of prior declarations is
safe. |
Tagged as safe for ECLAIR. |
| R8.4 |
The functions defined in the file xen/common/coverage/gcov_base.c
are meant to be called from gcc-generated code in a non-release build
configuration. Therefore, the absence of prior declarations is
safe. |
Tagged as safe for ECLAIR. |
| R8.6 |
The following variables are compiled in multiple translation units
belonging to different executables and therefore are safe.
- current_stack_pointer
- bsearch
- sort
|
Tagged as safe for ECLAIR. |
| R8.6 |
Declarations without definitions are allowed (specifically when the
definition is compiled-out or optimized-out by the compiler). |
Tagged as deliberate in ECLAIR. |
| R8.10 |
The gnu_inline attribute without static is deliberately
allowed. |
Tagged as deliberate for ECLAIR. |
| R9.5 |
The possibility of committing mistakes by specifying an explicit
dimension is higher than omitting the dimension, therefore all such
instances of violations are deviated. |
Project-wide deviation, tagged as deliberate for ECLAIR. |
| R10.1, R10.3, R10.4 |
The value-preserving conversions of integer constants are safe. |
Tagged as safe for ECLAIR. |
| R10.1 |
Shifting non-negative integers to the right is safe. |
Tagged as safe for ECLAIR. |
| R10.1 |
Shifting non-negative integers to the left is safe if the result is
still non-negative. |
Tagged as safe for ECLAIR. |
| R10.1 |
Bitwise logical operations on non-negative integers are safe. |
Tagged as safe for ECLAIR. |
| R10.1 |
The implicit conversion to Boolean for logical operator arguments is
well-known to all Xen developers to be a comparison with 0. |
Tagged as safe for ECLAIR. |
| R10.1 |
Xen only supports architectures where signed integers are
representend using two's complement and all the Xen developers are aware
of this. For this reason, bitwise operations are safe. |
Tagged as safe for ECLAIR. |
| R10.1 |
Given the assumptions on the toolchain detailed in
docs/misra/C-language-toolchain.rst and the build flags used by the
project, it is deemed safe to use bitwise shift operators. See
automation/eclair_analysis/deviations.ecl for the full explanation. |
Tagged as safe for ECLAIR. |
| R13.5 |
All developers and reviewers can be safely assumed to be well aware
of the short-circuit evaluation strategy for logical operators. |
Project-wide deviation; tagged as disapplied for ECLAIR. |
| R14.2 |
The severe restrictions imposed by this rule on the use of 'for'
statements are not counterbalanced by the presumed facilitation of the
peer review activity. |
Project-wide deviation; tagged as disapplied for ECLAIR. |
| R14.3 |
The Xen team relies on the fact that invariant conditions of 'if'
statements are deliberate. |
Project-wide deviation; tagged as disapplied for ECLAIR. |
| R20.7 |
Code violating Rule 20.7 is safe when macro parameters are used:
- as function arguments;
- as macro arguments;
- as array indices;
- as lhs in assignments.
|
Tagged as safe for ECLAIR. |