Error messages

When cerastes verify cannot prove something, it prints one error per problem, at the line of the C or C++ source that causes it:

<file>:<line>: error: <category>: <message>
<file>:<line>: note: <what the note says>

The category names what could not be proved. There are thirteen, and each has a section below. A note line follows an error when a second place matters: the clause of a contract that failed, or the callee’s clause that a call does not meet. Errors are sorted by file, line and category, and the exit status is 1 when there are any. Verifying a program describes the command and the other exit statuses.

Every example below is a program that fails with exactly the error named in its section (the example’s line is the one the error points at), followed by the same program fixed so that it verifies.

cerastes proves that an error cannot happen on any path, with the information it has: contracts, branches and loop invariants. It does not run your program. An error means that it could not exclude the problem, and not necessarily that a run reaches it. To find out which, use the counterexample in your head or a test; then either fix the code or give the verifier the missing fact.

Problems that are not verification errors, for example a program the tool does not accept, are described in What is not supported yet.

precondition

A call may not satisfy a CERASTES_REQUIRES clause of the function it calls. It is reported at the call, with a note that names the clause of the callee.

The verifier could not show that the arguments meet the callee’s precondition on every path that reaches the call. Here use_half passes m, which may be odd, to half, which requires an even number.

#include <cerastes.h>

int half(int n)
    CERASTES_REQUIRES(n >= 0 && n % 2 == 0)
    CERASTES_ENSURES(r, r == n / 2)
{
  return n / 2;
}

int use_half(int m)
    CERASTES_REQUIRES(m >= 0)
{
  return half(m);
}

precondition_error.cpp:16: error: precondition: the precondition of `half` may not hold
precondition_error.cpp:7: note: this is the requirement of `half`

How to fix it. Either establish the precondition before the call (a test and an early return, or a stronger CERASTES_REQUIRES on the caller, as below), or weaken what the callee requires if it does not need it.

#include <cerastes.h>

int half(int n)
    CERASTES_REQUIRES(n >= 0 && n % 2 == 0)
    CERASTES_ENSURES(r, r == n / 2)
{
  return n / 2;
}

int use_half(int m)
    CERASTES_REQUIRES(m >= 0 && m % 2 == 0)
{
  return half(m);
}

postcondition

A CERASTES_ENSURES clause may not hold when the function returns. It is reported at the return statement that may leave the clause false (or at the closing brace of a void function), with a note at the clause.

The value the function returns, together with what is known about the parameters, does not imply the clause. In the example the function returns one more than the contract allows.

#include <cerastes.h>

int double_it(int x)
    CERASTES_REQUIRES(0 <= x && x <= 1000)
    CERASTES_ENSURES(r, r == 2 * x)
{
  return 2 * x + 1;
}

postcondition_error.cpp:10: error: postcondition: the postcondition of `double_it` may not hold
postcondition_error.cpp:8: note: this is the postcondition

How to fix it. Change the code so that it returns the right value, or change the contract if it states the wrong thing. If the clause holds only for some arguments, add the condition to CERASTES_REQUIRES. Remember that a parameter in a postcondition is its value on entry.

#include <cerastes.h>

int double_it(int x)
    CERASTES_REQUIRES(0 <= x && x <= 1000)
    CERASTES_ENSURES(r, r == 2 * x)
{
  return 2 * x;
}

check

A CERASTES_CHECK may not hold. It is reported at the check.

What the verifier knows at that point (the precondition, the assignments and the branches taken) does not imply the condition. A check is a claim for the verifier to prove, and never an assumption.

#include <cerastes.h>

int step(int x)
    CERASTES_REQUIRES(0 <= x && x < 100)
{
  int y = x + 10;
  CERASTES_CHECK(y < 100);
  return y;
}

check_error.cpp:10: error: check: this `check` may not hold

An assert(e) from <assert.h> that may fail is reported in the same way, at the assert; the message names assert instead of check.

How to fix it. Establish the condition (a stronger precondition or loop invariant, as below), or correct the check.

#include <cerastes.h>

int step(int x)
    CERASTES_REQUIRES(0 <= x && x < 90)
{
  int y = x + 10;
  CERASTES_CHECK(y < 100);
  return y;
}

invariant-entry

A loop invariant may not hold when the loop is first reached. It is reported at the invariant clause.

The invariant must be true before the first evaluation of the loop condition. In the example i starts at 1, so when n is 0 the clause i ⇐ n is false on entry.

#include <cerastes.h>

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

invariant_entry_error.cpp:11: error: invariant-entry: this loop invariant may not hold on entry

