Annotations

You write the specification of a function, a loop or a program point as an annotation in your C or C++ source. This page describes the annotations that exist today, where each may be written, and what each means.

cerastes verify (Verifying a program) checks requires, ensures, invariant, decreases and check in functions over integers and bool. The other parts of this page are parsed, type-checked and placed on the function or statement they belong to, and the mistakes listed under Where annotations are not allowed are rejected, but nothing checks what they mean yet. cerastes verify does not accept them in a program it verifies: a fold or unfold statement is rejected (cerastes-unsupported_statement), and so is any call in an annotation other than cerastes::old (cerastes-call_in_annotation), which includes the predicates, pure functions and specification functions that this page describes. Their declarations are accepted. The rest of this page states what they will mean, so that you can write them now.

Everything on this page is a test. Each example is compiled by cerastes’s front end, and the listing it produces is compared with a stored copy. The examples marked as accepted by ordinary compilers are also built with Apple clang and GCC, as described in Building annotated code with ordinary compilers.

Writing annotations

There are nine annotations. You write them with macros from <cerastes.h>:

Macro Written Meaning

CERASTES_REQUIRES(p)

after a function’s parameter list

precondition: p holds when the function is called

CERASTES_ENSURES(p) or CERASTES_ENSURES(r, p)

after a function’s parameter list

postcondition: p holds when the function returns; r names the result

CERASTES_INVARIANT(p)

before a while, do, for or range-based for statement

p holds every time control reaches the loop test (for do, at the start of every iteration)

CERASTES_DECREASES(e1, …​)

before a while, do or for statement, or after a function’s parameter list

termination measure: it gets smaller with every iteration of the loop, or every recursive call of the function

CERASTES_CHECK(p)

as a statement

p holds at this point

CERASTES_FOLD(e), CERASTES_UNFOLD(e)

as a statement

exchange a predicate for its meaning, and back

CERASTES_PREDICATE, CERASTES_PURE

first in a function declaration

the function is specification, not program

Include the header once, with #include <cerastes.h>. The first example below shows a function with a precondition and a postcondition. The condition p is an ordinary C++ expression. In CERASTES_ENSURES(r, p) the name r is the function’s result.

#include <cerastes.h>

int abs_val(int x) CERASTES_REQUIRES(x > -1000000) CERASTES_ENSURES(r, r >= 0 && (r == x || r == -x))
{
  return x < 0 ? -x : x;
}

Each macro expands to a standard attribute in the namespace cerastes, for example [[cerastes::requires(x >= 0)]], when cerastes reads the file. The cerastes front end defines the macro __CERASTES__ itself, so you do not, and an #undef or a redefinition of it, on the command line or in the source, is an error (cerastes-cerastes_macro_changed). For any other compiler the contract macros expand to nothing, so the same file builds as before (see Building annotated code with ordinary compilers). You may write the attribute by hand, guarded in the same way:

#ifdef __CERASTES__
int twice(int x) [[cerastes::requires(x >= 0)]] [[cerastes::ensures(r, r == x + x)]];
#else
int twice(int x);
#endif

The namespace is closed. A name that cerastes does not define, such as [[cerastes::assert(x > 0)]], is an error, and there is deliberately no assume. The statement annotation is check, not assert, because <cassert> expands assert as a macro. (That macro is verified too: an assert(e) is checked like a check, but it is code, evaluated at run time; see Verifying a program.)

Contracts: requires and ensures

A contract is a list of requires and ensures annotations on a function, member function, constructor or destructor. They are written after the parameter list, and after any const, & or noexcept that follows it. They may not be written on a variable, a class, a typedef, a lambda or a function pointer.

requires

requires(p) is a precondition. The expression is not evaluated; it is type-checked, and it must convert to bool. It sees the function’s parameters, this and the members declared before it in a member function, and the names visible at the declaration. Of the variables outside the function, cerastes verify accepts only constants (named constants); the same holds for ensures, invariant, decreases and check.

int half(int x) CERASTES_REQUIRES(x >= 0);

Several annotations on one declaration are all part of the contract, as a conjunction, in the order written:

int clamp_pos(int x, int hi) CERASTES_REQUIRES(hi > 0) CERASTES_REQUIRES(x >= 0)
{
  return x < hi ? x : hi;
}

ensures

ensures(p) is a postcondition. ensures(r, p) also names the function’s result r, with the declared return type, for use in p:

int next(int x) CERASTES_ENSURES(x < 1000)
{
  x = x + 1;
  return x;
}
int abs_val(int x) CERASTES_ENSURES(r, r >= 0 && (r == x || r == -x))
{
  return x < 0 ? -x : x;
}

The first argument is a result name exactly when it is a lone identifier followed by a comma. A result name is an error when:

  • it is the name of a parameter;

  • the function returns void, or is a constructor or a destructor;

  • the return type is deduced (auto, decltype(auto)) or written as a trailing return type. This is a limit of the present version.

ensures(p) without a result name is always allowed, including for those functions.

