C semantics for contracts

Jens Gustedt, INRIA and ICube, France

2026-01-25

target

preliminary discussion for possible integration into IS ISO/IEC 9899:202y

document history

document number date comment
n3739 202511 Original proposal
n3789 202601 Retire the “syntactically equivalent” concept
Require that at most one declaration has contracts
Use “ghost state” instead of “ghost variable”
Add invariants as composition of pre- and postconditions
Simplify the example
Add more examples
Make _ReturnValue visible in preconditions
Add implicit conversion

license

CC BY, see https://creativecommons.org/licenses/by/4.0

1 Motivation

Traditionally, C’s function interfaces are particularly poor in the way information that can be transferred from the calling context into the caller and even poorer for the way back from the called function back to the caller. Originally, C only accounted for the number of arguments of a call and the return type, the addition of prototypes to the language added more static information about parameter types. This has later be enriched with only some more bits of dynamic information, in particular array sizes.

The goal of this paper is to continue this process of improvement of interface specifications to the dynamic verification of predicates which the current syntax is not capable to assert. Algorithmic invariants or properties that are needed for optimization are not expressible in the interfaces that the language currently offers and, in general, are either missed, annotated manually with external tools, or, most commonly, by handwritten textual proofs.

Nevertheless, many predicates that would be needed here can be written as C expressions, provided that we add some additional state that, without interacting with the core of the computation, helps to propagate properties forward. The goal of this paper is to show how function interfaces in C can be enriched such that necessary predicates for calling them and conclusions from a call can be naturally expressed in otherwise existing C syntax and semantics. The core argument of this paper is to show that this execution model, with reasonable assumptions on the acceptable predicates, is equivalent to an implementation in conventional C where shallow inline wrappers execute cascaded if statements to check the predicates.

The goal of this paper is not to provide methods for hardening existing interfaces, and, in particular, the C library. In the contrary, adding contracts as proposed here changes the semantics of interfaces (in general from UB to well-defined failures) and they are thus not suited to paint over existing deficiencies in interface design.

2 Related features

Numerous tools exist in the field that ensure the check of predicates, usually expressed either as assertions or as pre- or postconditions. In the following we discuss three of them that have had the most influence on this proposal, here. The main motivation came from a similar feature that is a candidate to make it into C++26, C++ contracts; others are the traditional assert macro and Annex K of the C standard.

2.1 C++ contracts

C++ contracts are a complicated feature, in particular they let implementations chose between different semantics of a translated contract (ignore, observe, enforce and quick-enforce). Additionally, for two of these semantics (observe and enforce) they allow to configure behavior in the case of a contract violation by means of a user-supplied contract handler, ::handle_contract_violation.

We don’t think that this whole spectrum of possibilities is adequate for a C feature. First, for C it is not appropriate that readily compiled translation units (such as the C library or other third-party libraries) change behavior by means of a user-supplied contract handler. Second, the ignore semantics are counter-productive as they inhibit the evaluation of the predicate, and thus change semantics even in case that a contract holds. Thereby, the ignore semantics partially repeat a design error that was already present for C’s assert feature, see below. Third, C++ contracts allow the predicates to have side-effects, which makes it difficult to argue about semantics of contracts and which makes it impossible for both the caller and the callee to check the contract independently if necessary.

As a consequence our proposal only is completely compatible with C++’s quick-enforce semantics, and this only if the contract has no side effects. In addition to that, we provide undefined-behavior semantics that actually assume that the predicate is evaluated but imply undefined behavior if it doesn’t hold. These may be different from C++’s ignore semantics even in the case that the evaluated predicate doesn’t have side-effects. Namely, as proposed here for C an optimizing compiler will be able to assume that the predicate holds unconditionally in all code that is sequenced after the evaluation.

Other features in our proposal that are different from C++ contracts:

Our proposed feature is meant to be compatible to C++ contracts at least for the quick-enforce semantics and in the absence of side-effects. We impose that the strategy in case of a contract violation is statically determined for each assertion and pre- or postcondition, and that either the execution (of the program or thread) terminates or that the execution continues as-if with an invocation of unreachable. In any case, a C proposal for contracts cannot have exactly the same syntax as for C++, because C++ uses syntactic concepts that are not available in C. Nevertheless, we try to provide a syntax that can be mapped between the languages by using some macro glue.

2.2 The assert C library macro

Historically, C also has a macro that is intended to diagnose the violation of a given predicate, assert from clause 7.2 “Diagnostics <assert.h>”. Unfortunately this macro has not aged well and lacks capacities that would be needed in a modern environment of translators with improved optimization capabilities or even with integrated static analyzers. The main defect of that macro is that it is switched off as a whole by the user defined macro NDEBUG and that thus the resulting executables have different syntax and semantics:

These semantic defects seem to be shared with C++’s ignore semantics.

Another issue with assert is that it uses abort to terminate the execution. Leaving invocations of assert without using NDEBUG is problematic:

