I'd rather use CBMC symbolic verification. Only one C code, also it's contracts, no ACSL needed.
The verifiers targets the whole range of the symbolic input. No need for expensive unit-testing over a single input value or random input values. You test all possible values. It's fast and practical.
Which is not feasible if there are, say 2^128 or more possible values. CBMC is a model checker, which is very useful for many problems that can be brute-forced but not the same thing as the correct-by-construction approach of Frama-C style formal methods, which deductively verifies that code works on all possible cases, even all conceivable edge cases, without having to exhaustively test all cases.
I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought.
CBMC can also be used for programs with unbounded loops. In this
case, CBMC is used for bug hunting only; CBMC does not attempt to
find all bugs.
Frama-C is about eliminating ALL bugs, you are allowed to prove your "unbounded" loop algorithm actually terminates, and terminates with the correct solution, if you are willing to learn to use the manual proof assistant. CBMC can check for an extremely important class of errors, but it doesn't let you prove, say, your traveling salesman solver always returns a shortest trip T through the graph G, or that the graph coloring register allocator for your C compiler always correctly colors the graph, something that is actually done for the CompCert formally verified C compiler (using the Coq/Gallina proof assistant, which can be used with Frama-C).
However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply,
$ sudo apt install cbmc
So I plan to give cprover a shot now, thanks for the heads up. : )
