Re: [PATCH v3] automation/eclair: generalize the noreturn function-pointer deviation

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2026-10-19 10:51, Dmytro Prokopchuk1 wrote:
> The R11.1 safe cast only matched void noreturn (*)(void *). Accept a
> conversion where noreturn is omitted and the signature is otherwise
> compatible. canonical() covers typeof destinations, and
> compatible_deep_unqualified keeps the parameter and return types 
> aligned.
> Discarding noreturn does not change the calling convention. Code after
> the call is unreachable when every possible callee is noreturn. Leaving
> that code in place is a tolerated Rule 2.1 violation. The full 
> rationale
> is in docs/misra/deviations.rst.
>
> Signed-off-by: Dmytro Prokopchuk <dmytro_prokopchuk1@xxxxxxxx>
Acked-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx> # 
automation/eclair_analysis/.*
> ---
> Changes in v3:
> - Reworded the deviation text per Jan's review: "noreturn omitted but 
> an
>   otherwise compatible signature", "all of the possible callees", and a
>   tolerated Rule 2.1 violation
> - rules.rst: use '(void *)' spelling
>
> Changes in v2:
> - do not claim that discarding noreturn leaves compiler behavior 
> unchanged
> - write that code after the call is unreachable, and that Xen's 
> behavior
>   is the same (whether the compiler deletes that code or leaves it)
> ---
>  automation/eclair_analysis/ECLAIR/deviations.ecl |  9 +++++----
>  docs/misra/deviations.rst                        | 12 ++++++++----
>  docs/misra/rules.rst                             |  8 +++++---
>  3 files changed, 18 insertions(+), 11 deletions(-)
>
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
> b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 6cdb10a129..c7a800c62f 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -394,11 +394,12 @@ constant expressions are required.\""
>  }
>  -doc_end
>
> --doc_begin="The conversion from 'void noreturn (*)(void *)' to 'void 
> (*)(void *)' is safe
> -because the semantics of the 'noreturn' attribute do not alter the 
> calling convention or behavior of the resulting code."
> +-doc_begin="The conversion from a noreturn function pointer to a 
> function
> +pointer with noreturn omitted but an otherwise compatible signature 
> does
> +not alter the calling convention."
>  -config=MC3A2.R11.1,casts+={safe,
> -  
> "kind(bitcast)&&to(type(pointer(inner(return(builtin(void))&&all_param(1, 
> pointer(builtin(void)))))))&&from(expr(skip(!syntactic(),
> -   ref(property(noreturn)))))"}
> +  
> "kind(bitcast)&&to(type(canonical(__function_pointer_types)))&&from(expr(skip(!syntactic(),
> +   ref(property(noreturn)))))&&relation(compatible_deep_unqualified)"}
>  -doc_end
>
>  -doc_begin="The conversion from a pointer to an incomplete type to 
> unsigned long does not lose any information, provided that the target 
> type has enough bits to store it."
> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> index 6bcc2adf95..76be6b3251 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -392,10 +392,14 @@ Deviations related to MISRA C:2012 Rules:
>       - Tagged as `safe` for ECLAIR.
>
>     * - R11.1
> -     - The conversion from 'void noreturn (*)(...)' to 'void (*)(...)' 
> is safe
> -       because the semantics of the 'noreturn' attribute do not alter 
> the calling
> -       convention or behavior of the resulting code, parameters 
> handling remain
> -       consistent.
> +     - The conversion from a noreturn function pointer to a function 
> pointer
> +       with noreturn omitted but an otherwise compatible signature 
> does not
> +       alter the calling convention. The callee does not return, so 
> code
> +       following a call through the resulting pointer is unreachable. 
> The
> +       compiler may delete that unreachable code when it can see that 
> all
> +       of the possible callees are noreturn, or it may leave the code 
> in
> +       place. Xen's behavior is the same in either case. Code left in 
> place
> +       is a tolerated violation of Rule 2.1.
>       - Tagged as `safe` for ECLAIR.
>
>     * - R11.2
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index a59cf1782e..5f9fe4c860 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -435,9 +435,11 @@ maintainers if you want to suggest a change.
>         and any other type
>       - All conversions to integer types are permitted if the 
> destination
>         type has enough bits to hold the entire value. Conversions to 
> bool
> -       and void* are permitted. Conversions from 'void noreturn 
> (*)(...)'
> -       to 'void (*)(...)' are permitted. Conversions from [unsigned] 
> long
> -       or '(void *)' to a function pointer are permitted.
> +       and '(void *)' are permitted. Conversions from a noreturn 
> function
> +       pointer to a function pointer with noreturn omitted but an 
> otherwise
> +       compatible signature are permitted.
> +       Conversions from [unsigned] long or '(void *)' to a function 
> pointer
> +       are permitted.
>         Example::
>
>             unsigned long func_addr = (unsigned long)&some_function;
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253