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):

https://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/

http://sva.cs.illinois.edu/downloads.html

Pretty much what we already use.

I was hoping for something new.