(no title)
nanolith | 3 months ago
As an aside, it is one of the reasons why I finally decided to let go of C++ after 20 years of use. It was just too difficult to teach developers all of the corner cases. Instead, I retooled my system programming around C with model checking to enforce resource management and function contracts. The code can be read just like this example and I can have guaranteed resource management that is enforced at build time by checking function contracts.
dmpk2k|3 months ago
nanolith|3 months ago
I include function contracts as part of function declarations in headers. These take the form of macros that clearly define the function contract. The implementation of the function evaluates the preconditions at the start of the function, and is written with a single exit so the postconditions can be evaluated at the end of the function. Since this function contract is defined in the header, shadow functions can be written that simulate all possibilities of the function contract. The two are kept in sync because they both depend on the same header. This way, model checks can be written to focus on individual functions with any dependencies simulated by shadows.
The model checks are included in the same project, but are separate from the code under instrumentation, similar to how unit tests are commonly written. I include the shadow functions as an installation target for the library when it is installed in development mode, so that downstream projects can use existing shadow functions instead of writing their own.