What a parameter means in ensures

In ensures, a parameter named x means the value that was passed in. A function may assign to its by-value parameters, but the postcondition still talks about the argument:

int bump(int x) CERASTES_ENSURES(r, r == x + 1)
{
  x = x + 1; // the contract still talks about the argument that was passed
  return x;
}

State that the function can change and that its caller can see is different: the object behind a pointer or a reference, a field, a global. cerastes::old(e) is the value of e when the function was entered. A reference parameter x always denotes the same object, so in ensures, x is that object’s value when the function returns and cerastes::old(x) is its value on entry. A pointer works the same way through *p:

void incr(int& x) CERASTES_REQUIRES(x < 1000) CERASTES_ENSURES(x == cerastes::old(x) + 1)
{
  x += 1;
}
void incr_ptr(int* p) CERASTES_REQUIRES(*p < 1000) CERASTES_ENSURES(*p == cerastes::old(*p) + 1)
{
  *p += 1;
}

Writing old(x) for a by-value parameter x is allowed and means x. old is meaningful only in ensures; using it anywhere else is an error.

Declarations that repeat a contract

A function often has several declarations: one in a header, a definition, a member declared in its class and defined outside it, a template declared and then defined. The contract is written on one of them, and every declaration that carries a contract must carry the same one: the same annotations, in the same order, with equivalent arguments. Parameters are compared by position, so you may rename them. A declaration without a contract has the function’s contract.

int bump(int x) CERASTES_REQUIRES(x > 0 && x < 100) CERASTES_ENSURES(r, r > x);
int bump(int y);
int bump(int z) CERASTES_REQUIRES(z > 0 && z < 100) CERASTES_ENSURES(r, r > z)
{
  return z + 1;
}

The usual style is to write the contract once, on the declaration in the header:

int halve(int x) CERASTES_REQUIRES(x >= 0) CERASTES_ENSURES(r, r <= x);

int halve(int x)
{
  return x / 2;
}

A different contract on a later declaration is an error at that declaration. There is no way to add to a contract later, on purpose. cerastes checks each translation unit by itself, so a definition that could add a precondition to its header’s would be checked against more than the callers in other translation units were promised.

Two limits follow from how declarations are compared. cerastes compares the expressions of the two contracts as the front end does, so two contracts that mean the same thing can still be reported as different:

  • this→a > x on one declaration and a > y on another;

  • any contract that contains a lambda, because two lambdas are never the same one. That includes every forall.

Write such a contract once, on one declaration, and leave the others without one:

bool all_nonneg(const int* a, int n)
  CERASTES_REQUIRES(n >= 0 && cerastes::forall([](int i, const int* a, int n) { return !(0 <= i && i < n) || a[i] >= 0; }, a, n));

bool all_nonneg(const int* a, int n)
{
  for (int i = 0; i < n; ++i) {
    if (a[i] < 0) {
      return false;
    }
  }
  return true;
}

An explicit specialization of a function template follows the same rule with respect to the primary template. It may repeat the primary template’s contract, or carry none, in which case it has the primary’s. It may not have a different one, whichever of the two is declared first. Callers rely on the primary template’s contract, but a call with those arguments runs the specialization.

template <class T> T twice(T v) CERASTES_REQUIRES(v >= 0) CERASTES_ENSURES(r, r >= v);

template <> int twice<int>(int v) CERASTES_REQUIRES(v >= 0) CERASTES_ENSURES(r, r >= v)
{
  return v + v;
}

template <> long twice<long>(long v)
{
  return v + v;
}

An explicit specialization of a member template of a class template is refused when the primary member template has a contract, on any of its declarations, and whether or not the specialization repeats the contract: attr_member_template_specialization.

#include <cerastes.h>

template <class U>
struct box {
  template <class T> T twice(T v) CERASTES_REQUIRES(v >= 0);
};

template <class U>
template <class T>
T box<U>::twice(T v)
{
  return v + v;
}

template <> template <>
int box<int>::twice<int>(int v) // <- error
{
  return v + v;
}

The same specialization written inside the class template (template <> int f<int>(int) in the class body, allowed since CWG 727) is not checked by the front end at all when the class template is never instantiated, so cerastes refuses it itself, whenever it, or the member template of the same name, has a contract: cerastes-in_class_specialization_contract. It is reported at the specialization. Write the specialization at namespace scope instead.

#include <cerastes.h>

template <class T>
struct Outer {
  template <class U> static int f(U y) CERASTES_REQUIRES(y > 0) { return 0; }
  template <> int f<int>(int y) { return 1; } // <- error
};

Members, constructors and destructors

In a member function, this and the members declared before the function are in scope. A class is not a complete context for an annotation, so a member declared later is not. If the contract names something outside the class that a member declared later in the class hides (int limit = 10; before the class, int f(int x) CERASTES_REQUIRES(x < limit) in it and int limit = 3; after it), the name means the outer one in the contract but the member in the body, so cerastes rejects the contract (cerastes-contract_name_hides_member). A member declared in its class and defined outside it follows the rule above:

