[mjn]

A side note I took away from this post is the existence of Frama-C, which appears to be a quite nice, open-source analyzer: http://frama-c.com/