How to fix it. Initialize the variables so that the invariant holds, or weaken the invariant. The error is about the first iteration; an invariant that is wrong later is invariant-preserved.

#include <cerastes.h>

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

invariant-preserved

A loop invariant may not hold again after an iteration of the body that started with it true. It is reported at the invariant clause.

The invariant and the loop condition hold at the start of the body, but the body, followed by the loop’s increment, may leave the invariant false. Here i += 2 can step past n.

#include <cerastes.h>

int count_to(int n)
    CERASTES_REQUIRES(0 <= n && n <= 1000)
    CERASTES_ENSURES(r, r >= 0)
{
  int i = 0;
  CERASTES_INVARIANT(0 <= i && i <= n)
  CERASTES_DECREASES(n - i)
  while (i < n) {
    i += 2;
  }
  return i;
}

invariant_preserved_error.cpp:11: error: invariant-preserved: this loop invariant may not be preserved by an iteration

How to fix it. Change the body so that it keeps the invariant, or strengthen or weaken the invariant until it is both preserved and strong enough to prove what follows the loop. A loop’s condition is checked each time it is evaluated, so an arithmetic error in the condition is reported separately.

#include <cerastes.h>

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

overflow

A signed arithmetic operation may produce a value that does not fit its type, or a signed division may be the smallest value divided by -1. It is reported at the operator.

Signed overflow is undefined behaviour in C and C++, so cerastes treats it as an error rather than assuming it wraps. See Integer semantics for the exact rules. Unsigned arithmetic never gives this error: it wraps. The error also appears for arithmetic inside a contract.

#include <cerastes.h>

int increment(int x)
{
  return x + 1;
}

overflow_error.cpp:8: error: overflow: signed `int` addition may overflow

How to fix it. Bound the operands in a CERASTES_REQUIRES, as below, test before computing, compute in a wider type, or use an unsigned type if wrapping is what you mean.

#include <cerastes.h>

int increment(int x)
    CERASTES_REQUIRES(x < 2147483647)
{
  return x + 1;
}

division-by-zero

A divisor of / or % may be zero. It is reported at the operator.

Nothing in the precondition or the code before the division excludes a zero divisor.

#include <cerastes.h>

unsigned per_item(unsigned total, unsigned count)
{
  return total / count;
}

division_by_zero_error.cpp:8: error: division-by-zero: the divisor may be zero

How to fix it. Require the divisor to be non-zero, or test it before dividing.

#include <cerastes.h>

unsigned per_item(unsigned total, unsigned count)
    CERASTES_REQUIRES(count != 0u)
{
  return total / count;
}

shift

A shift may have a count that is negative or at least the width of the promoted left operand, or a left shift of a signed value may have a negative left operand or a result that does not fit. It is reported at the operator.

In the example the count n may be 32 or more, which is undefined for a 32-bit unsigned.

#include <cerastes.h>

unsigned bit(unsigned n)
{
  return 1u << n;
}

shift_error.cpp:8: error: shift: the shift count may be negative or at least the width (32 bits) of `unsigned int`

How to fix it. Bound the count, as below, or mask or reduce it before shifting. Mind that operands narrower than int are promoted first, so the width that matters is the promoted type’s.

#include <cerastes.h>

unsigned bit(unsigned n)
    CERASTES_REQUIRES(n < 32u)
{
  return 1u << n;
}

conversion

A conversion to a signed type may be given a value that does not fit, or a conversion to an enumeration a value that is not one of the enumeration’s values. It is reported at the conversion: the cast, the initializer, the assignment, the argument or the return.

cerastes does not accept a wrapping conversion to a signed type, written or implicit, because the standards disagree on what it means. Conversions to unsigned types wrap and are never an error.

#include <cerastes.h>

signed char to_small(int x)
    CERASTES_REQUIRES(0 <= x && x <= 200)
{
  return (signed char)x;
}

conversion_error.cpp:9: error: conversion: the value may not fit in `signed char` (a conversion to a signed type must be exact)

How to fix it. Bound the value so that it fits, as below, or convert to the unsigned type of the same width and use that.

#include <cerastes.h>

signed char to_small(int x)
    CERASTES_REQUIRES(0 <= x && x <= 127)
{
  return (signed char)x;
}

A conversion to an enumeration is checked against the enumeration’s values (Enumerations), never wrapped, also when the enumeration’s underlying type is unsigned:

#include <cerastes.h>

enum color { RED, GREEN, BLUE };

enum color from_int(int x)
{
  return (enum color)x;
}

