Re: xen-analysis ECLAIR support

[Michal Orzel <michal.orzel@xxxxxxx>]

Hi Stefano,

On 25/08/2023 00:24, Stefano Stabellini wrote:
> 
> 
> Hi Luca,
> 
> We are looking into adding ECLAIR support for xen-analysis so that we
> can use the SAF-n-safe tags also with ECLAIR.
> 
> One question that came up is about multi-line statements. For instance,
> in a case like the following:
> 
> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
> index 8fa4b96d12..8bdc9208da 100644
> --- a/xen/common/inflate.c
> +++ b/xen/common/inflate.c
> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>      magic[1] = NEXTBYTE();
>      method   = NEXTBYTE();
> 
> +    /* SAF-1-safe */
>      if (magic[0] != 037 ||
>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>          error("bad gzip magic numbers");
> 
> 
> Would SAF-1-safe cover both 037, and also 0213 and 0213?
> Or would it cover only 037?
> 
> We haven't use SAFE-n-safe extensively through the codebase yet but
> my understanding is that SAFE-n-safe would cover the entire statement of
> the following line, even if it is multi-line. Is that also your
> understanding? Does it work like that with cppcheck?
Looking at the docs and the actual script, only the single line below SAF 
comment is excluded.
So in your case you would require:

/* SAF-1-safe */
if (magic[0] != 037 ||
    /* SAF-1-safe */
    ((magic[1] != 0213) && (magic[1] != 0236))) {
    error("bad gzip magic numbers");

I guess this was done so that it is clear that someone took all the parts of 
the statements into account
and all of them fall into the same justification (which might not be the case).

BTW. I don't think we have also covered the case where there is more than one 
violation in a single line
that we want to deviate (e.g. sth like /* SAF-1-safe, SAF-2-safe */

~Michal