I gave a talk about Frama-C a few years ago. It's very interesting technology, but not too useful at any scale (http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4) One aim we had with Bounds Checking GCC back in '95 was to make it possible to use with real programs. Although it was quite slow, any open source program of the era could use it (https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html).
CBMC works best with a contract-based programming style, where contracts are enforced by assertions and shadow functions exist to simplify model checking.
A single reply on HN is hardly a place where idiomatic styles can be expounded, but it is quite possible to build a resource-oriented idiomatic style that is reinforced with CBMC.
This led to the creation of function contracts and shadow functions. When evaluating functions, we actually want any calls that it makes to go to shadow functions instead of real functions. When we write a function, we include a contract that includes anything it may return, any side-effects it may have, and any memory it may touch / allocate / initialize. We then write a twin function -- its shadow function -- that technically follows the same contract in the most simplified terms, randomly choosing whether to succeed or fail. From CBMC's perspective, it's equivalent enough for model checking. But, it removes additional stack depth or recursion.
A good example of this would be a shadow function for the POSIX read function. Its contract should verify that the descriptor it is passed is valid. It should also assert that the memory region it is passed is bounded by the size it is given. The shadow function picks a non-deterministic state based on how it should set errno and how it should return. This state follows the POSIX standard, but the underlying system calls don't matter. Likewise, depending on the return code, it should initialize a number of bytes in the read buffer with non-deterministic values.
I used this shadow read function to find a buffer overflow in networking code and also to find a DOS infinite loop error in a tagged binary file format reader we were using.
CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.
I agree to a certain extent, but at what point are you putting in more effort than it would take to migrate to a stricter language that offers more safety by default?
I'd say that the added effort is minimal. The compiler spits out more errors. We think a little more carefully about how we write functions so CBMC doesn't complain. There are no silver bullets.
>While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation. Typical theories of interest in these applications include formalizations of arithmetic, arrays, bit vectors, algebraic datatypes, equality with uninterpreted functions, and various combinations of these.
Not that I'm an expert in processing what exactly is being tested, but it basically looks only able to prove that an individual function doesn't overrun buffers. If you tell it to assume that integer overflows can't happen (!). So I'm not impressed.