[XEN PATCH v2 0/7] address violations of MISRA C:2012 Rule 2.1

[XEN PATCH v2 0/7] address violations of MISRA C:2012 Rule 2.1

[Nicola Vetrini]

MISRA C:2012 Rule 2.1 states: "A project shall not contain unreachable code".
As such, this series eliminates various instances of unreachable code found in
Xen, by providing equivalent compliant constructs.

This series is loosely based on my earlier series [1], but the overall approach
has changed since; for instance, declarations without initialization are now
ignored, as detailed in docs/misra/deviations.rst.

[1] https://lore.kernel.org/xen-devel/cover.1690985045.git.nicola.vetrini@bugseng.com/

Changes in v2:
- Patch 4 has been committed;
- Drop Patch 7/7;
- Add two new patches:
  - "xen/arm: vcpreg: address violation of MISRA C Rule 2.1"
  - "automation/eclair_analysis: avoid violation of MISRA Rule 2.1"
- Reworked all other patches.

Nicola Vetrini (7):
  xen/shutdown: address MISRA C:2012 Rule 2.1
  x86/mm: address MISRA C:2012 Rule 2.1
  xen/arm: address MISRA C:2012 Rule 2.1
  xen/arm: traps: add ASSERT_UNREACHABLE() where needed
  x86/platform: removed break to address MISRA C:2012 Rule 2.1
  xen/arm: vcpreg: address violation of MISRA C Rule 2.1
  automation/eclair_analysis: avoid violation of MISRA Rule 2.1

 automation/eclair_analysis/ECLAIR/deviations.ecl |  7 ++++++-
 xen/arch/arm/mm.c                                |  1 +
 xen/arch/arm/traps.c                             |  3 ++-
 xen/arch/arm/vcpreg.c                            | 10 ++++++++--
 xen/arch/arm/vgic-v3-its.c                       |  1 +
 xen/arch/x86/mm.c                                |  2 --
 xen/arch/x86/platform_hypercall.c                |  1 -
 xen/common/shutdown.c                            | 15 ++++-----------
 8 files changed, 22 insertions(+), 18 deletions(-)

-- 
2.34.1

[XEN PATCH v2 1/7] xen/shutdown: address MISRA C:2012 Rule 2.1

[Nicola Vetrini]

Given that 'hwdom_shutdown' is a noreturn function, unreachable
breaks can be eliminated to resolve violations of Rule 2.1.

The rename s/maybe_reboot/reboot_or_halt/ is done to clarify
that the function is noreturn.

No functional change.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- rename maybe_reboot to reboot_or_halt.
---
 automation/eclair_analysis/ECLAIR/deviations.ecl |  2 +-
 xen/common/shutdown.c                            | 15 ++++-----------
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 683f2bbfe89b..85741a2c01a9 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -16,7 +16,7 @@ Constant expressions and unreachable branches of if and switch statements are ex
 
 -doc_begin="Unreachability caused by calls to the following functions or macros is deliberate and there is no risk of code being unexpectedly left out."
 -config=MC3R1.R2.1,statements+={deliberate,"macro(name(BUG||assert_failed))"}
--config=MC3R1.R2.1,statements+={deliberate, "call(decl(name(__builtin_unreachable||panic||do_unexpected_trap||machine_halt||machine_restart||maybe_reboot)))"}
+-config=MC3R1.R2.1,statements+={deliberate, "call(decl(name(__builtin_unreachable||panic||do_unexpected_trap||machine_halt||machine_restart||reboot_or_halt)))"}
 -doc_end
 
 -doc_begin="Unreachability inside an ASSERT_UNREACHABLE() and analogous macro calls is deliberate and safe."
diff --git a/xen/common/shutdown.c b/xen/common/shutdown.c
index 37901a4f3391..dfd5e41097e9 100644
--- a/xen/common/shutdown.c
+++ b/xen/common/shutdown.c
@@ -15,7 +15,7 @@
 bool __read_mostly opt_noreboot;
 boolean_param("noreboot", opt_noreboot);
 
