Have you tried Astree Analyzer? Papers I read indicated it was one of best but hard to find industry people to confirm or reject it. Want someone to clone it for FOSS. Meanwhile, I found these free ones for you two that have each found bugs in code with focus on minimal annotations. All are academic prototypes but Saturn was used on Linux kernel.
Saturn http://saturn.stanford.edu/pages/overviewindex.html
CSolve http://goto.ucsd.edu/csolve/
Calysto http://www.domagoj-babic.com/index.php/ResearchProjects/Caly...
Most academics are instead making compilers that translate C code into something mostly or totally safe while pushing the performance hit downward. Here's two of the top for you to try on various codes (or improve):