struct counter {
  int val;
  int get() const CERASTES_REQUIRES(val >= 0) CERASTES_ENSURES(r, r == val)
  {
    return val;
  }
  void set(int v) CERASTES_REQUIRES(v >= 0) CERASTES_ENSURES(val == v);
};

void counter::set(int w) CERASTES_REQUIRES(w >= 0) CERASTES_ENSURES(val == w)
{
  val = w;
}

A constructor’s contract is written after its parameter list and before its member-initializer list. A constructor and a destructor have no result, so ensures takes no result name there.

struct range {
  int lo;
  int hi;
  range(int l, int h) CERASTES_REQUIRES(l <= h) CERASTES_ENSURES(lo == l && hi == h) : lo(l), hi(h) {}
  ~range() CERASTES_REQUIRES(lo <= hi) {}
};

Templates

An annotation in a function template is type-checked in the template, with dependent types, as any template code is. It is checked again in each instance, with the types substituted, and an error found only in an instance is reported with the instantiation context. A template that is never instantiated has its annotations type-checked in the template, but cerastes’s own checks that need the instance are made only in instances. In a template that is never instantiated, these are not checked yet: a fold or unfold whose callee is dependent, a predicate whose return type is dependent, a call of a predicate or a pure function from ordinary code that depends on a template parameter, and an assignment to an object of a template-parameter type.

template <class T>
T inc(T v) CERASTES_REQUIRES(v >= 0) CERASTES_ENSURES(r, r > v)
{
  return v + 1;
}

int use(int x)
{
  return inc(x);
}

Which templates are verified once, for every type that meets their requirements, is a later milestone. Today an annotation in a template is only placed and type-checked.

Loop invariants

invariant(p) is written immediately before a while, do, for or range-based for statement. It says that p holds each time control reaches the loop’s test. A do loop runs its body before its first test, so there the invariant holds at the start of every iteration: on entry, and each time the test is true. continue goes to the test (in a for loop, through the increment), so the invariant must hold there too; break leaves the loop without reaching the test, so it need not. Several invariants on one loop are conjoined.

int sum_to(int n) CERASTES_REQUIRES(n >= 0)
{
  int i = 0;
  int s = 0;
  CERASTES_INVARIANT(0 <= i && i <= n && s >= 0) while (i < n) {
    s += i;
    i += 1;
  }
  return s;
}
int at_least_one(int n) CERASTES_REQUIRES(n >= 0)
{
  int i = 0;
  CERASTES_INVARIANT(0 <= i && i <= n + 1) do {
    i += 1;
  } while (i < n);
  return i;
}

The invariant is read before the loop’s own declarations exist, so declare a loop counter before the loop, not in the for statement. A name declared in the for init-statement, by a range-based for, or in the condition of a while or for (while (int i = next())) is not in scope in its invariant. If nothing else has that name, naming it is an error. If something else does (an outer variable, a data member or static member of the enclosing class, an enumerator, a function), the invariant would silently be about that entity, so cerastes rejects it (see Where annotations are not allowed).

int count(int n) CERASTES_REQUIRES(n >= 0)
{
  int i;
  int c = 0;
  CERASTES_INVARIANT(0 <= i && i <= n && c == i) for (i = 0; i < n; ++i) {
    c += 1;
  }
  return c;
}

The invariant is written before the loop, and nowhere else: not on the loop body and not after it.

Termination measures: decreases

decreases(e1, …​, en) says why a loop or a recursion ends. It has one or more integer expressions, a measure, and it is written in one of two places. Before a loop (next to its invariants) it is the loop’s measure: it must get smaller with every iteration, and must not be negative when the loop condition holds. A do { …​ } while (0), the macro idiom whose body runs once, needs none (when its condition names no variable: do { …​ } while (k) with a constant k equal to zero is an ordinary loop). After a function’s parameter list (with requires and ensures, in any order) it is part of the function’s contract: it is compared from the entry of the function to each recursive call. With several expressions the comparison is lexicographic: at the first one that changes it must have got smaller (from a value that is not negative), and the later ones may be anything.

int count_up(int n) CERASTES_REQUIRES(n >= 0)
{
  int i = 0;
  CERASTES_INVARIANT(0 <= i && i <= n)
  CERASTES_DECREASES(n - i)
  while (i < n) {
    i += 1;
  }
  return i;
}
int count_down(int n)
    CERASTES_REQUIRES(n >= 0)
    CERASTES_DECREASES(n)
    CERASTES_ENSURES(r, r == 0)
{
  if (n == 0) {
    return 0;
  }
  return count_down(n - 1);
}

The measure is an annotation like the others: it has no side effects, may not call cerastes::old, names the parameters of the function by their values on entry, and, in the loop form, may not name a variable that the loop itself declares (the same rule as for invariant). A measure on a function is a contract, so every declaration that carries one must carry the same, and it is refused on a predicate. The same macros build the file with other compilers: CERASTES_DECREASES expands to nothing there.