-static void noreturn maybe_reboot(void)
+static void noreturn reboot_or_halt(void)
 {
     if ( opt_noreboot )
     {
@@ -38,39 +38,32 @@ void hwdom_shutdown(u8 reason)
         printk("Hardware Dom%u halted: halting machine\n",
                hardware_domain->domain_id);
         machine_halt();
-        break; /* not reached */
 
     case SHUTDOWN_crash:
         debugger_trap_immediate();
         printk("Hardware Dom%u crashed: ", hardware_domain->domain_id);
         kexec_crash(CRASHREASON_HWDOM);
-        maybe_reboot();
-        break; /* not reached */
+        reboot_or_halt();
 
     case SHUTDOWN_reboot:
         printk("Hardware Dom%u shutdown: rebooting machine\n",
                hardware_domain->domain_id);
         machine_restart(0);
-        break; /* not reached */
 
     case SHUTDOWN_watchdog:
         printk("Hardware Dom%u shutdown: watchdog rebooting machine\n",
                hardware_domain->domain_id);
         kexec_crash(CRASHREASON_WATCHDOG);
         machine_restart(0);
-        break; /* not reached */
 
     case SHUTDOWN_soft_reset:
         printk("Hardware domain %d did unsupported soft reset, rebooting.\n",
                hardware_domain->domain_id);
         machine_restart(0);
-        break; /* not reached */
 
     default:
         printk("Hardware Dom%u shutdown (unknown reason %u): ",
                hardware_domain->domain_id, reason);
-        maybe_reboot();
-        break; /* not reached */
+        reboot_or_halt();
     }
-}  
-
+}
-- 
2.34.1

Re: [XEN PATCH v2 1/7] xen/shutdown: address MISRA C:2012 Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> Given that 'hwdom_shutdown' is a noreturn function, unreachable
> breaks can be eliminated to resolve violations of Rule 2.1.
> 
> The rename s/maybe_reboot/reboot_or_halt/ is done to clarify
> that the function is noreturn.
> 
> No functional change.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>


Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

[XEN PATCH v2 2/7] x86/mm: address MISRA C:2012 Rule 2.1

[Nicola Vetrini]

The "return 0" after the swich statement in 'xen/arch/x86/mm.c'
is unreachable because all switch clauses end with returns, and
can thus be dropped.

No functional changes.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- Drop the final return instead. A stripped-down version of this switch has been
  tested on godbolt.org with gcc-4.1.2 and shows no compile-time issues.
---
 xen/arch/x86/mm.c | 2 --
 1 file changed, 2 deletions(-)

diff --git a/xen/arch/x86/mm.c b/xen/arch/x86/mm.c
index 0a66db10b959..49d9f371f35c 100644
--- a/xen/arch/x86/mm.c
+++ b/xen/arch/x86/mm.c
@@ -4887,8 +4887,6 @@ long arch_memory_op(unsigned long cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
     default:
         return subarch_memory_op(cmd, arg);
     }
-
-    return 0;
 }
 
 int cf_check mmio_ro_emulated_write(
-- 
2.34.1

Re: [XEN PATCH v2 2/7] x86/mm: address MISRA C:2012 Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> The "return 0" after the swich statement in 'xen/arch/x86/mm.c'
> is unreachable because all switch clauses end with returns, and
> can thus be dropped.
> 
> No functional changes.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

Re: [XEN PATCH v2 2/7] x86/mm: address MISRA C:2012 Rule 2.1

[Jan Beulich]

On 18.12.2023 11:17, Nicola Vetrini wrote:
> --- a/xen/arch/x86/mm.c
> +++ b/xen/arch/x86/mm.c
> @@ -4887,8 +4887,6 @@ long arch_memory_op(unsigned long cmd, XEN_GUEST_HANDLE_PARAM(void) arg)
>      default:
>          return subarch_memory_op(cmd, arg);
>      }
> -
> -    return 0;
>  }

When a function is small and it's easy to see that all paths return by
other means, omitting such a final "return <value>" is imo okay. Here,
however, this isn't easy to see, and hence omitting the return is
confusing in a different way from having the return. I guess I'll make
an alternative change (as iirc I had outlined before), for other x86
maintainers to at least consider. The other alternative (causing less
code churn) would imo be to pull out the default case from the switch().

Jan

[XEN PATCH v2 3/7] xen/arm: address MISRA C:2012 Rule 2.1

[Nicola Vetrini]