One goal of this paper here is to provide a better tool that in the future could replace uses of assert that are meant what the name verbally indicates, namely where the users seeks to assert a specific property. On the other hand, uses of assert as a diagnostic tool (and which goal is indicated by the clause header of 7.2 “Diagnostics”) would and should not be replaced.

2.3 Annex K, “bounds checking”

For the C library, Annex K has already taken the approach to replace the existing C library interfaces by new variants that make more guarantees and that introduce runtime checks for constraints. This can be seen as a case-study to amended specific C library interfaces. What are called runtime constraints, there, has a lot of similarities with predicates as defined in this paper.

Our approach differs from Annex K in multiple ways

3 Approach

As it is the common model in C, we will assume that the functions that make up a program are split in translation units, TU, that each correspond to a C file that is compiled separately from all the others. A TU knows about functions in another TU only by declarations, most properties of these other functions are hidden. The advantages of such an approach are plenty, for example modularization, maintainability and fast compilation times, but there are also severe disadvantages: false assumptions lead to complicated bugs and lack of information misses optimization opportunities.

The proposed model for adding contracts to C interfaces is relatively simple at the surface: we create the possibility to add a list of contracts (pre-, postconditions and invariants) to function declarations, right after the closing parenthesis of the parameter list (resp. after possible attributes). Contracts can effectively be checked from the calling context of a function or within the function itself (or both) without leading to semantic differences. The intent is that in general for preconditions the check is effected in the caller and for postconditions in the callee, such that these checks may seamlessly use knowledge that is already present in these contexts.

We took care that contracts as proposed here

3.1 Design choices

There is a multitude of possible design choices for contracts, but for us, when restricted to the context of C, several choices seemed to impose themselves.

3.1.1 Overall design

Our main choices for the feature are as follows; changing any of these substantially would possibly invalidate the approach as a whole.

3.1.2 Termination

A crucial property of contracts is, that, in general, a violated predicate terminates execution. As of today, after more than half a century of C, there is still no established strategy on how to terminate an erroneous execution; the C standard alone has 6 different features (exit, quick_exit, _Exit, thrd_exit, abort and signals). Indeed, depending on the field, requirements for such termination are very different; in some contexts a graceful exit with cleanup is completely adequate; others should never terminate at all (such as an operating system); some cannot assure any consistent behavior after a violation and should halt instantly without any cleanup.

For these reasons we left the specific choice how to terminate by default to the implementation. They are best placed to offer the necessary tools and local choices to their customers. Additionally, we provide a configuration macro __STDC_CONTRACT_BEHAVIOR__ that provides three different choices about the extent to which a particular termination policy applies:

predefined macro value
__STDC_CONTRACT_BEHAVIOR_DEFAULT__ 0 default behavior
__STDC_CONTRACT_BEHAVIOR_UNREACHABLE__ 1 unreachable()
__STDC_CONTRACT_BEHAVIOR_TERMINATE__ 2 function call

All of these decide behavior at compilation time for each specific translation unit, before linkage.

The first, default behavior, fixes the behavior to whatever the implementation chooses for a given binary translation unit. This mode is particularly important for providers of libraries that cannot afford that user code (or other libraries) impose a different termination strategy on them. Implementations may want provide fine-tuning for this policy by means of command line arguments or configuration macros; such a specification is willingly left out of the proposed text.

The second leads to undefined behavior in case of the violation of a predicate, as-if all contracts had been formulated with just assumptions instead of assertions. Performance critical applications that are not worried about the impact of failed executions on their system may chose this mode, but such a choice should only be done after intensive testing. Talk to your layers first.

The third mode is a form of compromise as it delegates the policy choice to a single, per-program external function. This mode is perhaps a good choice during debugging or for programs that don’t have high risk of damage when a predicate is violated.

Other values and policies may be added by implementations.

3.1.3 Enforcing consistency within the same TU

Different declarations of the same function with contracts within the same TU would raise the question of consistency between those declarations. An early version of this paper attempted to provide a mechanism that would enforce consistency, but was considered too complicated, at least for an initial specification of such a features.

Instead, we now require that exactly one declaration may be annotated with contracts, such that a contradiction can simply not occur. For functions that are defined before possibly being redeclared (in general static or inline functions) contracts should be specified there; for functions that are forward declared in headers and then only defined in one TU, the contract is assumed to be at the forward declaration.

Within the same TU, function types with contracts can only be compatible if they are the same, that is if they refer to the same function type declaration; no redeclaration with contracts of a function type that already has them leads to a compatible type. Thereby function pointers to functions with contracts can only be interchanged if they refer to the same original type, and not a redeclaration of a compatible type. In cases where there is need for such a design, forward declarations with contracts should refer to a common type either by using a typedef:

typedef void* allocation_type(size_t n) _Post(_ReturnValue);
allocation_type my_malloc;
allocation_type my_arena;
allocation_type* what_can_we_do_for_you_today = my_arena;

or by using typeof to avoid a redeclaration

void* my_alloc(size_t n) _Post(_ReturnValue);
typeof(my_alloc) my_arena;
typeof(my_alloc)* what_can_we_do_for_you_today = my_arena;