A measure before anything but a loop, or before a function’s declaration instead of after its parameter list, is an error:

#include <cerastes.h>

int pick(int a, int b) CERASTES_REQUIRES(a >= 0 && b >= 0)
{
  int m = a;
  CERASTES_DECREASES(a) if (a < b) { // <- error
    m = b;
  }
  return m;
}
#include <cerastes.h>

CERASTES_DECREASES(1) int count_down(int n); // <- error

What a measure proves, and what cerastes verify requires (a measure on every loop and every function in a recursion cycle), is on Verifying a program.

check

check(p) states that p holds at that point of the function. It is a statement of its own, and it sees everything in scope there.

int pick(int a, int b) CERASTES_REQUIRES(a >= 0 && b >= 0)
{
  CERASTES_CHECK(a + b >= 0);
  int m;
  if (a < b) {
    CERASTES_CHECK(a < b);
    m = a;
  } else {
    CERASTES_CHECK(a >= b);
    m = b;
  }
  return m;
}

It is named check, not assert, so that it cannot collide with the <cassert> macro. A check is never executed; assert from <assert.h> is code, and cerastes checks it with its run-time meaning (Verifying a program). Write it with braces after an if, because the macro leaves an empty statement behind in an ordinary build (see Building annotated code with ordinary compilers).

Predicates, pure functions, fold and unfold

A predicate is a function that you write in C++ and mark as specification: a named condition that annotations can use. A pure function is a specification function that returns a value. Neither is part of the program that runs. Write the macro first in the declaration:

CERASTES_PREDICATE bool in_range(int lo, int hi, int v)
{
  return lo <= v && v < hi;
}
CERASTES_PURE int clamp_hi(int x, int hi)
{
  return x < hi ? x : hi;
}

A predicate returns bool, cannot also be pure, and has no requires or ensures. A pure function does not return void, and may have a contract. The body of either is ordinary C++ and may use the specification functions below. In an annotation, a call to one is an ordinary call (cerastes verify does not accept it yet, see above).

fold(e) and unfold(e) are statements. Their argument is a call to a predicate: fold records that the predicate’s condition holds and may be used as a unit, and unfold exchanges the unit for the condition it stands for. Their effect is not checked yet, and cerastes verify rejects them; their placement and argument are checked by the front end.

int use([[maybe_unused]] int lo, [[maybe_unused]] int hi, int v) CERASTES_REQUIRES(in_range(lo, hi, v))
{
  CERASTES_UNFOLD(in_range(lo, hi, v));
  int w = v + 0;
  CERASTES_FOLD(in_range(lo, hi, w));
  return w;
}

Specification functions

<cerastes.h> declares five functions in namespace cerastes for use in annotations. They are declared and type-checked like any function, and they are never defined, so a program cannot call one. cerastes recognizes them by the declarations in <cerastes.h>: written cerastes::old(x), or old(x) after using namespace cerastes; or using cerastes::old;, or as a template-id (old<int>(x)). A function of your own with the same name, called qualified with your own namespace (algo::forall, mine::old), is ordinary code, also inside a template, and so is any such call in a file that does not include <cerastes.h>. Inside a template, an unqualified call old(x) (or owns, reads, forall, owns_range) whose callee depends on a template parameter is taken to be the specification function whenever <cerastes.h> is included, even if argument-dependent lookup would find a function of yours: qualify your own functions there (this errs on the side of rejecting). The five functions:

Function What it will mean

owns(place)

full permission to read and write place

reads(place)

permission to read place

old(e)

the value of e on entry, in ensures

owns_range(p, n)

permission to the n elements starting at p

forall(body, free…​)

for every value of the first parameter of body

Today they only have to type-check (and cerastes verify accepts only old); a later milestone gives owns, reads and owns_range their meaning, in the memory model.

struct cell {
  int val;
};

void bump(cell* c)
  CERASTES_REQUIRES(cerastes::owns(c->val) && c->val < 100)
  CERASTES_ENSURES(cerastes::owns(c->val) && c->val == cerastes::old(c->val) + 1)
{
  c->val += 1;
}

int get(const cell* c) CERASTES_REQUIRES(cerastes::reads(c->val)) CERASTES_ENSURES(r, r == c->val)
{
  return c->val;
}

int first(const int* a, unsigned n)
  CERASTES_REQUIRES(n > 0 && cerastes::owns_range(a, n))
  CERASTES_ENSURES(r, r == a[0])
{
  return n > 0 ? a[0] : 0;
}

forall

cerastes::forall(body, free…​) takes a lambda as its first argument. The lambda’s first parameter is the quantified variable, and its other parameters receive the trailing arguments, in order. The lambda has no captures, because an annotation after a parameter list cannot name a parameter inside a lambda: pass what it needs as trailing arguments.