There are no paths that can reach the last return statement
of function 'vgic_v3_its_mmio_write' in 'vcig-v3-its.c' and
'arch_memory_op' in 'arch/arm/mm.c', thus violating
MISRA C:2012 Rule 2.1:
"A project shall not contain unreachable code".

Therefore, an ASSERT_UNREACHABLE() is inserted to remove the unreachable
return statement and protect against possible mistakes.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- Changed resolution strategy to have an ASSERT_UNREACHABLE() before
  the return.
---
 xen/arch/arm/mm.c          | 1 +
 xen/arch/arm/vgic-v3-its.c | 1 +
 2 files changed, 2 insertions(+)

diff --git a/xen/arch/arm/mm.c b/xen/arch/arm/mm.c
index eeb65ca6bb79..b15a18a49412 100644
--- a/xen/arch/arm/mm.c
+++ b/xen/arch/arm/mm.c
@@ -283,6 +283,7 @@ long arch_memory_op(int op, XEN_GUEST_HANDLE_PARAM(void) arg)
         return -ENOSYS;
     }
 
+    ASSERT_UNREACHABLE();
     return 0;
 }
 
diff --git a/xen/arch/arm/vgic-v3-its.c b/xen/arch/arm/vgic-v3-its.c
index 05429030b539..70b5aeb82219 100644
--- a/xen/arch/arm/vgic-v3-its.c
+++ b/xen/arch/arm/vgic-v3-its.c
@@ -1409,6 +1409,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
         return 0;
     }
 
+    ASSERT_UNREACHABLE();
     return 1;
 
 write_ignore_64:
-- 
2.34.1

Re: [XEN PATCH v2 3/7] xen/arm: address MISRA C:2012 Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:

> There are no paths that can reach the last return statement
> of function 'vgic_v3_its_mmio_write' in 'vcig-v3-its.c' and
> 'arch_memory_op' in 'arch/arm/mm.c', thus violating
> MISRA C:2012 Rule 2.1:
> "A project shall not contain unreachable code".
> 
> Therefore, an ASSERT_UNREACHABLE() is inserted to remove the unreachable
> return statement and protect against possible mistakes.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>


> ---
> Changes in v2:
> - Changed resolution strategy to have an ASSERT_UNREACHABLE() before
>   the return.
> ---
>  xen/arch/arm/mm.c          | 1 +
>  xen/arch/arm/vgic-v3-its.c | 1 +
>  2 files changed, 2 insertions(+)
> 
> diff --git a/xen/arch/arm/mm.c b/xen/arch/arm/mm.c
> index eeb65ca6bb79..b15a18a49412 100644
> --- a/xen/arch/arm/mm.c
> +++ b/xen/arch/arm/mm.c
> @@ -283,6 +283,7 @@ long arch_memory_op(int op, XEN_GUEST_HANDLE_PARAM(void) arg)
>          return -ENOSYS;
>      }
>  
> +    ASSERT_UNREACHABLE();
>      return 0;
>  }
>  
> diff --git a/xen/arch/arm/vgic-v3-its.c b/xen/arch/arm/vgic-v3-its.c
> index 05429030b539..70b5aeb82219 100644
> --- a/xen/arch/arm/vgic-v3-its.c
> +++ b/xen/arch/arm/vgic-v3-its.c
> @@ -1409,6 +1409,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
>          return 0;
>      }
>  
> +    ASSERT_UNREACHABLE();
>      return 1;
>  
>  write_ignore_64:
> -- 
> 2.34.1
> 

[XEN PATCH v2 4/7] xen/arm: traps: add ASSERT_UNREACHABLE() where needed

[Nicola Vetrini]

The statements after a call to the noreturn function 'do_unexpected_trap'
can't be reached, thus violating MISRA C:2012 Rule 2.1
("A project shall not contain unreachable code.").
ASSERT_UNREACHABLE() is used to signal that the unreachable break-s are used as
a defensive coding measure to prevent inadvertent fallthrough.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- Use ASSERT_UNREACHABLE() to prevent mistakes.
---
 xen/arch/arm/traps.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/xen/arch/arm/traps.c b/xen/arch/arm/traps.c
