9 Declarations [dcl.dcl]

9.11 Attributes [dcl.attr]

9.11.4 Contract attributes [dcl.attr.contract]

9.11.4.2 Contract conditions [dcl.attr.contract.cond]

1
#
A contract condition is a precondition or a postcondition.
The first declaration of a function shall specify all contract conditions (if any) of the function.
Subsequent declarations shall either specify no contract conditions or the same list of contract conditions; no diagnostic is required if corresponding conditions will always evaluate to the same value.
The list of contract conditions of a function shall be the same if the declarations of that function appear in different translation units; no diagnostic required.
If a friend declaration is the first declaration of the function in a translation unit and has a contract condition, the declaration shall be a definition and shall be the only declaration of the function in the translation unit.
2
#
Two lists of contract conditions are the same if they consist of the same contract conditions in the same order.
Two contract conditions are the same if their contract levels are the same and their predicates are the same.
Two predicates contained in contract-attribute-specifiers are the same if they would satisfy the one-definition rule ([basic.def.odr]) were they to appear in function definitions, except for renaming of parameters, return value identifiers (if any), and template parameters.
3
#
[ Note
:
A function pointer cannot include contract conditions.
[ Example
: 
typedef int (*fpt)() [[ensures r: r != 0]];     // error: contract condition not on a function declaration

int g(int x)
  [[expects: x >= 0]]
  [[ensures r: r > x]]
{
  return x+1;
}

int (*pf)(int) = g;                             // OK
int x = pf(5);                                  // contract conditions of g are checked
— end example
 ]
— end note
 ]
4
#
The predicate of a contract condition has the same semantic restrictions as if it appeared as the first expression-statement in the body of the function it applies to.
Additional access restrictions apply to names appearing in a contract condition of a member function of class C:
  • (4.1)
    Friendship is not considered ([class.friend]).
  • (4.2)
    For a contract condition of a public member function, no member of C or of an enclosing class of C is accessible unless it is a public member of C, or a member of a base class accessible as a public member of C ([class.access.base]).
  • (4.3)
    For a contract condition of a protected member function, no member of C or of an enclosing class of C is accessible unless it is a public or protected member of C, or a member of a base class accessible as a public or protected member of C.
For names appearing in a contract condition of a non-member function, friendship is not considered.
[ Example
: 
class X {
public:
  int v() const;
  void f() [[expects: x > 0]];                  // error: x is private
  void g() [[expects: v() > 0]];                // OK
  friend void r(int z) [[expects: z > 0]];      // OK
  friend void s(int z) [[expects: z > x]];      // error: x is private
protected:
  int w();
  void h() [[expects: x > 0]];                  // error: x is private
  void i() [[ensures: y > 0]];                  // OK
  void j() [[ensures: w() > 0]];                // OK
  int y;
private:
  void k() [[expects: x > 0]];                  // OK
  int x;
};

class Y : public X {
public:
  void a() [[expects: v() > 0]];                // OK
  void b() [[ensures: w() > 0]];                // error: w is protected
protected:
  void c() [[expects: w() > 0]];                // OK
};
— end example
 ]
5
#
A precondition is checked by evaluating its predicate immediately before starting evaluation of the function body.
[ Note
:
The function body includes the function-try-block and the ctor-initializer.
— end note
 ]
A postcondition is checked by evaluating its predicate immediately before returning control to the caller of the function.
[ Note
:
The lifetime of local variables and temporaries has ended.
Exiting via an exception or via longjmp ([csetjmp.syn]) is not considered returning control to the caller of the function.
— end note
 ]
6
#
If a function has multiple preconditions, their evaluation (if any) will be performed in the order they appear lexically.
If a function has multiple postconditions, their evaluation (if any) will be performed in the order they appear lexically.
[ Example
: 
void f(int * p)
  [[expects: p != nullptr]]                     // #1
  [[ensures: *p == 1]]                          // #3
  [[expects: *p == 0]]                          // #2
{
  *p = 1;
}
— end example
 ]
7
#
If a postcondition odr-uses ([basic.def.odr]) a parameter in its predicate and the function body makes direct or indirect modifications of the value of that parameter, the behavior is undefined.
[ Example
: 
int f(int x)
  [[ensures r: r == x]]
{
  return ++x;                   // undefined behavior
}

int g(int * p)
  [[ensures r: p != nullptr]]
{
  *p = 42;                      // OK, p is not modified
}

int h(int x)
  [[ensures r: r == x]]
{
  potentially_modify(x);        // undefined behavior if x is modified
  return x;
}
— end example
 ]