Re: [PATCH 3/3] misra: add deviation of Rule 10.1 for unary minus

[Jan Beulich <jbeulich@xxxxxxxx>]

On 23.04.2025 01:43, victorm.lira@xxxxxxx wrote:
> From: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> 
> The unary minus operator applied to an unsigned quantity has
> a semantics (wrap around) that is well-known to all Xen developers.
> Thus, this operation is deemed safe.

Please, as you have it in the other two patches, can the rule title be
reproduced in such patches? As it stands, without mentioning the doc
version either, someone finding this later on may be left with a pretty
wide ambiguity as to what's meant.

> No functional change.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> Signed-off-by: Federico Serafini <federico.serafini@xxxxxxxxxxx>
> Signed-off-by: Victor Lira <victorm.lira@xxxxxxx>
> ---
> Cc: Andrew Cooper <andrew.cooper3@xxxxxxxxxx>
> Cc: Anthony PERARD <anthony.perard@xxxxxxxxxx>
> Cc: Michal Orzel <michal.orzel@xxxxxxx>
> Cc: Jan Beulich <jbeulich@xxxxxxxx>
> Cc: Julien Grall <julien@xxxxxxx>
> Cc: Roger Pau Monné <roger.pau@xxxxxxxxxx>
> Cc: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> Cc: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> Cc: Federico Serafini <federico.serafini@xxxxxxxxxxx>
> Cc: Bertrand Marquis <bertrand.marquis@xxxxxxx>
> ---
>  automation/eclair_analysis/ECLAIR/deviations.ecl | 6 ++++++
>  docs/misra/deviations.rst                        | 6 ++++++
>  2 files changed, 12 insertions(+)
> 
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
> b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 303b06203a..2cfce850bd 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -347,6 +347,12 @@ constant expressions are required.\""
>    "any()"}
>  -doc_end
> 
> +-doc_begin="Unary minus operations on non-negative integers have a semantics 
> (wrap around) that is well-known to all Xen developers."

Why "non-negative"? A variable of type "int" holding a non-negative value is,
aiui, well within the bounds of the rule here. It's unsigned types where the
use of unary minus would constitute a violation. You actually say so ...

> +-config=MC3A2.R10.1,etypes+={safe,
> +  "stmt(node(unary_operator)&&operator(minus))",
> +  "src_expr(definitely_in(0..))"}
> +-doc_end
> +
>  #
>  # Series 11
>  #
> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> index a93ef1ff44..8c1f97358a 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -321,6 +321,12 @@ Deviations related to MISRA C:2012 Rules:
>         If no bits are set, 0 is returned.
>       - Tagged as `safe` for ECLAIR.
> 
> +   * - R10.1
> +     - Applying the unary minus operator to an unsigned quantity has a
> +       semantics (wrap around) that is well-known to all Xen developers.
> +       For this reason, the operation is safe.
> +     - Tagged as `safe` for ECLAIR.

... here, just that this one's getting blurred by using "quantity" when
"type" is meant. Imo we need to be pretty precise here, using terminology
that's used by the standard or the Misra rules, and not anything "coming
close enough" in someone's perception.

Jan