3.1.4 Consistency between translation units

Between different translation units, ensuring consistency is difficult. The overall idea is that for functions that are called from different TU, the contract is specified in a declaration in a header file, and that that specification is precise enough such that no ambiguity occurs.

In general, such consistency cannot be guaranteed without additional mechanisms and tools. Therefore our specification only forsees UB in case that during an execution evaluations of parameter types or contracts would lead to different results. For parameter types this UB was already present, though implicitly. For contracts this is a new UB, but which we think is unavoidable for current C.

It is possible to put mechanisms in place that would guarantee that contracts between different translation units are consistent. Our reference implementation (see below) for example does this by encoding all contracts into the name of the auxiliary function as hashs; thus only translation units with consistent contracts can be linked into one executable. But since there is no commonly agreed mechanism for this, we leave it to the quality of implementation for the moment.

4 Suggested text fragments, exact placement to be decided

4.1 Library: add a new header <stdc_contract.h>

Remark: It would also be possible to add these macros to <assert.h> (but without using the NDEBUG mechanism) or <stdlib.h> (because it already hosts unreachable).

1 Contracts enable macros (stdc_contract_terminate, stdc_contract_assume, stdc_contract_assert, inv, pre and post) and annotations for function declarations (_Inv, _Pre and _Post) that check specified predicates and that declare a number of internal states that can be used to ensure the consistency of an execution. The intent is to make such contracts visible simultaneously for the call side of a function and its implementation, and, to restrict the specified predicates such that evaluating them on either side (caller or callee) leads to the same result. Thereby contracts open the possibility to verify programs and to provide optimization opportunities, even if the program is composed of several translation units.

2 Here, a predicate is a logical condition specified as an expression of scalar type. When converted to bool a predicate is said to hold if the result is true and it is said to be violated if it is false. If a predicate that is evaluated as an argument to one of stdc_contract_assume, stdc_contract_assert, _Inv, _Pre or _Post is violated, an execution (of the program or of an individual thread) is henceforth erroneous and it is either terminated or the behavior is undefined. Additionally, if such a predicate is an integer constant expression, the value is determined at translation time and if it is violated a diagnostic is required.

3 For stdc_contract_assert, _Inv, _Pre and _Post, an optional program-defined configuration macro __STDC_CONTRACT_BEHAVIOR__ describes if a violated predicate terminates execution in a defined way or if such an execution continues with undefined behavior. If the predicate is violated, the same effects as an invocation of the macro stdc_contract_terminate take place; if the predicate holds execution continues.

4 The macros inv, pre and post are defined as if by the following

#ifndef inv
# define inv  _Inv
#endif
#ifndef pre
# define pre  _Pre
#endif
#ifndef post
# define post _Post
#endif

5 Recommended practice Application programs are encouraged to define __STDC_CONTRACT_BEHAVIOR__ only if this is unavoidable. For example, if the predicates that lead to a contract violation are not traceable by the translator, or in situations where terminating an execution in a controlled way is not possible.

4.1.1 The stdc_contract_terminate function and macro

Synopsis

[[noreturn]] void (stdc_contract_terminate)(char const* mess);
typedef void stdc_contract_termination_t(int);

2 The stdc_contract_terminate macro takes one argument, which is an ordinary string literal, called the message, that provides a diagnostic message.

Rationale: strings are always required to be ordinary string literals, here, to ensure that these strings are valid during all phases of termination of the execution and that no character set conversion has to be performed dynamically. In particular, dynamic allocations of diagnostic strings are to be avoided.

The behavior of an invocation of stdc_contract_terminate depends on the value of the configuration macro __STDC_CONTRACT_BEHAVIOR__ at the point of invocation. Three values are predefined as macros (6.10.10.2)

predefined macro value
__STDC_CONTRACT_BEHAVIOR_DEFAULT__ 0 default behavior
__STDC_CONTRACT_BEHAVIOR_UNREACHABLE__ 1 unreachable()
__STDC_CONTRACT_BEHAVIOR_TERMINATE__ 2 function call

3 If during translation at the position of an invocation of the stdc_contract_terminate macro the configuration macro __STDC_CONTRACT_BEHAVIOR__

default behavior of stdc_contract_terminate results if that position is reached during execution:

The latter happens as if by a call to a function that is compatible to stdc_contract_termination_t with the argument EXIT_FAILURE. It is implementation-defined if one of the function _Exit, quick_exit, exit or thrd_exit is called, or if it is a different implementation-defined function with type stdc_contract_termination_t.Ex) The implementation-defined choice is determined before or during translation phase 7.Link)

Ex) Note that the behavior of calling any of _Exit, quick_exit, and exit is undefined in the presence of multiple threads of execution.

Link) The behavior of a particular translation unit does not depend on linking.

4 If the execution reaches an invocation of the stdc_contract_terminate macro where during translation the macro __STDC_CONTRACT_BEHAVIOR__ expands to the token 1, the effect is as-if the unreachable macro is invoked.