enumeration_range.c:11: error: conversion: the value may not be one of the values of `enum color` (0 to 3)

How to fix it. Bound the value with a requires or a test before the cast.

missing-return

A function that returns a value may reach its closing brace without a return. It is reported at the closing brace.

Flowing off the end of a non-void function is undefined behaviour in C++ and C when the caller uses the result. The only exception is main, which returns 0.

#include <cerastes.h>

int sign(int x)
{
  if (x > 0) {
    return 1;
  }
  if (x < 0) {
    return -1;
  }
}

missing_return_error.cpp:14: error: missing-return: control may reach the end of `sign` without returning a value

How to fix it. Add the missing return, or restructure the function so that every path returns.

#include <cerastes.h>

int sign(int x)
{
  if (x > 0) {
    return 1;
  }
  if (x < 0) {
    return -1;
  }
  return 0;
}

termination

A termination measure (CERASTES_DECREASES) may be negative, or may not decrease. For a loop it is reported at the loop’s CERASTES_DECREASES clause, and for a recursive function at the recursive call, with a note at the callee’s measure.

The measure must get smaller from one iteration to the next (for a function, from the entry to each recursive call), and must not be negative when the loop condition holds. A measure that stays the same, grows, or can go below zero does not show that the loop or recursion ends, so cerastes does not accept it. In the example the body forgot to add 1 to i.

#include <cerastes.h>

int count_to(int n)
    CERASTES_REQUIRES(n >= 0)
    CERASTES_ENSURES(r, r == n)
{
  int i = 0;
  CERASTES_INVARIANT(0 <= i && i <= n)
  CERASTES_DECREASES(n - i)
  while (i < n) {
  }
  return i;
}

termination_error.cpp:12: error: termination: the measure of this loop may not decrease, or may not be bounded below by zero

How to fix it. Change the code so that the measure decreases, as below, or choose a measure that does: for a loop that counts up to n, the distance n - i to the bound. A measure with several expressions is compared lexicographically (see Verifying a program). The measure’s own arithmetic is checked too: an overflow in it is an overflow error at the measure.

#include <cerastes.h>

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

noreturn

A function declared not to return (with the attribute noreturn, or with _Noreturn in C) may return. It is reported at the return that may be reached, or at the closing brace.

Returning from such a function is undefined behaviour in C and C++: its callers are compiled, and verified, as if the call never comes back. Every path through its body must end in a call of another function that does not return, such as abort or exit.

#include <stdlib.h>
#include <cerastes.h>

// Ends the program when bad is not zero.
[[noreturn]] void fail_if(int bad)
{
  if (bad) {
    abort();
  }
}

noreturn_error.c:14: error: noreturn: `fail_if` is declared not to return, but control may reach its end

How to fix it. Make every path end in a call that does not return, or remove the attribute noreturn. A function that ends the program only on some inputs is better written without the condition, with the test at the call:

#include <stdlib.h>
#include <cerastes.h>

[[noreturn]] void fail(void)
{
  abort();
}

int check_positive(int x)
    CERASTES_ENSURES(r, r > 0)
{
  if (x <= 0) {
    fail();
  }
  return x;
}

The contract of check_positive is what its callers rely on: the path through fail() ends the program, so only the path that returns has to satisfy r > 0.

uninitialized

A local variable may be read before it has a value. It is reported at the read.

A variable declared without an initializer has no value until it is assigned: reading it first is undefined behaviour in C and in C++ (erroneous behaviour in C++26), and it is the first thing the C++ initialization profile forbids (P4222). Look for a path that reaches the read without passing an assignment: a branch that does not assign the variable, a loop that may run zero times, a switch without default, or a goto or case label that jumps past the assignment, or a read that comes before an assignment in the same expression ((y = x, x = 1)). A read is any use of the value, including the old value in x += 1 or x++, a return, an argument, and an annotation such as CERASTES_CHECK or a loop invariant (there it is reported where the invariant is checked).

#include <cerastes.h>

int positive_or_none(int a)
{
  int r;
  if (a > 0) {
    r = a;
  }
  return r;
}

uninitialized_error.c:12: error: uninitialized: `r` may be read here before it is given a value

How to fix it. Give the variable a value on every path that reaches the read, or initialize it where it is declared. cerastes follows the paths of the program, so the assignments need not be in the same branch as the read, only on every way to it:

#include <cerastes.h>

int positive_or_none(int a)
    CERASTES_ENSURES(res, res == (a > 0 ? a : -1))
{
  int r;
  if (a > 0) {
    r = a;
  } else {
    r = -1;
  }
  return r;
}