@dse said:Which one do you suggest?
I've used FindBugs, but it's a tool for Java IIRC. Wrote my own (a long time ago) but the language we were analysing was a bit unusual, as it was aimed at hardware synthesis instead of software systems. Hardware languages are a bit different to working with C (e.g., you go for a formally-finite type system in anything you are ever going to synthesise, have no memory allocation at all — memory is something you describe — and you've vast amounts of parallelism) and that has a whole load of downstream implications.
Aside from that, most of the approaches used in the field back when I was working in Formal Methods were actually based on being correct by construction, using provably correct methods to generate correct code from specifications. They were mostly aimed at safety critical applications like railway signalling. I've no personal experience with them, but my boss at the time was quite insistent that ad hoc after-the-fact proofs were a lot more difficult to work with.