5 If the execution reaches an invocation of the stdc_contract_terminate macro where during translation the configuration __STDC_CONTRACT_BEHAVIOR__ macro expands to the token 2, the function with external linkage and with the same name stdc_contract_terminate is called. The behavior of that function is as described for the default behavior only that the particular choice of the function with type stdc_contract_termination_t may be different; it is determined in translation phase 8 and is the same for all calls to the stdc_contract_terminate function of the same program execution. If the external function is called with an argument that does not refer to an immutable object with static life time that holds a sequence of printable characters which is terminated by a null character, the behavior is undefined.

6 Otherwise, there is an implementation-defined set (possibly empty) of decimal integer tokens (without suffix or digit separator) that provide implementation-defined behavior if the execution reaches an invocation of the stdc_contract_terminate macro where during translation the configuration macro __STDC_CONTRACT_BEHAVIOR__ expands to such a token. For each such implementation-defined token the implementation provides a macro with prefix __STDC_CONTRACT_BEHAVIOR_ (6.10.10.2) that expands to that token.

7 If the execution reaches an invocation of the stdc_contract_terminate macro where during translation the configuration __STDC_CONTRACT_BEHAVIOR__ macro expands to any other token sequence, the behavior is undefined.

8 Recommended practice It is recommended that the implementation-defined diagnostic message that is printed before termination also contains the values of __FILE__ and __LINE__ as of the point of invocation of the macro.

4.1.2 The stdc_contract_assert and stdc_contract_assume macros

1 Similar to a static_assert expression, these macros have the syntactic properties of a function call of type void where the first parameter has type bool and the second parameter has type char const*, only that the second argument is optional and, if present, is an ordinary string literal. The first argument to an invocation of these macros is called the predicate, the optional string argument, if any, the message. When converted to bool, a predicate is said to hold if the result is true and it is said to be violated if it is false.

2 If the predicate is an integer constant expression, an invocation is equivalent to a static_assert expression with the macro arguments as operands.

3 Otherwise, if the predicate is not an integer constant expression, the predicate is evaluated and converted to bool each time the execution meets the invocation. Then,

#define stdc_contract_assume(PREDICATE, ...)   \
((bool)(PREDICATE)                             \
    ? (void)0                                  \
    : unreachable())
#define stdc_contract_assert(PREDICATE, ...)   \
  ((bool)(PREDICATE)                           \
    ? (void)0                                  \
    : stdc_contract_terminate("" __VA_ARGS__))

footer) If the predicate does not hold, it follows that the diagnostic string that is printed contains the message argument, if any.

Thus, if the predicate holds the behavior for both macros is is the same; the only effects on the execution then are those of the evaluation of the predicate.FTN)

FTN) The translator may assume that the predicate holds for program code that is sequenced after such an invocation and optimize the program with that knowledge.

4 NOTE For both macros the predicate is evaluated unconditionally. This property is important to warrant a consistent execution of the program.

4.2 Language

4.2.1 in 6.2.1, Scopes of identifiers, type names, and compound literals

in p4

… If the declarator, abstract declarator or type specifier that declares the identifier appears within the list of parameter declarations in a function prototype (not part of a function definition), the identifier has function prototype scope, which terminates at the end of the direct declarator that contains the function declarator or the end of the direct abstract declarator that contains the function abstract declarator. …

4.2.2 in 6.3.3.3 Pointers

8 A pointer to a function of one type can be converted to a pointer to a function of another type and back again; the result shall compare equal to the original pointer. If a converted pointer is used to call a function whose type is not compatible with the referenced type or if a function without contracts is called with a type with contracts, the behavior is undefined.

4.2.3 in 6.4.2, Keywords

add _Inv, _Post and _Pre to the list of keywords.

4.2.4 in 6.5.17.2 Simple Assignment

Add items in p1 after the second position

— the left operand has atomic, qualified, or unqualified pointer to a function type without contracts, and (considering the type the left operand would have after lvalue conversion) both operands are pointers to compatible types;
— the left operand has atomic, qualified, or unqualified pointer to a function type with contracts, and (considering the type the left operand would have after lvalue conversion) and the right operand has the same type as the left operand;

and amend the now fifth item

— the left operand has atomic, qualified, or unqualified pointer type, and (considering the type the left operand would have after lvalue conversion) both operands are pointers to qualified or unqualified versions of compatible object types, and the type pointed to by the left operand has all the qualifiers of the type pointed to by the right operand;

4.2.5 Clause 6.7.7.4

4.2.5.1 Syntax

Apply the following changes.

Add contract-list to the syntax in 6.7.7.1

direct-declarator:

identifier attribute-specifier-sequenceopt

( declarator )

array-declarator attribute-specifier-sequenceopt

function-declarator attribute-specifier-sequenceopt contract-listopt

and in 6.7.8

direct-abstract-declarator:

( abstract-declarator )

array-abstract-declarator attribute-specifier-sequenceopt

function-abstract-declarator attribute-specifier-sequenceopt contract-listopt

4.2.5.2 In 6.7.7.4, Function declarators

