Re: [XEN PATCH 10/11] xen/sched: add ASSERT_UNREACHABLE() to address MISRA C:2012 Rule 2.1

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

On Tue, 8 Aug 2023, Julien Grall wrote:
> On 08/08/2023 16:53, Nicola Vetrini wrote:
> > > > ... "return" alone already tells the compiler that "break" is
> > > > unreachable. You don't need unreachable() for that. As said before,
> > > > "break" like this simply want purging (and Misra is wrong to demand
> > > > "break" everywhere - it should instead demand no [unannotated]
> > > > fall-through, which can also be achieved by return, continue, and
> > > > goto).
> > > 
> > > My suggestion was in the context of this series where we add
> > > ASSERT_UNREACHABLE() before break. From my understanding, we don't
> > > have a lot of leeway here because, from what Nicola wrote, rule 16.3
> > > is mandatory.
> > > 
> > > So I think using unreachable is better if we every decide to use break
> > > after return.
> > > 
> > > Cheers,
> > 
> > 16.3 is not Mandatory, just Required.
> 
> Ah I misread what you wrote. In that case...
> 
> > I was just reluctant to knowingly add one more violation
> > while fixing another before submitting the patch. If indeed 16.3 won't
> > likely be adopted by Xen,
> > then that break should indeed go away.
> > 
> > However, the main thing that's holding me back from doing a slimmed-down v2
> > here is that
> > evidently there's no consensus even on the ASSERT_UNREACHABLE() patches.
> 
> ... I agree with the following statement from Jan:
> 
> "it should instead demand no [unannotated] fall-through, which can also be
> achieved by return, continue, and goto"

I also think it is a better idea to have no unannotated fall-through in
switch statements (unless we have a "case" with nothing underneath, so
two cases next to each other). In other words the following are all OK
in my view:

  case A:
    do();
    break;
  case B:
    do();
    return true;
  case Ca:
  case Cb:
    goto fail;
  case D:
    i++;
    continue;
  case E:
    do();
    /* fall-through */
  case F:
    do();
    break;

While the following is not OK:

  case A:
    do();
  case B:
    do();

This should be what we already do in Xen, although it is not documented
properly. Jan, Julien do you agree?

If so, could Eclair be configured to check for this pattern (or
similar)?

We must have one of the following:
- break, continue, return, goto
- /* fall-through */
- empty case body (case Ca/Cb)