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;