int first_nonneg(const int* a, [[maybe_unused]] int n)
  CERASTES_REQUIRES(n > 0 && cerastes::forall([](int i, const int* a, int n) { return !(0 <= i && i < n) || a[i] >= 0; }, a, n))
  CERASTES_ENSURES(r, r >= 0)
{
  return a[0];
}

In a check or an invariant, which are statements in a function body, a lambda may capture as usual. The form above works there too:

int fill(int* a, int n) CERASTES_REQUIRES(n >= 0)
{
  int i = 0;
  while (i < n) {
    a[i] = 0;
    i += 1;
  }
  CERASTES_CHECK(cerastes::forall([&](int k) { return !(0 <= k && k < n) || a[k] == 0; }));
  return i;
}

The lambda’s parameters have concrete types: a generic lambda (auto parameters, a template lambda) is rejected.

In the contract of a function template, and of a member template of a class template, the lambda may name a template parameter: a parameter of type const T*, sizeof(T) in the body, or, in a member template, the class’s U next to the member’s own T. That is how forall quantifies over an array of T. In the template itself the lambda’s parameter has the dependent type const T *; in each instance it has the deduced type (const int *, const long *).

template <class T>
bool all_pos([[maybe_unused]] const T* data, [[maybe_unused]] int n)
  CERASTES_REQUIRES(n >= 0 && cerastes::forall([](int i, const T* a, int m) { return !(0 <= i && i < m) || a[i] > 0; }, data, n))
{
  return true;
}

template <class U>
struct buffer {
  const U* data;
  int n;

  template <class T>
  bool all_ge([[maybe_unused]] T lo)
    CERASTES_REQUIRES(cerastes::forall([](int i, const U* a, int m, T l) { return !(0 <= i && i < m) || a[i] >= l; }, data, n, lo))
  {
    return true;
  }
};

bool use(const int* p, const long* q, buffer<int>& b)
{
  return all_pos(p, 1) && all_pos(q, 1) && b.all_ge(1) && b.all_ge(2L);
}

Three forms are still rejected. Each is rejected, never accepted with a changed meaning:

  • A lambda that depends on T only through decltype of a function parameter (decltype(data) a). This is valid C++, but the front end cannot yet substitute it in the contract. cerastes reports cerastes-annotation_substitution_error ("an annotation argument is erroneous after template substitution") and then cerastes-unsupported_annotation_expression, both on the contract’s line, when the template is instantiated; the parameter is rejected whether or not the lambda’s body uses it. Write the parameter’s type with the template parameter instead (const T* a).

  • A parameter pack. A contract that names a function parameter pack is rejected by the front end (cannot refer to a function parameter pack), also inside a lambda’s trailing arguments, and a lambda that names a template parameter pack (sizeof…​(Ts)) is rejected when the template is instantiated.

  • A lambda that calls the template whose contract it is in. The front end does not find the name when it substitutes the contract (identifier "h" is undefined, "detected during instantiation of"). A call of a different template from the lambda is accepted by the front end.

cerastes does not yet check that the lambda takes one more parameter than there are trailing arguments. Writing it correctly is your job today.

What cerastes checks, and who reports it

The EDG front end reports an unknown name, the wrong entity or statement kind, an annotation that attaches to nothing, the wrong number of arguments, an argument that is undeclared or ill-typed, every error in a result name, and a reference to a function parameter pack or a pack expansion in an argument. The front end exits with status 2 when it reports one.

cerastes itself reports the rest (listed below), in the same format and at the C++ line. Both exit with status 2.

An annotation does not change anything. It must not contain:

  • a built-in assignment, a built-in compound assignment, ++ or --;

  • new, delete or throw;

  • a read or write of a volatile object;

  • a GNU statement expression.

This includes the body of a lambda written in the annotation. The front end alone accepts a call to a function that is not a specification function, and so an overloaded operator= (or any other overloaded operator), which is a call. cerastes verify rejects every call in an annotation other than cerastes::old (cerastes-call_in_annotation), the implicit ones included.

Every annotation is checked, in whatever file it is: a header, a system header or a directory given with --sys_include is not exempt.

An error inside the argument of a macro such as CERASTES_REQUIRES is reported at the argument’s own line and column, even when the macro invocation spans several lines.

Where annotations are not allowed

Each diagnostic has a tag. EDG’s tags are the names of its messages. cerastes’s own are written cerastes-<tag>. The examples below are tests that expect exactly that diagnostic at the marked line.

A contract before the declaration

requires and ensures belong directly after the parameter list. Written before the declaration, or after the function’s name, they are rejected by cerastes with cerastes-contract_not_after_parameters.

#include <cerastes.h>

int limit = 10;

CERASTES_REQUIRES(limit > 0) int scale(int x); // <- error

If the contract names a parameter, EDG reports undefined_identifier instead, because the parameter does not exist yet at that point:

#include <cerastes.h>

CERASTES_REQUIRES(x > 0) int scale(int x); // <- error

A name that does not exist

An annotation is type-checked like any expression. A name that is not declared is undefined_identifier:

