On 08.08.2023 23:14, Stefano Stabellini wrote: > 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?
Yes. > 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 */ - fallthrough; (the pseudo keyword that we have; see compiler.h for actually having the documentation you're looking for, albeit missing "continue", and of course not really expected to live [just] there) Jan > - empty case body (case Ca/Cb)