15 Two function types without contract list are compatible if and only if all of the following hold:

In the determination of type compatibility and of a composite type, each parameter declared with function or array type is taken as having the adjusted type and each parameter declared with qualified type is taken as having the unqualified version of its declared type.

15′ Two function types F and E where F is without a contract list, E is with a contract list and E' is the type E without contract list, are compatible if F and E' are compatible. The composite type of such a pair is the type E.
15′′ Two function types F and E that are both with a contract list and that are declared in different translation units are compatible if they are compatible when the contract lists are omitted.Fuß)
Fuß) No two such function types appear in the same translation unit without violating a constraint (6.7.7.4.1).

4.2.6 Add a new subclause for contracts

6.7.7.4.1 Contracts

Syntax

1 contract-list:

contract

contract-list contract

contract:

precondition

postcondition

invariant

precondition:

_Pre attribute-specifier-sequenceopt ( selection-header )

postcondition:

_Post attribute-specifier-sequenceopt ( selection-header )

invariant:

_Inv attribute-specifier-sequenceopt ( expression )

Description

2 The expression of an invariant or the expression part of a selection header in a pre- or postcondition, if present, is called the predicate of the contract; if in a pre- or postcondition there is no such expression, the selection header is a simple declaration with an initializer and the predicate is that initializer. The optional attribute specifier sequence in a contract appertains to the declared contract.

3 Contracts serve to formulate requirements that are transferred from the calling context into the function context (preconditions) and others that are transferred back from the call into the calling context (postconditions). Invariants combine a pre- and a postcondition as described later in this subclause. Function declarations with a contract list are restricted such that the evaluation of all array length expressions of parameters and of all contracts in the context of the function call (with the declaration visible at the call site) or in the context of the function definition (with the declaration visible at the definition) lead to the same results.

4 In the selection header of each contract, zero, one or several objects with automatic storage duration, called ghost states, are defined and initialized. The names of ghost states have a scope of visibility similar to parameters that starts with the declaration and ends with the end of the function prototype scope or the block scope of the function body, respectively. In particular, they are visible to all following contracts in the list.

5 Additionally, if the return type of the function is not void, an additional ghost state is provided by the predefined identifier _ReturnValue that evaluates to a non-modifiable lvalue of the const-qualified return type that holds the return value of the function during all evaluations in a postcondition. It is visible in all pre- and postconditions, but only accessible in postconditions.Foot)

Foot) Thus _ReturnValue is even usable in preconditions for constructs such as typeof_unqual(_ReturnValue). It is recommended that implementations diagnose an access to the underlying lvalue in a precondition.

6 Within preconditions, names of parameters evaluate to the value and type as provided by the call, after it has been converted to the adjusted type of the corresponding parameter. For postconditions, it is unspecified if the result of the evaluation of a parameter is the value provided by the call or as possibly modified by the function body.FT)

FT) If a postcondition needs to access the unmodified value of a parameter as provided by the corresponding call, it is recommended to store that initial value in a ghost state of a precondition and then to access that ghost state in the postcondition.

Constraints

7 If a translation unit contains the definition of a function F and anywhere in the translation unit there is a declaration of F with contract list, that declaration shall be visible in the position of the definition of F; such a function is said with contracts.

Rationale: The definition must always implement the contracts for the case that it is called through a function pointer.

Rationale: It is difficult to specify conditions in different parts of a TU that would be guaranteed to evaluate to the same value, regardless of the circumstances.

8 Where the composite type of two function types is constructed, at most one of the types shall have a contract list.FTT)

FTT) This means in particular that if there are several declarations of a function (including a definition) or of a function pointer, at most one of them has a contract list.

9 In a declaration with contract list, the special token * that replaces an array length expression in the declaration of a parameter shall not be used. All identifiers used in a contract shall have visible declarations and, unless they are named constants, shall not refer to objects or functions with internal linkage. All ghost states shall have an initializer and a type that is neither an atomic type nor is volatile qualified. If the function declaration is also a definition, the name of a ghost state shall not be used inside the compound statement of the function body in any way.

Rationale: contracts are primarily thought as annotations of an interface between different translation units. Therefore they should not read the contents of static variables or call static functions. They must not have UB if a ghost state would be uninitialized in some situations.

10 A predicate shall have scalar type. A predicate that is an integer constant expression shall not have the value zero.

Rationale: predicates that are known to be always false should abort compilation with semantics similar to static_assert.

11 The address of a function with contracts shall not be passed as the second argument to a call to thrd_create.

Rationale: Calling such a function would evaluate the contracts in a different thread than the visible context of the call to thrd_create.

Semantics

12 On entry to a function with contracts, after the parameter values and their types have been determined, after evaluation of array length expressions of parameters and after array parameter adjustment, but before the compound statement of the function body is executed, all preconditions are evaluated and converted to bool. Similarly, after a return statement has been reached and a possible return expression has been evaluated or if the closing brace of the body has been reached, all postconditions are evaluated and converted to bool. All evaluations and conversions of preconditions are sequenced in the order in which they are specified and within the same thread as the function call; similarly, evaluations and conversions of postconditions are sequenced in declaration order.

