Contracts for C (Early Stages)
5 days ago
- #contracts
- #C programming
- #optimization
- C++ contracts proposal (P2900) is being considered for adaptation in C, focusing on pre- and postconditions for function interfaces.
- Pre- and postconditions are verifiable conditions checked on function entry/exit, aiding optimization and correctness without affecting ABI.
- Conditions can be integer constant expressions, similar to static_assert, causing compilation failure if false.
- Two primitives introduced: contract_assert (similar to assert but always active) and contract_assume (dangerous if misused, assumes condition holds).
- Example shows my_malloc with pre(size) and post(r: r) conditions ensuring non-zero size and non-null return.
- Inline functions in headers can enforce contracts, with defer ensuring postconditions are checked on all exits.
- Observation: Redundant assertions/assumptions on the same condition can be optimized away by the compiler.
- Proposed execution model replaces pre/postconditions with assertions before calls and assumptions in function bodies.
- e��lipsis tool provides macros (EXBINDING/INBINDING) to simplify contract expression and avoid code duplication.
- Current limitations: Needs proper interface specification and compiler support, but serves as a proof of concept for C contracts.