#include <cerastes.h>

int scale(int x) CERASTES_REQUIRES(limit > 0); // <- error

A name in the cerastes namespace that is not one of the nine, such as assert, is unrecognized_attribute:

int f(int x)
{
  [[cerastes::assert(x > 0)]]; // <- error
  return x;
}

A result name that is not allowed

A result name that is also a parameter is decl_hides_function_parameter:

#include <cerastes.h>

int next(int x) CERASTES_ENSURES(x, x > 0); // <- error

On a void function, a constructor or a destructor it is attr_result_name_void_function:

#include <cerastes.h>

void clear(int x) CERASTES_ENSURES(r, x > 0); // <- error

When the return type is deduced it is attr_result_name_deduced_type:

#include <cerastes.h>

auto next(int x) CERASTES_ENSURES(r, r > x) { return x + 1; } // <- error

The wrong entity or statement

requires and ensures on anything but a function are wrong_entity_for_attribute:

#include <cerastes.h>

int limit = 10;
int counter CERASTES_REQUIRES(limit > 0) = 1; // <- error

invariant on a statement that is not a loop is attr_requires_iteration_statement:

#include <cerastes.h>

int f(int n)
{
  CERASTES_INVARIANT(n >= 0) if (n > 0) { // <- error
    n -= 1;
  }
  return n;
}

A variable declared in a for statement is not in scope in the loop’s invariant, so naming it is undefined_identifier:

#include <cerastes.h>

int count(int n)
{
  CERASTES_INVARIANT(i >= 0) for (int i = 0; i < n; ++i) { // <- error
  }
  return n;
}

If an outer variable, a data member (static or not), an enumerator or a function has the same name as the loop’s own variable, the front end finds that one, and the invariant would be about the wrong entity. cerastes rejects an invariant that names an entity which a variable declared in the loop’s init-statement, range-based for declaration or condition hides, cerastes-invariant_shadowed_by_loop_variable. The check is deliberately broad: it rejects any entity with the name of the loop’s variable, however the invariant writes it (i, this→i, (*this).i, Cfg::i, Mode::i), because it cannot tell which spellings the loop’s variable hides. The one exception is a member function called through another object (v.size()). Rename the loop’s variable when the check gets in the way:

#include <cerastes.h>

int count(int n) CERASTES_REQUIRES(n >= 0)
{
  [[maybe_unused]] int i;
  int c = 0;
  CERASTES_INVARIANT(0 <= i && i <= n && c == i) for (int i = 0; i < n; ++i) { // <- error
    c += 1;
  }
  return c;
}

check, fold and unfold on anything but a null statement, a loop for example, are attr_requires_null_statement:

#include <cerastes.h>

int f(int n)
{
  CERASTES_CHECK(n >= 0) while (n > 0) { // <- error
    n -= 1;
  }
  return n;
}

Predicates and pure functions

fold and unfold need a call to a predicate. Anything else is cerastes-fold_callee_not_predicate, or cerastes-fold_argument_not_call when the argument is not a call at all:

#include <cerastes.h>

CERASTES_PURE int twice(int x)
{
  return x + x;
}

int f(int x)
{
  CERASTES_FOLD(twice(x)); // <- error
  return x;
}

A predicate that does not return bool is cerastes-predicate_not_bool:

#include <cerastes.h>

CERASTES_PREDICATE int positive(int x) // <- error
{
  return x > 0;
}

A contract on a predicate is cerastes-contract_on_predicate:

#include <cerastes.h>

CERASTES_PREDICATE bool positive(int x) CERASTES_REQUIRES(x > -100) // <- error
{
  return x > 0;
}

The program must not use a predicate, a pure function or a specification function: a call from ordinary code, a use in a namespace-scope initializer, a default member initializer or a member-initializer, a use as a template argument or in an address constant, or taking its address, is cerastes-spec_call_in_code. The bodies of predicate and pure functions are specification, so they may call the specification functions.

#include <cerastes.h>

CERASTES_PREDICATE bool nonneg(int x)
{
  return x >= 0;
}

int caller(int x)
{
  return nonneg(x) ? 1 : 0; // <- error
}

A constexpr predicate or pure function can be evaluated by the compiler, which would run its body as ordinary code. So the front end refuses to evaluate a call of a predicate or a pure function at compile time once it has seen the marker (a use that comes before the first marker, when the marker is only on a later redeclaration, is not refused: write the marker on the first declaration). Where the language requires a constant expression and the front end evaluates it, the call is an error: an array bound outside a function body (global and member), a static_assert (at any scope), an enumerator, a constexpr variable’s initializer, a bit-field width, alignas, a template argument that is used (explicit, or a default one that an instantiation takes), the noexcept(…​) specifier, explicit(…​), a case label, if constexpr. The front end’s message is expression must have a constant value, followed by a note that says it cannot call the function in a constant expression because an attribute of the function does not allow it.

#include <cerastes.h>

CERASTES_PURE constexpr int scale(int x)
{
  return x + 1;
}