13 An invariant of the form

_Inv [[ … attributes … ]] (Expr)

is equivalent to an in-place replacement by two contracts

_Pre [[ … attributes … ]] (auto AUXID = (Expr); AUXID)

_Post [[ … attributes … ]] ((Expr) == AUXID)

where AUXID is a unique auxiliary identifier that is not otherwise used in the translation unit.fu)

fu) Note that the predicate Expr in the contract does not have side effects.

14 For each contract, if the predicate holds during the evaluation the execution continues normally. If a predicate is violated, execution terminates as-if by an invocation of the macro stdc_contract_terminate with an ordinary string literal argument that contains at least the current expansion of the macros __FILE__ and __LINE__; for that invocation of stdc_contract_terminate the value of the __STDC_CONTRACT_BEHAVIOR__ configuration macro is determined at the place of the declaration of the contract.

15 For a function declaration with contract list, evaluations of array length expressions in parameters and evaluations in contracts shall not have side effects other than

They shall not access objects of functions of static storage duration unless these stem from a definition with external linkage, unless they are accessed through a pointer parameter, or unless they are string literals.

16 If a function without contract is called with a visible declaration that has a contract list, the behavior is undefined.

Rationale: This forbids the compilation of a function without contracts and then adding such contracts later to a header file. If that would be allowed, the function could eventually be called without the check for any of the predicates in place, and thus the semantics of the contracted interface would be violated.

If a function with contracts is called in a different translation unit than the definition through a type with contract list, the evaluation of array length expressions of parameter declarations in the context of the function call and of the function definition shall result in parameter types, before array parameter substitution, that are pairwise compatible. Both contexts shall either have a contract that is violated or both have no contract that is violated; in the case that both have a contract that is violated the macro __STDC_CONTRACT_BEHAVIOR__ shall have the same value, if any, for both contract declarations.

17 NOTE A function with contracts may always be called by using a declaration without contracts or by using its address, but such a call may be less efficient than a direct call.

18 EXAMPLE 1 Provided that the implementation has the type uintptr_t and that the ordering of that type is compatible with the conversion from unsigned char* the following presents contracts for a function my_memcpy that fulfills similar requirements as memcpy. Other than for memcpy, here, passing overlapping byte arrays as arguments terminates the program execution in a controlled way, no undefined behavior occurs in that case.

void *my_memcpy(void* dest, const void* src, size_t n)
    _Inv(dest) _Pre(src)
    _Pre(const unsigned char *const dest_start = dest,
                             *const src_start  = src;
        ((uintptr_t)(src_start + n)  <= (uintptr_t)dest_start)
     || ((uintptr_t)(dest_start + n) <= (uintptr_t)src_start))
    _Post(_ReturnValue == dest);

The first two contracts make the general guarantees for functions in the library clause that all parameters have valid values. Additionally, the invariant ensures that the function does not change dest; such an invariant is stronger than decorating the dest pointer with a const qualification, since such a qualification is subject to adjustment. The precondition with ghost states tests that both byte arrays of length n that are passed as arguments do not overlap; note that the requirements here could also be expressed by adding restrict qualifications, but note also that doing so would not enforce them. Last, the postcondition assures that the function returns the same value as dest.

Information for the range check will in general be present at the point of a call; thus if a translator is able to prove that requirement the check for it can be omitted. For the postcondition, dest is used because the invariant guarantees that that value is not changed by the function. Alternatively, also the ghost state dest_start can be used, because it also holds the original value that was passed to dest. In general, the implementation will be able to make this guarantee when translating the definition of the function, so then the check for this postcondition is superfluous. On the other hand, a translator where only the declaration is visible is able to deduce that property from the postcondition and optimize accordingly in the context of the call.

19 EXAMPLE 2 If a functions with contract is defined as inline, the contracts are best placed at the inline definition.

// header "range.h"
#include <stdint.h>
inline
bool range_check(void const*const a, void const*const b, size_t n)
_Pre(a) _Pre(b) _Pre(n)
{
     const unsigned char *const dest_start = a,
     const unsigned char *const src_start  = b;
     return
        ((uintptr_t)(src_start + n)  <= (uintptr_t)dest_start)
        || ((uintptr_t)(dest_start + n) <= (uintptr_t)src_start);
}

The declaration of the previous example may then be rewritten to use a call to that function as a predicate.

#include "range.h"
void *my_memcpy(void* dest, const void* src, size_t n)
    _Inv(dest)
    _Pre(range_check(dest, src, n))
    _Post(_ReturnValue == dest);

Here the same contracts as before are checked recursively in the call to range_check. Note that implicitly this specifies a contract _Pre(dest) twice, once from the invariant and once for the call to range_check, but since both are visible at the call side of a call to my_memcpy evaluating the first of the two is sufficient. In the translation unit that provides the external definition of range_check, there is no need to specify the contracts, again:

#include "range.h"

