Contracts for C (Early Stages)

Summary

C++ seems to finally converge with their contracts proposal, https://wg21.link/p2900. I decided to give it a try and come up with ideas how such a thing would look for C. This is in early stages, not a full proposal yet, and still would need implementation by some of the major compilers. In particular, the C++ feature is full of sidetracks that I don’t like at all, such as user-defined global handlers and ignorability. But there is a core of ideas, syntax and semantics that I found interesting and that I think should be considered for C. The principal features are Contract pre- and postconditions add verifiable conditions that are added to function interfaces. They are checked on entry to a function call and provide knowledge that is valuable for the code following a call. If the condition is an integer constant expression, a pre- or postcondition is similar to an invocation of static_assert. If the condition is false, compilation fails. In the following we will not illustrate this aspect to simplify the discourse. They have no implications on ABI. They can be made composable. If applied rigorously, such conditions can often be deduced from the context. They need not be checked dynamically. Besides verified correctness, they offer optimization opportunities for the context of a function call and for the called function itself. To see how all of this works we first need understand two fundamental primitives, assertions and assumptions. Their syntax looks something like contract_assert(COND, "some explanatory text"); contract_assume(COND, "some explanatory text"); Here, in both cases COND is some condition that is supposed to be fulfilled. The first, contract_assert, is quite similar to a feature that we already have in C namely the assert macro. Both test for the condition; if it is fulfilled nothing happens and execution goes on. If it is not fulfilled, a diagnostic is printed to stderr and abort is called to end the execution. The difference to assert is that contr...