index 3784e8276ef6..77220ba0927a 100644
--- a/xen/arch/arm/traps.c
+++ b/xen/arch/arm/traps.c
@@ -2152,6 +2152,7 @@ void do_trap_hyp_sync(struct cpu_user_regs *regs)
     case HSR_EC_SVE:
         /* An SVE exception is a bug somewhere in hypervisor code */
         do_unexpected_trap("SVE trap at EL2", regs);
+        ASSERT_UNREACHABLE();
         break;
 #endif
     case HSR_EC_DATA_ABORT_CURR_EL:
@@ -2171,7 +2172,7 @@ void do_trap_hyp_sync(struct cpu_user_regs *regs)
             dump_hyp_walk(get_hfar(is_data));
 
         do_unexpected_trap(fault, regs);
-
+        ASSERT_UNREACHABLE();
         break;
     }
     default:
-- 
2.34.1

Re: [XEN PATCH v2 4/7] xen/arm: traps: add ASSERT_UNREACHABLE() where needed

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> The statements after a call to the noreturn function 'do_unexpected_trap'
> can't be reached, thus violating MISRA C:2012 Rule 2.1
> ("A project shall not contain unreachable code.").
> ASSERT_UNREACHABLE() is used to signal that the unreachable break-s are used as
> a defensive coding measure to prevent inadvertent fallthrough.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>


> ---
> Changes in v2:
> - Use ASSERT_UNREACHABLE() to prevent mistakes.
> ---
>  xen/arch/arm/traps.c | 3 ++-
>  1 file changed, 2 insertions(+), 1 deletion(-)
> 
> diff --git a/xen/arch/arm/traps.c b/xen/arch/arm/traps.c
> index 3784e8276ef6..77220ba0927a 100644
> --- a/xen/arch/arm/traps.c
> +++ b/xen/arch/arm/traps.c
> @@ -2152,6 +2152,7 @@ void do_trap_hyp_sync(struct cpu_user_regs *regs)
>      case HSR_EC_SVE:
>          /* An SVE exception is a bug somewhere in hypervisor code */
>          do_unexpected_trap("SVE trap at EL2", regs);
> +        ASSERT_UNREACHABLE();
>          break;
>  #endif
>      case HSR_EC_DATA_ABORT_CURR_EL:
> @@ -2171,7 +2172,7 @@ void do_trap_hyp_sync(struct cpu_user_regs *regs)
>              dump_hyp_walk(get_hfar(is_data));
>  
>          do_unexpected_trap(fault, regs);
> -
> +        ASSERT_UNREACHABLE();
>          break;
>      }
>      default:
> -- 
> 2.34.1
> 

[XEN PATCH v2 5/7] x86/platform: removed break to address MISRA C:2012 Rule 2.1

[Nicola Vetrini]

The break statement is redundant, hence it can be removed.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- Remove the outer break, instead of the inner one.
---
 xen/arch/x86/platform_hypercall.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/xen/arch/x86/platform_hypercall.c b/xen/arch/x86/platform_hypercall.c
index 4dde71db275c..7a2e4b9b603e 100644
--- a/xen/arch/x86/platform_hypercall.c
+++ b/xen/arch/x86/platform_hypercall.c
@@ -725,7 +725,6 @@ ret_t do_platform_op(
             0, cpu_down_helper, (void *)(unsigned long)cpu);
         break;
     }
-    break;
 
     case XENPF_cpu_hotadd:
         ret = xsm_resource_plug_core(XSM_HOOK);
-- 
2.34.1

Re: [XEN PATCH v2 5/7] x86/platform: removed break to address MISRA C:2012 Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> The break statement is redundant, hence it can be removed.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

[XEN PATCH v2 6/7] xen/arm: vcpreg: address violation of MISRA C Rule 2.1

[Nicola Vetrini]

There is no path that reaches the call to 'advance_pc', thus violating MISRA C
Rule 2.1.
A call to ASSERT_UNREACHABLE() is added after the switch, despite this being
useful to detect errors only in debug builds; if that marker is ever reached,
a domain crash is triggered, as a defensive coding measure.

No functional change.

Signed-off-by: Julien Grall <julien@xen.org>
Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
The code changes (including the comment) were made by Julien in [1]; I added the
commit text and all other informations.

All the switch clauses, when expanded, end with a return statement
and the default clause has an unconditional return, therefore
advance_pc() is never reached.

