Annotating fall through case statements in a switch

Accidental fall throughs in a switch statement can lead to some nasty bugs. I have used the following banner for quite a long time to indicate that the fall through is intentional and not an oversite (this banner is also a part of the KMDF coding guidelines). It has definitely helped me debug coding mistakes over the years.

     case IRP_MJ_DEVICE_CONTROL:
    case IRP_MJ_INTERNAL_DEVICE_CONTROL:
        //    ||  ||  Fall through  ||   ||
        //    \/  \/                \/   \/
    default:
        return NULL;
    }

While the banner is certainly human readable, it is not apparent to static analysis tools that the fall through was intentional. Today I discovered that there is a SAL annotation, __fallthrough, which can indicate the intentional fall through. This means you can annotate the code and tools like PreFAST and PreFAST for Drivers can better understand and analyze the code. I have not yet decided if I want to use the annotation by itself without the current banner or addition to my current banner. I am leaning towards just using the annotation though.