Re: [XEN PATCH] automation/eclair: extend deviations of MISRA C:2012 Rule 16.3

[Federico Serafini <federico.serafini@xxxxxxxxxxx>]

On 28/02/24 10:06, Jan Beulich wrote:
> On 28.02.2024 09:53, Federico Serafini wrote:
> > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> Comments below apply similarly to text added to this file.
>
> > --- a/docs/misra/deviations.rst
> > +++ b/docs/misra/deviations.rst
> > @@ -291,7 +291,14 @@ Deviations related to MISRA C:2012 Rules:
> >        - Project-wide deviation; tagged as `deliberate` for ECLAIR.
> >   
> >      * - R16.3
> > -     - Switch clauses ending with continue, goto, return statements are safe.
> > +     - Switch clauses ending with an unconditional flow control statement
> > +       (i.e., continue, goto, or return) are safe.
> > +     - Tagged as `safe` for ECLAIR.
> With this edit (unmentioned in the description, btw) ...
>
> > +   * - R16.3
> > +     - Switch clauses ending with an if-else statement are safe if both
> > +       branches consist of a flow control statement (i.e., continue, break,
> > +       goto, return).
> ... why is it not also "ending with" here?
Because the allowed pattern is:

if ( cond )
 return; /* Or continue / break / goto */
else
 break;  /* Or continue / goto / return */

See below for more information.

> Also what about either situation ending with a call to a noreturn function?
This can be added.

> > @@ -307,6 +314,16 @@ Deviations related to MISRA C:2012 Rules:
> >        - Switch clauses ending with failure method \"BUG()\" are safe.
> >        - Tagged as `safe` for ECLAIR.
> >   
> > +   * - R16.3
> > +     - On X86, switch clauses ending generating an exception through
> > +       \"generate_exception()\" are safe.
> > +     - Tagged as `safe` for ECLAIR.
> This macro is limited to the emulator, so shouldn't be deviated globally.
Noted.

> Furthermore - why does the special case need mentioning here? Shouldn't
> it be the underlying pattern which is deviated (along the lines of the
> earlier ones):
>
>      if ( true )
>      {
>          ...
>          goto ...; /* Or break / continue / return */
>      }
This pattern that involves a compound statement for the true branch
is not deviated by this configuration.

See below for more information.

> > +   * - R16.3
> > +     - Switch clauses ending generating a parse error through
> > +       \"PARSE_ERR_RET()\" are safe.
> > +     - Tagged as `safe` for ECLAIR.
> Again this isn't a global scope macro, so shouldn't be deviated globally.
Noted.

> Plus it ends in "return", so ought to be covered by the earlier clause.
> The fact that the return is in a body of do {} while(0) shouldn't matter
> at all - that's purely syntactic sugar.
I gather from your comments/questions that you would like to deviate
*all* the patterns where an unintentional fall through can not happen.

Rule 16.3 is a purely syntactic rule, and, as a consequence,
in the current version of ECLAIR additional "allowed pattern" (aka
deviations) for that rule need to be described through AST nodes,
meaning that all what you consider as syntactic sugar cannot be ignored.

A deviation that covers all the pattern you are asking for could be
done, but it will result in a complex and quite long expression
(not easy to read and justify in front of an assessor).

Hence, what I am proposing is to deviate only the the simplest and
most readable cases, such as:

if ( cond )
  return x;
else
  return y;

without involving compound statements, fake do-wile and fake if
statements but rather deviating the macro inside of which are used
(as I did).

--
Federico Serafini, M.Sc.

Software Engineer, BUGSENG (http://bugseng.com)