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]).
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 F1 is a
first declaration of f
in one translation unit and
a declaration F2 is a
first declaration of f in another translation unit,
F1 and F2 shall specify the same
function-contract-specifier-seq, no diagnostic required.
their predicates P1 and P2 would
satisfy the one-definition rule ([basic.def.odr])
if placed in function definitions on
the declarations D1 and D2, respectively, except for
and,
if D1 and D2 are in different translation units,
corresponding entities defined within each predicate
behave as if there is a single entity with a single definition, and
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.
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.
[Example 1: int f()
post(r : r ==1){return1;
}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]
[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 valueauto k()
post (r: r >=0)/ OK{return0;
} — end example]