However, it has been deemed safer to crash the domain if the switch is ever
exited.

[1] https://lore.kernel.org/xen-devel/alpine.DEB.2.22.394.2312151232580.3175268@ubuntu-linux-20-04-desktop/T/#maa91d8025532455a6317119a1e4affa00a99e1ce
---
 xen/arch/arm/vcpreg.c | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/xen/arch/arm/vcpreg.c b/xen/arch/arm/vcpreg.c
index 39aeda9dab62..a2d050070473 100644
--- a/xen/arch/arm/vcpreg.c
+++ b/xen/arch/arm/vcpreg.c
@@ -707,8 +707,14 @@ void do_cp10(struct cpu_user_regs *regs, const union hsr hsr)
         inject_undef_exception(regs, hsr);
         return;
     }
-
-    advance_pc(regs, hsr);
+    
+    /*
+     * All the cases in the switch should return. If this is not the
+     * case, then something went wrong and it is best to crash the
+     * domain.
+     */
+    ASSERT_UNREACHABLE();
+    domain_crash(current->domain);
 }
 
 void do_cp(struct cpu_user_regs *regs, const union hsr hsr)
-- 
2.34.1

Re: [XEN PATCH v2 6/7] xen/arm: vcpreg: address violation of MISRA C Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> There is no path that reaches the call to 'advance_pc', thus violating MISRA C
> Rule 2.1.
> A call to ASSERT_UNREACHABLE() is added after the switch, despite this being
> useful to detect errors only in debug builds; if that marker is ever reached,
> a domain crash is triggered, as a defensive coding measure.
> 
> No functional change.
> 
> Signed-off-by: Julien Grall <julien@xen.org>
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>


> ---
> The code changes (including the comment) were made by Julien in [1]; I added the
> commit text and all other informations.
> 
> All the switch clauses, when expanded, end with a return statement
> and the default clause has an unconditional return, therefore
> advance_pc() is never reached.
> 
> However, it has been deemed safer to crash the domain if the switch is ever
> exited.
> 
> [1] https://lore.kernel.org/xen-devel/alpine.DEB.2.22.394.2312151232580.3175268@ubuntu-linux-20-04-desktop/T/#maa91d8025532455a6317119a1e4affa00a99e1ce
> ---
>  xen/arch/arm/vcpreg.c | 10 ++++++++--
>  1 file changed, 8 insertions(+), 2 deletions(-)
> 
> diff --git a/xen/arch/arm/vcpreg.c b/xen/arch/arm/vcpreg.c
> index 39aeda9dab62..a2d050070473 100644
> --- a/xen/arch/arm/vcpreg.c
> +++ b/xen/arch/arm/vcpreg.c
> @@ -707,8 +707,14 @@ void do_cp10(struct cpu_user_regs *regs, const union hsr hsr)
>          inject_undef_exception(regs, hsr);
>          return;
>      }
> -
> -    advance_pc(regs, hsr);
> +    
> +    /*
> +     * All the cases in the switch should return. If this is not the
> +     * case, then something went wrong and it is best to crash the
> +     * domain.
> +     */
> +    ASSERT_UNREACHABLE();
> +    domain_crash(current->domain);
>  }
>  
>  void do_cp(struct cpu_user_regs *regs, const union hsr hsr)
> -- 
> 2.34.1
> 

[XEN PATCH v2 7/7] automation/eclair_analysis: avoid violation of MISRA Rule 2.1

[Nicola Vetrini]

The presence of an unlinked object file triggers a violation
of MISRA C Rule 2.1, which is deviated, as it's not part of
the final Xen binary.

No functional change.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
 automation/eclair_analysis/ECLAIR/deviations.ecl | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 85741a2c01a9..e3de0fb2adf8 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -28,6 +28,11 @@ not executable, and therefore it is safe for them to be unreachable."
 -config=MC3R1.R2.1,ignored_stmts+={"any()", "pure_decl()"}
 -doc_end
 
++-doc_begin="The following autogenerated file is not linked deliberately."
++-file_tag+={C_runtime_failures,"^automation/eclair_analysis/C-runtime-failures\\.rst\\.c$"}
++-config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(file(C_runtime_failures)))"}
++-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
-- 
2.34.1