int g_table[scale(3)]; // <- error

Other uses are found by cerastes, not by the front end, and are reported as cerastes-spec_call_in_code:

  • a decltype or sizeof operand, and the noexcept(…​) operator (the specifier after a function’s parameters is the front end’s);

  • an array bound in a function body (the front end reads it as a variable-length array, so it does not evaluate it), also inside a sizeof operand;

  • a default template argument that no instantiation uses;

  • the body of a constexpr or consteval function;

  • any of these uses inside a template that is never instantiated.

A marker on a function that is defaulted (P() = default;, or a defaulted comparison) is refused by the front end too: "an attribute that forbids constant evaluation cannot be applied to a function that is defaulted". A deleted function can carry the marker.

A function marked both predicate and pure is cerastes-predicate_and_pure, and a pure function that returns void is cerastes-pure_returns_void.

The marker goes on a function of your own. On a constructor, a destructor or an assignment operator (which have effects, defaulted or not) it is cerastes-spec_marker_on_special_member, and a marker written in a system header is cerastes-spec_marker_in_system_file. Do not mark a library function that you redeclare, and write the marker on the first declaration of a function: cerastes does not check either yet, and a use that comes before the marker is not refused by the front end’s constant evaluation (see above).

Side effects and old

An annotation that changes something is cerastes-annotation_side_effect:

#include <cerastes.h>

int f(int x)
{
  int y = x;
  CERASTES_CHECK((y = 5) > 0); // <- error
  return y;
}

cerastes::old outside ensures is cerastes-old_outside_ensures:

#include <cerastes.h>

void incr(int& x) CERASTES_REQUIRES(cerastes::old(x) < 1000) // <- error
{
  x += 1;
}

old also does not belong in the body of a predicate or a pure function, which has no entry state to name: that is cerastes-old_outside_ensures too, whether it is called, its address is taken, or it is named in a template.

#include <cerastes.h>

CERASTES_PURE int previous(int x)
{
  return cerastes::old(x); // <- error
}

Declarations that disagree

A later declaration with a different contract is attr_redeclaration_mismatch:

#include <cerastes.h>

int bump(int x) CERASTES_REQUIRES(x > 0);
int bump(int x) CERASTES_REQUIRES(x > 10); // <- error

So is an explicit specialization whose contract differs from the primary template’s:

#include <cerastes.h>

template <class T> T twice(T v) CERASTES_REQUIRES(v >= 0) CERASTES_ENSURES(r, r >= v);

template <> int twice<int>(int v) CERASTES_REQUIRES(v > 0) CERASTES_ENSURES(r, r >= v) // <- error
{
  return v + v;
}

And so is repeating a contract that contains a lambda, even when the text is the same:

#include <cerastes.h>

bool all_nonneg(const int* a, int n)
  CERASTES_REQUIRES(n >= 0 && cerastes::forall([](int i, const int* a, int n) { return !(0 <= i && i < n) || a[i] >= 0; }, a, n));

bool all_nonneg(const int* a, int n)
  CERASTES_REQUIRES(n >= 0 && cerastes::forall([](int i, const int* a, int n) { return !(0 <= i && i < n) || a[i] >= 0; }, a, n)) // <- error
{
  for (int i = 0; i < n; ++i) {
    if (a[i] < 0) {
      return false;
    }
  }
  return true;
}

Lambdas, deduction guides and modules

A lambda cannot carry a contract: the attribute would attach to the closure’s call operator. Written after the lambda’s parameter list, it is wrong_entity_for_attribute. Written between the introducer and the parameter list, cerastes rejects it with cerastes-annotation_on_lambda.

#include <cerastes.h>

int use(int x)
{
  auto twice = [] CERASTES_REQUIRES(true) (int v) { return v + v; }; // <- error
  return twice(x);
}

A lambda that you write in an annotation, as in forall, must have concrete parameter types. A generic lambda (an auto parameter, or a template lambda such as []<class T>(T x) { …​ }) is rejected with cerastes-generic_lambda_in_annotation, because its call operator is never instantiated in an annotation, so a body that does not compile would be accepted without a word.

#include <cerastes.h>

int first_nonneg(const int* a, [[maybe_unused]] int n)
  CERASTES_REQUIRES(n > 0 && cerastes::forall([](auto i, const int* a, int n) { return !(0 <= i && i < n) || a[i] >= 0; }, a, n)) // <- error
{
  return a[0];
}

A lambda in the contract of a function template may name a template parameter, but not through decltype of a function parameter alone. That is rejected when the template is instantiated, with cerastes-annotation_substitution_error and cerastes-unsupported_annotation_expression on the contract’s line:

#include <cerastes.h>

template <class T>
bool all_pos([[maybe_unused]] T* data, [[maybe_unused]] int n)
  CERASTES_REQUIRES(cerastes::forall([](int i, decltype(data) a, int m) { return !(0 <= i && i < m) || a[i] > 0; }, data, n)) // <- error
{
  return true;
}

