Building annotated code with ordinary compilers

Source that carries cerastes annotations is meant to build, unchanged, with the compiler you already use. This page says how, and what to watch for. It applies to Apple clang and GCC, with -std=c++20 for C++ and -std=c23 for C, and warnings turned all the way up.

One source, two builds

Include <cerastes.h> and write the annotations with its CERASTES_* macros (Annotations). The header defines them in one of two ways, and it chooses by asking the compiler whether it knows the attributes, not by looking at a macro: __has_cpp_attribute(cerastes::requires) (in C23, __has_c_attribute(cerastes::requires)) is 1 only in cerastes’s front end.

In cerastes’s front end each macro expands to the attribute it stands for.
Any other compiler gives 0, so the contract and statement macros expand to nothing.

The front end also defines the macro __CERASTES__, for your own #ifdef. You never define it in a build, and cerastes refuses to undefine it or define it again, on the command line (-U, -D) and in the source (#undef, #define, cerastes-cerastes_macro_changed): both are errors. Because the header does not depend on it, undefining it could not turn the contracts off, but it is still reported. The header has no #error of its own.

The macros of <cerastes.h> are not a place to customize. Redefining one of them (for example CERASTES_CHECK), or defining the guard CERASTES_H before including the header, is not supported, and cerastes does not detect it: the annotations would silently mean something else, or nothing.

#include <cerastes.h>

int sum_to(int n) CERASTES_REQUIRES(n >= 0) CERASTES_ENSURES(r, r >= 0)
{
  int i = 0;
  int s = 0;
  CERASTES_INVARIANT(0 <= i && i <= n && s >= 0) while (i < n) {
    s += i;
    i += 1;
  }
  CERASTES_CHECK(s >= 0);
  return s;
}

For cerastes this function has a contract, a loop invariant and a check. For clang or GCC it is the same function without them. The written-out form below is what the macro for a precondition expands to in each case:

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

You can write the attribute yourself like this, but you should not write it bare, outside the guard: clang warns unknown attribute … ignored (-Wunknown-attributes) and GCC warns scoped attribute directive ignored (-Wattributes), and either becomes an error under -Werror. That is why the macros exist.

The include path

The header is include/cerastes.h in the cerastes repository. It includes no other header, so it works with any standard library.

For clang or GCC, give the directory with -I:

clang++ -std=c++20 -Wall -Wextra -Werror -I path/to/cerastes/include -c sum_to.cpp
g++ -std=c++20 -Wall -Wextra -Werror -I path/to/cerastes/include -c sum_to.cpp

scripts/cerastes-fe.sh adds the same directory for you, as a system include directory, so it needs no option.

Predicates and pure functions

CERASTES_PREDICATE and CERASTES_PURE expand to the attribute and inline for cerastes, and to inline alone for an ordinary compiler. Both builds give the function the same linkage, and a function that nothing calls is not emitted, so an unused predicate causes no warning.

Write the macro first in the declaration, before static, constexpr and the return type. An attribute cannot appear in the middle of a decl-specifier sequence.

CERASTES_PREDICATE constexpr bool small(int x)
{
  return x < 10;
}

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

The program must not call a predicate or a pure function. A predicate that an ordinary compiler does emit (because something called it) calls specification functions, and those are the next section’s subject.

Specification functions are declared, not defined

cerastes::owns, reads, old, forall and owns_range are declared in <cerastes.h> and never defined. They are only ever named inside annotations, which an ordinary compiler never sees, or inside the body of a predicate or a pure function. If a program calls one of them, directly or through a predicate that it calls, the build ends in a link error that names a cerastes:: function. Read that error as "specification code is reachable at run time": find the call and remove it. A definition that returned true would have let such a call succeed silently.

Warnings to expect

An annotation that an ordinary compiler removes can leave something behind. Three cases come up:

A parameter that only a contract uses draws -Wunused-parameter. Mark the parameter [[maybe_unused]].
A local variable that only a CERASTES_CHECK uses draws -Wunused-variable. Mark it [[maybe_unused]].
CERASTES_CHECK(p); leaves an empty statement. After if (c) with no braces that draws -Wempty-body, so write the braces.

int first(const int* a, [[maybe_unused]] int n) CERASTES_REQUIRES(n > 0)
{
  return a[0];
}

int twice(int x)
{
  [[maybe_unused]] int before = x;
  int r = x + x;
  CERASTES_CHECK(r == before + before);
  return r;
}

int f(int x)
{
  if (x > 0) {
    CERASTES_CHECK(x > 0);
  }
  return x;
}

C

In C23 the macros work as well, because a attribute is valid C23 and may follow a function declarator. Build with -std=c23. The specification functions in namespace cerastes are C++ only for now, so a C program uses the macros, and predicates written in C, but not owns and the others.

#include <cerastes.h>

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

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