Re: [PATCH 5/6] x86/Viridian: annotate Eclair false-positives for rule 18.2

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 2026-09-09 15:01, Jan Beulich wrote:
> "Subtraction between pointers shall only be applied to pointers that
> address elements of the same array" is not violated here: 
> start_stimer()
> is only ever passed a sane argument, and stimer_expire() is either 
> called
> from start_stimer() (using its parameter as argument) or as a callback,
> where a sane callback argument is also guaranteed to be set up.
>
> Suggested-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> Signed-off-by: Jan Beulich <jbeulich@xxxxxxxx>
> ---
> As per Nicola Eclair 16.0.0 has this fixed.
Perhaps I didn't express clearly that the remark was about the violation 
annotated in patch 4/6. Here instead, a suitable reproducer is not yet 
available. Nevertheless, if the claim is true the approach to address 
the violation is still ok.
> --- a/docs/misra/false-positive-eclair.json
> +++ b/docs/misra/false-positive-eclair.json
> @@ -10,6 +10,13 @@
>          },
>          {
>              "id": "SAF-1-false-positive-eclair",
> +            "violation-id": "MC3A2.R18.2",
> +            "tool-version": "3.14.0",
> +            "name": "Rule 18.2: pointer subtraction",
> +            "text": "Viridian stimer index calculations use sane 
> pointers"
> +        },
> +        {
> +            "id": "SAF-2-false-positive-eclair",
>              "violation-id": "",
>              "tool-version": "",
>              "name": "Sentinel",
> --- a/xen/arch/x86/hvm/viridian/time.c
> +++ b/xen/arch/x86/hvm/viridian/time.c
> @@ -136,6 +136,7 @@ static void cf_check stimer_expire(void
>      struct viridian_stimer *vs = data;
>      struct vcpu *v = vs->v;
>      struct viridian_vcpu *vv = v->arch.hvm.viridian;
> +    /* SAF-1-false-positive-eclair vs is always sane */
>      unsigned int stimerx = vs - &vv->stimer[0];
>
>      set_bit(stimerx, &vv->stimer_pending);
> @@ -146,6 +147,7 @@ static void start_stimer(struct viridian
>  {
>      const struct vcpu *v = vs->v;
>      struct viridian_vcpu *vv = v->arch.hvm.viridian;
> +    /* SAF-1-false-positive-eclair vs is always sane */
>      unsigned int stimerx = vs - &vv->stimer[0];
>      int64_t now = time_ref_count(v->domain);
>      int64_t expiration;
--
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253