contract-attribute-specifier: [ [ expects contract-level : conditional-expression ] ] [ [ ensures contract-level identifier : conditional-expression ] ] [ [ assert contract-level : conditional-expression ] ]
contract-level: default audit axiom
int f(char * c) [[ensures res: res > 0 && c != nullptr]]; int g(double * p) [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];— end example
void push(int x, queue & q)
[[expects: !q.full()]]
[[ensures: !q.empty()]]
{
/* ... */
[[assert: q.is_valid()]];
/* ... */
}
int min = -42;
constexpr int max = 42;
constexpr int g(int x)
[[expects: min <= x]] // error
[[expects: x < max]] // OK
{
/* ... */
[[assert: 2*x < max]];
[[assert: ++min > 0]]; // undefined behavior
/* ... */
} — end exampletypedef 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
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 examplevoid f(int * p) [[expects: p != nullptr]] // #1 [[ensures: *p == 1]] // #3 [[expects: *p == 0]] // #2 { *p = 1; }— end 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
int z;
bool is_prime(int k);
void f(int x)
[[expects: x > 0]]
[[expects audit: is_prime(x)]]
[[ensures: z > 10]]
{
/* ... */
} — end example
void f(int x) noexcept [[expects: x > 0]];
void g() {
f(0); // std::terminate() if violation handler throws
/* ... */
} — end example
void f(int x) [[expects: x > 0]];
void g() {
f(0); // std::terminate() after handler if continuation mode is off;
// proceeds after handler if continuation mode is on
/* ... */
} — end example