bool use(int* p)
{
  return all_pos(p, 1);
}

A deduction guide cannot carry a contract either. The front end rejects an attribute written after the guide’s parameters (wrong_entity_for_attribute) and one written between the template header and the guide (unattached_attribute). A parameter of a requires-expression is not a function, so a contract after it is wrong_entity_for_attribute too.

C++20 modules are not supported yet. A module unit is rejected with cerastes-modules_unsupported, because a contract on an entity that a module file exports is not carried through it.

Changing the cerastes macro

The front end defines __CERASTES__. Undefining it, or defining it again, in the source (#undef, #define) is cerastes-cerastes_macro_changed. The macros of <cerastes.h> no longer depend on it, but code of your own that tests __CERASTES__ would silently stop seeing what the front end reads. On the command line the options that do it are refused before the front end runs. The report is positioned at the line of the #undef or #define, also when it is written with a line splice, a comment or a digraph. cerastes reads the source text to find it, so a source that it cannot read twice (standard input) is rejected with cerastes-source_scan_incomplete, and the precompiled-header options are refused.

#include <cerastes.h>

#undef __CERASTES__ // <- error

The same holds for every name that the annotations depend on. A #define or #undef, anywhere in the translation unit and outside <cerastes.h> itself, of one of these is cerastes-annotation_macro_changed, reported at the directive:

  • cerastes, an attribute name (requires, ensures, invariant, check, fold, unfold, predicate, pure) and a specification-function name (old, owns, reads, forall, owns_range): #define ensures requires would turn every postcondition into a precondition;

  • CERASTES_H and every CERASTES_* macro, which are the header’s own;

  • every predefined macro of the front end, among them __cplusplus, __STDC_VERSION__, __has_cpp_attribute and __has_c_attribute: the header uses them to decide whether the annotations are on, and the header stops with an #error when they were changed before it was included.

The check uses the front end’s own record of what the preprocessor did, so a directive in a comment, a string literal or a skipped #if 0 group does not count, and neither does one that changes nothing: an #undef of a macro that is not defined, or the identical redefinition of one that is. A header of the system that defines one of these names is rejected as well.

#include <cerastes.h>

#define ensures requires // <- error

int half(int x) CERASTES_REQUIRES(x >= 0);

<cerastes.h> in a namespace

<cerastes.h> must be included at global scope. Included inside a namespace, it declares foo::cerastes::owns and the others, which no check of cerastes recognizes as specification functions, so their uses would be read as ordinary code. A use of such a function is cerastes-cerastes_header_in_namespace:

namespace foo {
#include <cerastes.h>
}

struct cell {
  int val;
};

void set(cell* c, int v)
  CERASTES_REQUIRES(foo::cerastes::owns(c->val)) // <- error
{
  c->val = v;
}

Language modes

cerastes reads C++ in Clang’s emulation mode, and C as C23. It refuses to run in GNU emulation (--gnu_version), and it refuses C before C23. Redeclarations in different namespaces could otherwise escape the rule that contracts must match, and the identifier-list declarators of older C could bind the names in a contract to global variables.

Seeing what cerastes reads

The front end can print a listing of what it understood. From a clone of the repository, build it with scripts/bootstrap.sh (see Installation), then run it on a file:

scripts/cerastes-fe.sh --c++20 --cerastes_walk annotated.cpp

The listing has one entry for each routine of the file you named (routines that come from other files, such as the headers it includes, are not listed), with the annotations that belong to it under it, each followed by the typed expression tree of its arguments: the parameters, the result name, the operators and the types. Annotations on statements are listed under their routine. For the contract above, this is the whole listing:

routine abs_val plain body @ L7:5
  returns int
  param 1 x: int
  attr [[cerastes::requires]] on routine @ L7:20
    arg 1 @ L7:38
      op eok_gt type_kind=tk_integer type=bool @ L7:40
        param 1 x: int @ L7:38
        const -1000000 type=int @ L7:42
  attr [[cerastes::ensures]] on routine @ L7:52
    arg 1 binder r: int @ L7:69
    arg 2 @ L7:72
      op eok_land type_kind=tk_integer type=bool @ L7:79
        op eok_ge type_kind=tk_integer type=bool @ L7:74
          binder r: int @ L7:72
          const 0 type=int @ L7:77
        op eok_lor type_kind=tk_integer type=bool @ L7:90
          op eok_eq type_kind=tk_integer type=bool @ L7:85
            binder r: int @ L7:83
            param 1 x: int @ L7:88
          op eok_eq type_kind=tk_integer type=bool @ L7:95
            binder r: int @ L7:93
            op eok_negate type_kind=tk_integer type=int @ L7:98
              param 1 x: int @ L7:99
end walk: 1 routines reported, 0 routines with bodies in non-system files outside the primary file

The listing is a developer view, not a stable interface: use it to see where an annotation landed and how a name was resolved, for example whether a name in a precondition is a parameter or something else.