Re: [XEN PATCH] docs/misra: document the C dialect and translation toolchain assumptions.

[Jan Beulich <jbeulich@xxxxxxxx>]

On 19.06.2023 12:53, Roberto Bagnara wrote:
> On 19/06/23 09:54, Jan Beulich wrote:
>> On 16.06.2023 17:54, Roberto Bagnara wrote:
>>> On 16/06/23 01:26, Stefano Stabellini wrote:
>>>> On Thu, 15 Jun 2023, Roberto Bagnara wrote:
>>>>> +       static function is used in an inline function with external 
>>>>> linkage:
>>>>> +          non-documented GCC extension.
>>>>
>>>> I am not sure if I follow about this one. Did you mean "static is used
>>>> in an inline function with external linkage" ?
>>>
>>> An inline function with external linkage can be inlined everywhere.
>>> If that calls a static functions, which is not available everywhere,
>>> the behavior is not defined.
>>
>> I guess I could do with an example where this leads to UB. What I'd expect
>> is that it leads to a compilation error.
> 
> Here are the two occurrences we have in ARM64 code:
> 
> violation for rule MC3R1.R1.1: (required) The program shall contain no 
> violations of the standard C syntax and constraints, and shall not exceed the 
> implementation's translation limits.
> xen/common/spinlock.c:316.29-316.40: Loc #1 [culprit: static function 
> `observe_head(spinlock_tickets_t*)' is used in an inline function with 
> external linkage (ill-formed for the C99 standard, ISO/IEC 9899:1999: "An 
> ill-formed source detected by the parser."
> xen/common/spinlock.c:301.26-301.37: Loc #2 [evidence: 
> `observe_head(spinlock_tickets_t*)' declared here]
> xen/include/xen/spinlock.h:180.1-180.4: Loc #3 [evidence: use 'static' to 
> give inline function `_spin_lock_cb(spinlock_t*, void(*)(void*), void*)' 
> internal linkage]
> 
> violation for rule MC3R1.R1.1: (required) The program shall contain no 
> violations of the standard C syntax and constraints, and shall not exceed the 
> implementation's translation limits.
> xen/common/spinlock.c:324.5-324.12: Loc #1 [culprit: static function 
> `got_lock(union lock_debug*)' is used in an inline function with external 
> linkage (ill-formed for the C99 standard, ISO/IEC 9899:1999: "An ill-formed 
> source detected by the parser."
> xen/common/spinlock.c:227.13-227.20: Loc #2 [evidence: `got_lock(union 
> lock_debug*)' declared here]
> xen/include/xen/spinlock.h:180.1-180.4: Loc #3 [evidence: use 'static' to 
> give inline function `_spin_lock_cb(spinlock_t*, void(*)(void*), void*)' 
> internal linkage]

I know _spin_lock_cb() was an example of a violation (it isn't anymore),
but this does not serve as an example for the UB you claim may occur.
The "inline" there was in a .c file, and hence the function could only
be inlined with its (static) helper also in scope.

Jan