> diff --git a/xen/arch/arm/psci.c b/xen/arch/arm/psci.c
> index 695d2fa1f1..2a8527cacc 100644
> --- a/xen/arch/arm/psci.c
> +++ b/xen/arch/arm/psci.c
> @@ -59,6 +59,7 @@ void call_psci_cpu_off(void)
> }
> }
> +/* SAF-2-safe */
I think any use of SAF-2-safe should be accompanied with an
attribute...
> void call_psci_system_off(void)
... noreturn for function or ...
> {
> if ( psci_ver > PSCI_VERSION(0, 1) )
> diff --git a/xen/arch/x86/shutdown.c b/xen/arch/x86/shutdown.c
> index 7619544d14..47e0f59024 100644
> --- a/xen/arch/x86/shutdown.c
> +++ b/xen/arch/x86/shutdown.c
> @@ -118,6 +118,7 @@ static inline void kb_wait(void)
> break;
> }
> +/* SAF-2-safe */
> static void noreturn cf_check __machine_halt(void *unused)
> {
> local_irq_disable();
> diff --git a/xen/include/xen/bug.h b/xen/include/xen/bug.h
> index e8a4eea71a..d47c54f034 100644
> --- a/xen/include/xen/bug.h
> +++ b/xen/include/xen/bug.h
> @@ -117,6 +117,7 @@ struct bug_frame {
> #endif
> #ifndef BUG
> +/* SAF-2-safe */
> #define BUG() do { \
> BUG_FRAME(BUGFRAME_bug, __LINE__, __FILE__, 0, NULL); \
> unreachable(); \
... unreachable for macros. But the /* SAF-2-safe */ feels a little
bit
redundant when a function is marked as 'noreturn'.
Is there any way to teach eclair about noreturn?
Actually I had the same thought while writing this patch. If we can
adopt unreachable and noreturn consistently maybe we don't need
SAF-2-safe. If the checker can support it.
Nicola, what do you think?
A couple of remarks:
- if you put the noreturn attribute on some functions, then surely the
code after those is
reported as unreachable. ECLAIR should pick up all forms of noreturn
automatically; otherwise, a simple configuration can be used.
- Note that the cause of unreachability in the vast majority of cases is
the call to
__builtin_unreachable(), therefore a textual deviation on the definition
of unreachable, plus
a bit of ECLAIR configuration, can deviate it (to be clear, just the SAF
comment is not
sufficient, since deviations comments are meant to be applied at the top
expansion location,
which is not on the macro definition).
This is what it should look like, roughly:
-config=MC3R1.R2.1,reports+={deliberate,
"any_area(any_loc(text(^<REGEX>$, -1)))"}
#if (!defined(__clang__) && (__GNUC__ == 4) && (__GNUC_MINOR__ < 5))
/* SAF-2-safe */
#define unreachable() do {} while (1)
#else
/* SAF-2-safe */
#define unreachable() __builtin_unreachable()
#endif
where REGEX will match the translation of SAF-2-safe.
However, this will then entail that *some* SAF comments are treated
specially and, moreover,
that some modification to the definition of unreachable won't work
(e.g.
#define M() __builtin_unreachable()
/* SAF-2-safe */
#define unreachable() M()
My opinion is that it's far easier for this to be an eclair
configuration (which has the
advantage not to depend on the exact definition of unreachable) and then
perhaps a comment
above it explaining the situation.
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)