// makes the definition external
// the composite type has the contracts
extern typeof(range_check) range_check;

20 EXAMPLE 3 If the addresses of a set of functions with contracts are to be used interchangeably, it is recommended to use a type definition for the declarations that add the contracts.

// header file "alloc.h"
typedef void* alloc_t(size_t n) _Pre(n) _Post(_ReturnValue);
extern alloc_t  alloc_uninit;
extern alloc_t  alloc_init;
extern alloc_t* alloc_today;

This ensures that both function pointers &alloc_init and &alloc_uninit are candidates for assignment to alloc_today; since the types are the same (and not only compatible) no type compatibility problems arise between different function pointers.

In the translation unit that implements the functions, definitions without contract list are used:

// implementation
#include <stdlib.h>
#include "alloc.h"

alloc_t* alloc_today =
#if USE_ALLOC‿UNINIT
    alloc_uninit
#else
    alloc_init
#endif
;

// the composite type has the contracts
void* alloc_uninit(size_t n) {
    void* ret = malloc(n);
    stdc_contract_assert(ret, "out of memory in allocation");
    return ret;
}

// the composite type has the contracts
void* alloc_init(size_t n) {
    void* ret = calloc(n, 1);
    stdc_contract_assert(ret, "out of memory in allocation");
    return ret;
}

Here, the composite type of a type with contract list (from the header) is formed with a type that has no contract list.

4.2.7 Clause 6.10.10.2 Mandatory macros

Add to the item list where appropriate:

5 Discussion of the semantics expressed in equivalent C code

As defined in the suggested text above, it may seem as if contracts impose severe constraints to all executions, as they assume that all contracts are checked on all function calls. Because of the strong impact that such a behavior would then have for example on execution times, as such this would probably not be a viable proposal.

In fact, modern compilers and static analyzers should be able to prove for many contracts that they hold unconditionally; thus they are dead code and can be removed. One of the keys to that is that all evaluations in contracts are forced to be free of side effects and can in general be hoisted out of the immediate calling context. The other key is the requirement that contracts for the same function, even if specified in different translation units, have to behave the same when presented with the same arguments.

In the following a selection-header of a precondition is given in the form

dec_preᵢ predicate_preᵢ

where the part

type_preᵢ ghost_pre⁰ᵢ = init_pre⁰ᵢ, ...;

The same syntax as for if-statements is admissible, that is either dec_preᵢ or predicate_preᵢ can be empty, but not both. Both, dec_preᵢ and predicate_preᵢ, are the usual C constructs as they may appear in if-statements.

If predicate_preᵢ is empty, then (per definition of the if statement) dec_preᵢ is a simple declaration defining exactly one ghost state ghost_pre⁰ᵢ with initializer init_pre⁰ᵢ. predicate_preᵢ is then assumed to be the expression init_pre⁰ᵢ.

Analogous definitions hold for postconditions in the form dec_postᵢ predicate_postᵢ.

In the following we discuss three different views of a function with contracts,

5.1 Semantics of an inline definition

If a function with contracts is given as an inline definition, the semantics are relatively simple and easily explained in existing C syntax: tests for the preconditions have to be inserted before the rest of the function body and tests for post conditions afterwards. There is only one subtlety, namely the handling of return statements. In fact, all return statements are replaced by assignments to the auxiliary variable _ReturnValue and then a proper return statement is added at the end, after all postconditions have been checked.

Suppose a list of contracts is attached to a function definition with inline:

// header
inline returnType func(parameterTypeList)
  pre(dec_pre₀ predicate_pre₀)
  pre(dec_pre₁ predicate_pre₁)
  …
  pre(dec_preₙ predicate_preₙ)
  post(dec_post₀ predicate_post₀)
  post(dec_post₁ predicate_post₁)
  …
  post(dec_postₘ predicate_postₘ)
function-body
// translation unit
typeof(func) func; // instantiation of func

The effect is as-if the function was augmented with cascaded if statements that test for the conditions.

// header
inline returnType func(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        stdc_contract_terminate("some string");
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        stdc_contract_terminate("some string");
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        stdc_contract_terminate("some string");
    } else {

        replaced-function-body      // replace return by assignment

        if (dec_post₀ !predicate_post₀) {
            static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
            stdc_contract_terminate("some string");
        } else if (dec_post₁ !predicate_post₁) {
            static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
            stdc_contract_terminate("some string");
        } else if (…) {
            ...
        } else if (dec_postₘ !predicate_postₘ) {
            static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
            stdc_contract_terminate("some string");
        } else {
            return _ReturnValue;
        }
    }
    stdc_contract_terminate("severe bug, execution must never reach here");
}

Here, replaced-function-body is the function-body where all returnexpression statements are replaced by assignments _ReturnValue =expression and the macro ICE_OR_TRUE is supposed to resolve to its argument if that is an ICE and to true, otherwise.

Note that the if-statements with the inverted condition are such that all definitions of ghost states in the form dec_preᵢ or dec_postᵢ are visible to all evaluations in the subsequent contracts.