Re: [XEN PATCH v2 7/7] automation/eclair_analysis: avoid violation of MISRA Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> The presence of an unlinked object file triggers a violation
> of MISRA C Rule 2.1, which is deviated, as it's not part of
> the final Xen binary.
> 
> No functional change.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Acked-by: Stefano Stabellini <sstabellini@kernel.org>


> ---
>  automation/eclair_analysis/ECLAIR/deviations.ecl | 5 +++++
>  1 file changed, 5 insertions(+)
> 
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 85741a2c01a9..e3de0fb2adf8 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -28,6 +28,11 @@ not executable, and therefore it is safe for them to be unreachable."
>  -config=MC3R1.R2.1,ignored_stmts+={"any()", "pure_decl()"}
>  -doc_end
>  
> ++-doc_begin="The following autogenerated file is not linked deliberately."
> ++-file_tag+={C_runtime_failures,"^automation/eclair_analysis/C-runtime-failures\\.rst\\.c$"}
> ++-config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(file(C_runtime_failures)))"}
> ++-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
> -- 
> 2.34.1
> 

Re: [XEN PATCH v2 7/7] automation/eclair_analysis: avoid violation of MISRA Rule 2.1

[Stefano Stabellini]

On Mon, 18 Dec 2023, Stefano Stabellini wrote:
> On Mon, 18 Dec 2023, Nicola Vetrini wrote:
> > The presence of an unlinked object file triggers a violation
> > of MISRA C Rule 2.1, which is deviated, as it's not part of
> > the final Xen binary.
> > 
> > No functional change.
> > 
> > Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> 
> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
> 
> 
> > ---
> >  automation/eclair_analysis/ECLAIR/deviations.ecl | 5 +++++
> >  1 file changed, 5 insertions(+)
> > 
> > diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > index 85741a2c01a9..e3de0fb2adf8 100644
> > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > @@ -28,6 +28,11 @@ not executable, and therefore it is safe for them to be unreachable."
> >  -config=MC3R1.R2.1,ignored_stmts+={"any()", "pure_decl()"}
> >  -doc_end
> >  
> > ++-doc_begin="The following autogenerated file is not linked deliberately."
> > ++-file_tag+={C_runtime_failures,"^automation/eclair_analysis/C-runtime-failures\\.rst\\.c$"}
> > ++-config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(file(C_runtime_failures)))"}
> > ++-doc_end

Would it make sense to add it to exclude-list instead?

Re: [XEN PATCH v2 7/7] automation/eclair_analysis: avoid violation of MISRA Rule 2.1

[Nicola Vetrini]

On 2023-12-19 02:43, Stefano Stabellini wrote:
> On Mon, 18 Dec 2023, Stefano Stabellini wrote:
>> On Mon, 18 Dec 2023, Nicola Vetrini wrote:
>> > The presence of an unlinked object file triggers a violation
>> > of MISRA C Rule 2.1, which is deviated, as it's not part of
>> > the final Xen binary.
>> >
>> > No functional change.
>> >
>> > Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>> 
>> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
>> 
>> 
>> > ---
>> >  automation/eclair_analysis/ECLAIR/deviations.ecl | 5 +++++
>> >  1 file changed, 5 insertions(+)
>> >
>> > diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> > index 85741a2c01a9..e3de0fb2adf8 100644
>> > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
>> > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
>> > @@ -28,6 +28,11 @@ not executable, and therefore it is safe for them to be unreachable."
>> >  -config=MC3R1.R2.1,ignored_stmts+={"any()", "pure_decl()"}
>> >  -doc_end
>> >
>> > ++-doc_begin="The following autogenerated file is not linked deliberately."
>> > ++-file_tag+={C_runtime_failures,"^automation/eclair_analysis/C-runtime-failures\\.rst\\.c$"}
>> > ++-config=MC3R1.R2.1,reports+={deliberate, "any_area(any_loc(file(C_runtime_failures)))"}
>> > ++-doc_end
> 
> Would it make sense to add it to exclude-list instead?

I don't think so, because if some documentation about runtime error that 
is supposed to be here is missing it won't be obvious that the file that 
needs to be fixed is this. Moreover, you'd need to put the path of the 
generated .c file there, which I'm not sure how well it would behave 
w.r.t. other tooling.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)