https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81230
Jakub Jelinek <jakub at gcc dot gnu.org> changed:
What |Removed |Added
----------------------------------------------------------------------------
Status|UNCONFIRMED |RESOLVED
CC| |jakub at gcc dot gnu.org
Resolution|--- |INVALID
--- Comment #2 from Jakub Jelinek <jakub at gcc dot gnu.org> ---
Yes, it is documented.
The comment needs to be followed after optional whitespace and other comments
by @code{case} or @code{default} keywords or by a user label that precedes some
@code{case} or @code{default} label.
So the reporter has just not read the documentation.
They can either move the comment, or use attribute which can be used even
inside of the {}s.