Automatically make buggy code pass static checkers! Yay!

You mean, you could automatically convert existing buggy code into something semantically identical which passes all your new-fangled static checking.

You miss my point. I was just addressing backward-compatibility concerns when initally moving a lot of code to the new system. Certainly a conversion of a buggy program is still a buggy program (although the converter should highlight dubious bits in the code for possible corrections). The real value of the proposed new rules would be realized when writing new code or hand-modifying old.

splint already supports most of the things you suggest, without changes to the syntax of C itself (it uses comments and/or macros) or to the semantics of existing code.

So why isn't it used more? Answer: precisely because it is an extra pass, it is not installed everywhere the compiler is, and it requires extra annotations to be really useful. Correctness is not an add-on feature. Programmers should mind it all the time when writing code, without imagining it can be retrofitted with a final lint run, or with testing. Having every compiler run nag about dubious code helps better in achieving this. Anyway, my proposed changes are really not so much about adding extra statical checking, but removing totally unnecessary error sources from the language.