I just recently came upon a new C compiler, Deputy; anybody happen to have heard of it?
The idea sounded promising so I went ahead and built a copy on my linux box; it's actually a pretty interesting compiler. It can be used as a drop-in for GCC; files are linkable between the two compilers and if you link with deputy, you get the deputy RTL that will inform you of 'fishyness' in your code. It also provides many type annotations to describe common idioms. So you can use deputy to help check your code, but it can be built with existing libraries and the like (it uses the gcc-backend and you can pretty much just interchange them.)
Anybody else tried it? I don't have time right now, but I might try using the annotated code later.
CornedBee