The derived inline function definition has the following properties.

In the calling context some information may be present which ensures that the preconditions are always satisfied. Then, these can effectively be optimized out at compile time without changing the semantics. Similarly, the knowledge about postconditions can be integrated into the calling context.

5.2 Semantics of an external declaration

If a function is split into an external declaration in a header and a definition in one TU, things get a bit more complicated. Here, we define an auxiliary inline definition that tests for contracts as above and calls a different internal function to access the original definition. The subtlety here is that we only want preconditions to be evaluated in the calling context as assertions, but postconditions should only appear as assumptions.

Suppose a list of contracts is attached to a function declaration without inline:

// header
returnType func(parameterTypeList)
  pre(dec_pre₀ predicate_pre₀)
  pre(dec_pre₁ predicate_pre₁)
  …
  pre(dec_preₙ predicate_preₙ)
  post(dec_post₀ predicate_post₀)
  post(dec_post₁ predicate_post₁)
  …
  post(dec_postₘ predicate_postₘ);
// translation unit
returnType func(parameterTypeList) function-body

The effect is as-if the following function were defined in the header.

// header
inline returnType func(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        stdc_contract_terminate("some string");
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        stdc_contract_terminate("some string");
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        stdc_contract_terminate("some string");
    } else {

        typeof(func) func_aux;
        _ReturnValue = func_aux(parameters, …);

        if (dec_post₀ !predicate_post₀) {
            static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
            unreachable();
        } else if (dec_post₁ !predicate_post₁) {
            static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
            unreachable();
        } else if (…) {
            ...
        } else if (dec_postₘ !predicate_postₘ) {
            static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
            unreachable();
        } else {
            return _ReturnValue;
        }
    }
    stdc_contract_terminate("severe bug, execution must never reach here");
}

The function func_aux will be shown in the next section. The name func_aux is only chosen for the example, a real implementation chooses a unique name that is not predictable for the user.

The auxiliary inline function definition has the following properties.

Note that again preconditions that are known to hold in the calling context can effectively be optimized out at compile time without changing the semantics. Similarly, postconditions can provide valuable information for the calling context. For these optimization opportunities it is essential that contracts do not have side effects.

5.3 Semantics of the function implementation

The translation unit then provides two function symbols: the auxiliary function func_aux that is called by func as given above, and the instantiation of func itself. As mentionned, the name func_aux is only for the example; it is a unique name that is not predictable for the user.

// translation unit
returnType func_aux(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        unreachable();
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        unreachable();
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        unreachable();
    } else {

        replaced-function-body      // replace return by assignment

        if (dec_post₀ !predicate_post₀) {
            static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
            stdc_contract_terminate("some string");
        } else if (dec_post₁ !predicate_post₁) {
            static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
            stdc_contract_terminate("some string");
        } else if (…) {
            ...
        } else if (dec_postₘ !predicate_postₘ) {
            static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
            stdc_contract_terminate("some string");
        }
    }
    stdc_contract_terminate("severe bug, execution must never reach here");
}

typeof(func) func; // instantiation of func

The only function that is called by user code is func, either as the inline definition in the header file or via the external symbol; both types of calls have the same semantics.

In particular, func_aux, will never be called directly by user code. It

A non-optimized version of the instantiation of func would evaluate each predicate twice, once from the inline body of func and once from the body of funx_aux. Indeed, each predicate is first checked as an assertion (possibly calling stdc_contract_terminate()) and then as an assumption (running into unreachable()), so because the predicate cannot have side effects and has to evaluate the same in both contexts.

6 Implementation experience

It seems that in the advent of C++26, all major C++ compilers have implementations of C++ contracts with some of the semantics models mentioned above.

In C, there is now wide support for some form of “assume” feature, either as builtins (clang, MSV) or as an attribute (gcc). Together with C23’s unreachable, in C this helps to implement the semantics with shallow inline wrappers as described previously.

If there is no additional help from the compiler, the need to implement two consistent wrappers (the inline version of func and func_aux above) makes the approach a bit tedious and not very practical. Nevertheless, this already provides a way to test the semantics and to see how modern compilers are able to detect redundancies in chained contracts.

Our eĿlipsis preprocessor provides include files <ellipsis-contracts.h>, <ellipsis-interface.h> and <ellipsis-implementation.h> that uses a syntax that is relatively close to the proposed syntax for declarations with contracts, and uses them to implement the following features:

The features stdc_contract_assert, _Pre, _Post and _Inv use static strings for the diagnostics that are forcibly embedded in the executable. These can be used to evaluate which of the contracts actually survived optimization. Thereby a detailed assessment of the particular optimization capabilities can be made. A small script is provided to facilitate such an analysis.

eĿlipsis’ sources also uses contracts as described themselves. This provides a lot of test cases for the abilities of modern compilers. Evaluations with gcc and clang show interesting level of optimization, as long as not too much aliasing analysis needed for the contracts.

Acknowledgments

Thanks to Martin Uecker, David Tarditi, Joseph Myers, and Ville Voutilainen for review and discussions.