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

[Dmytro Prokopchuk1 <dmytro_prokopchuk1@xxxxxxxx>]

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>
---
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;
-- 
2.43.0