[dcl.contract] (original) (raw)

9 Declarations [dcl]

9.4 Function contract specifiers [dcl.contract]

9.4.1 General [dcl.contract.func]

A precondition-specifierintroduces a precondition assertion, which is a function contract assertion associated with entering a function.

A postcondition-specifierintroduces a postcondition assertion, which is a function contract assertion associated with exiting a function normally.

[Note 1:

A postcondition assertion is not associated with exiting a function in any other fashion, such as via an exception ([expr.throw]) or via a call to longjmp ([csetjmp.syn]).

— _end note_]

Each function-contract-specifierof a function-contract-specifier-seq (if any) of an unspecified first declaration ([basic.def]) of a function introduces a corresponding function contract assertion for that function.

The optional attribute-specifier-seqfollowing pre or postappertains to the introduced contract assertion.

A declaration Dof a function or function template _f_that is not a first declaration shall have either no function-contract-specifier-seqor the same function-contract-specifier-seq (see below) as any first declaration F reachable from D.

If D and F are in different translation units, a diagnostic is required only if D is attached to a named module.

If a declaration is a first declaration of fin one translation unit and a declaration is a first declaration of f in another translation unit, and shall specify the samefunction-contract-specifier-seq, no diagnostic required.

A function-contract-specifier-seq is the same as a function-contract-specifier-seq if and consist of the same function-contract-specifier_s_in the same order.

A function-contract-specifier on a function declaration is the same as a function-contract-specifier on a function declaration if

• their predicates and would satisfy the one-definition rule ([basic.def.odr]) if placed in function definitions on the declarations and , respectively, except for
  • renaming of the parameters of f,
  • renaming of template parameters of a template enclosing , and
  • renaming of the result binding ([dcl.contract.res]), if any,
    and, if and are in different translation units, corresponding entities defined within each predicate behave as if there is a single entity with a single definition, and
• both and specify a result-name-introduceror neither do.

If this condition is not met solely due to the comparison of two lambda-expression_s_that are contained within and , no diagnostic is required.

[Note 3:

Equivalentfunction-contract-specifier-seq_s_apply to all uses and definitions of a function across all translation units.

— _end note_]

[Example 1: bool b1, b2;void f() pre (b1) pre ([]{ return b2; }());void f(); void f() pre (b1) pre ([]{ return b2; }()); void f() pre (b1); int g() post(r : b1);int g() post(b1); namespace N { void h() pre (b1);bool b1;void h() pre (b1); } — _end example_]

If the predicate of a postcondition assertion of a function _f_odr-uses ([basic.def.odr]) a non-reference parameter of f, that parameter and the corresponding parameter on all declarations of _f_shall have const type.

[Note 4:

This requirement applies even to declarations that do not specify the postcondition-specifier.

Parameters with array or function type will decay to non-const types even if a const qualifier is present.

[Example 2: int f(const int i[10]) post(r : r == i[0]); — _end example_]

— _end note_]

[Note 5:

The function contract assertions of a function are evaluated even when invoked indirectly, such as through a pointer to function or a pointer to member function.

A pointer to function, pointer to member function, or function type alias cannot have a function-contract-specifier-seqassociated directly with it.

— _end note_]

The function contract assertions of a function are considered to be needed ([temp.inst]) when

• the function is odr-used ([basic.def.odr]) or
• the function is defined.

[Note 6:

[Example 3: template <typename T> void f(T t) pre( t == "" );template <typename T> void f(T&& t);void g() { f(5); } — _end example_]

— _end note_]

9.4.2 Referring to the result object [dcl.contract.res]

The result-name-introducerof a postcondition-specifieris a declaration.

The result-name-introducerintroduces the identifieras the name of a result bindingof the associated function.

If a postcondition assertion has a result-name-introducerand the return type of the function is cv void, the program is ill-formed.

A result binding denotes the object or reference returned by invocation of that function.

The type of a result binding is the return type of its associated function The optional attribute-specifier-seqof the attributed-identifierin the result-name-introducerappertains to the result binding so introduced.

[Example 1: int f() post(r : r == 1) { return 1;} int i = f(); — _end example_]

[Example 2: struct A {};struct B { B() {} B(const B&) {} };template <typename T>T f(T* const ptr) post(r: &r == ptr) { return {};} int main() { A a = f(&a); B b = f(&b); } — _end example_]

When the declared return type of a non-templated function contains a placeholder type, a postcondition-specifierwith a result-name-introducershall be present only on a definition.

[Example 3: auto g(auto&) post (r: r >= 0); auto h() post (r: r >= 0); auto k() post (r: r >= 0) { return 0;} — _end example_]