9 Declarations [dcl]

9.4 Function contract specifiers [dcl.contract]

9.4.1 General [dcl.contract.func]

1
#
A function contract assertion is a contract assertion ([basic.contract.general]) associated with a function.
A precondition-specifier introduces a precondition assertion, which is a function contract assertion associated with entering a function.
A postcondition-specifier introduces 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]
2
#
The predicate ([basic.contract.general]) of a function contract assertion is its conditional-expression contextually converted to bool.
3
#
Each function-contract-specifier of 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-seq following pre or post appertains to the introduced contract assertion.
[Note 2: 
The function-contract-specifier-seq of a lambda-declarator applies to the function call operator or operator template of the corresponding closure type ([expr.prim.lambda.closure]).
— end note]
4
#
A declaration D of a function or function template f that is not a first declaration shall have either no function-contract-specifier-seq or 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 f in one translation unit and a declaration is a first declaration of f in another translation unit, and shall specify the same function-contract-specifier-seq, no diagnostic required.
5
#
A function-contract-specifier-seq is the same as a function-contract-specifier-seq if and consist of the same function-contract-specifiers 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
  • (5.1)
    their predicates and would satisfy the one-definition rule ([basic.def.odr]) if placed in function definitions on the declarations and , respectively, except for 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
  • (5.2)
    both and specify a result-name-introducer or neither do.
If this condition is not met solely due to the comparison of two lambda-expressions that are contained within and , no diagnostic is required.
[Note 3: 
Equivalent function-contract-specifier-seqs 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(); // OK, function-contract-specifiers omitted void f() pre (b1) pre ([]{ return b2; }()); // error: closures have different types. void f() pre (b1); // error: function-contract-specifiers only partially repeated int g() post(r : b1); int g() post(b1); // error: mismatched result-name-introducer presence namespace N { void h() pre (b1); bool b1; void h() pre (b1); // error: function-contract-specifiers differ according to // the one-definition rule ([basic.def.odr]). } — end example]
6
#
A virtual function ([class.virtual]), a deleted function ([dcl.fct.def.delete]), or a function defaulted on its first declaration ([dcl.fct.def.default]) shall not have a function-contract-specifier-seq.
7
#
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]); // error: i has type const int * (not int* const). — end example]
— end note]
8
#
[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-seq associated directly with it.
— end note]
9
#
The function contract assertions of a function are considered to be needed ([temp.inst]) when
[Note 6: 
Overload resolution does not consider function-contract-specifiers ([temp.deduct], [temp.inst]).
[Example 3: template <typename T> void f(T t) pre( t == "" ); template <typename T> void f(T&& t); void g() { f(5); // error: ambiguous } — end example]
— end note]

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

1
#
The result-name-introducer introduces the identifier as the name of a result binding of the associated function.
If a postcondition assertion has a result-name-introducer and 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-seq of the attributed-identifier in the result-name-introducer appertains to the result binding so introduced.
[Note 1: 
An id-expression that names a result binding is a const lvalue ([expr.prim.id.unqual]).
— end note]
[Example 1: int f() post(r : r == 1) { return 1; } int i = f(); // Postcondition check succeeds. — 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); // The postcondition check can fail if the implementation introduces // a temporary for the return value ([class.temporary]). B b = f(&b); // The postcondition check succeeds, no temporary is introduced. } — end example]
2
#
When the declared return type of a non-templated function contains a placeholder type, a postcondition-specifier with a result-name-introducer shall be present only on a definition.
[Example 3: auto g(auto&) post (r: r >= 0); // OK, g is a template. auto h() post (r: r >= 0); // error: cannot name the return value auto k() post (r: r >= 0) // OK { return 0; } — end example]