Integer semantics

This page says what cerastes proves about integer arithmetic. It describes one meaning for each expression, used for C23 and for C++20 alike, so a .c file verifies, or fails, the same way in both modes. Where the two standards differ, cerastes takes the stricter rule. Each rule below says what is an error, and every error is reported at the operator with the category named in Error messages.

In short:

  • signed arithmetic that does not fit its type is an error;

  • unsigned arithmetic wraps;

  • a conversion to a signed type that does not fit is an error, with or without a cast;

  • division by zero, and a shift whose count or result is out of range, are errors;

  • operands narrower than int are promoted, as in C and C++, and that has consequences you can prove or trip over;

  • a value of an enumeration is always one of its values, and a conversion into an enumeration that may not give one is an error.

Types and ranges

The integer types are bool, char, signed char, unsigned char, short, int, long, long long and their unsigned forms, wchar_t, char8_t, char16_t, char32_t, and __int128 with unsigned __int128. Their sizes and whether plain char is signed come from the compiler’s description of the target (on macOS for Apple silicon int is 32 bits, long is 64 and plain char is signed), never from constants inside cerastes.

A value of a type is always inside its range. A parameter is assumed to be in the range of its type when the function starts, and cerastes proves that every result, and every value an operation produces, is in range too.

Enumerations have their own range, described in Enumerations. _BitInt, floating point and vector types are rejected in this version (the list of constructs not yet supported). So are the bitwise operators &, |, ^ and ~.

Signed overflow is an error

+, -, *, unary -, ++, -- and the compound assignments on a signed type must produce a value that fits the type. If one may not, cerastes reports overflow at the operator. This holds wherever they appear: the value of an assignment used inside an expression is the value stored, converted to the variable’s type by the rules below.

#include <cerastes.h>

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

The fix is to state in a contract what the caller must guarantee:

#include <cerastes.h>

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

Unsigned arithmetic wraps

An unsigned operation produces the mathematical result modulo 2N, as both standards define it, so it is never an error, and a contract can rely on it. That includes -u, which is 2^N - u for u != 0, and << on an unsigned value.

#include <cerastes.h>

unsigned wrap(unsigned x)
    CERASTES_REQUIRES(x == 4294967295u)
    CERASTES_ENSURES(r, r == 0u)
{
  return x + 1u;
}

Conversions

Conversion to Rule

an unsigned type

modulo 2N, no error

a signed type

the value must fit, otherwise conversion; this holds for an implicit conversion and for a cast written by you ((short)x, static_cast<short>(x)), and for an initialization, an assignment, a compound assignment, an argument and a return value

an enumeration

the value must be one of the values of the enumeration, otherwise conversion; this holds for a cast, for C’s implicit conversions, and for an enumeration whose underlying type is unsigned: it never wraps (Enumerations)

bool

v != 0

C++20 defines the conversion of an out-of-range value to a signed type as modular, and C23 leaves it to the implementation. cerastes makes it an error in both, which is also what VeriFast does by default. A conversion that cannot lose anything (the source range lies within the target’s) needs no check.

#include <cerastes.h>

signed char small(int x)
    CERASTES_REQUIRES(0 <= x && x <= 127)
    CERASTES_ENSURES(r, r == x)
{
  return (signed char)x;
}

unsigned char low_byte(int x)
    CERASTES_ENSURES(r, r >= 0)
{
  return (unsigned char)x;
}

small verifies because the contract keeps x in the range of signed char. low_byte converts to an unsigned type, which wraps. Without the requires, (signed char)x is the error:

#include <cerastes.h>

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

To get a wrapped byte from a value, convert to the unsigned type first, as low_byte does, and then use the unsigned value; do not rely on a signed type wrapping.

Promotions and the usual arithmetic conversions

C and C++ compute with operands of rank lower than int in int. cerastes follows them exactly, so these faithful consequences apply:

  • the product of two unsigned short values is computed in int, and can overflow it;

  • unsigned char operands promote to int, so the product of two of them always fits, and converting it back to unsigned char wraps;

  • when int meets unsigned, the int converts to unsigned, so -1 < 0u is false and i + 0u > 0u is true for i == -1.

#include <cerastes.h>

unsigned char scale(unsigned char a, unsigned char b)
    CERASTES_ENSURES(r, r == (a * b) % 256)
{
  return a * b;
}
#include <cerastes.h>

unsigned short product(unsigned short a, unsigned short b)
{
  return a * b;
}

The same arithmetic gives the same answer in C23 and in C++20:

#include <cerastes.h>

int sum_is_positive(int i)
    CERASTES_REQUIRES(i == -1)
    CERASTES_ENSURES(r, r == 1)
{
  return i + 0u > 0u;
}

A compound assignment computes in the common type of its operands and then converts the result back to the variable’s type, with the check of the conversion table above. So us *= us on unsigned short is computed in int and then converted back, and c += 1 on a signed char is an error when c is the largest signed char.

In C, a condition (of if, while, for and ?:, and an operand of !, && and ||) is true when it is not zero, and a comparison produces an int with the value 0 or 1. In C++ those positions are bool. A contract means the same either way:

#include <cerastes.h>

int is_zero(int x)
    CERASTES_ENSURES(r, r == (x == 0))
{
  if (x) {
    return 0;
  }
  return 1;
}

Division and remainder

/ and % truncate toward zero. A zero divisor is an error, division-by-zero. For a signed type, the smallest value divided by -1 does not fit, so it is overflow, not a division by zero.

#include <cerastes.h>

int quotient(int a)
    CERASTES_REQUIRES(a == -7)
    CERASTES_ENSURES(r, r == -3)
{
  return a / 2;
}

int remainder_of(int a)
    CERASTES_REQUIRES(a == -7)
    CERASTES_ENSURES(r, r == -1)
{
  return a % 2;
}
#include <cerastes.h>

int quotient(int a, int b)
    CERASTES_REQUIRES(b != 0)
{
  return a / b;
}

Shifts

The count of a shift must be at least 0 and less than the width of the promoted left operand; otherwise it is shift. Left shift of an unsigned value wraps. Left shift of a signed value must have a non-negative left operand and a result that fits; C++20 would define more, but cerastes uses C23’s stricter rule in both modes. Right shift of a negative value is arithmetic (it rounds toward negative infinity): defined in C++20 and what this target does in C23.

#include <cerastes.h>

int halve(int a)
    CERASTES_REQUIRES(a == -8)
    CERASTES_ENSURES(r, r == -4)
{
  return a >> 1;
}

unsigned top_bit(unsigned x)
    CERASTES_REQUIRES(x == 3u)
    CERASTES_ENSURES(r, r == 2147483648u)
{
  return x << 31;
}
#include <cerastes.h>

int shift_up(int a)
    CERASTES_REQUIRES(a == -1)
{
  return a << 1;
}

Annotations mean their C value

An annotation is an expression of the program’s language, and it means what that expression computes. Unsigned arithmetic wraps in a contract too, and signed overflow, a division by zero, a bad shift or a narrowing conversion in a contract is an error at the annotation’s line, with the same category as in code. Each clause is checked under the clauses before it, so a requires may rely on an earlier requires, and an ensures on every requires and the earlier ensures.

#include <cerastes.h>

int larger(int a, int b)
    CERASTES_REQUIRES(a + b > 0)
{
  return a > b ? a : b;
}

To reason with unbounded arithmetic in a contract, widen the operands:

#include <cerastes.h>

int larger(int a, int b)
    CERASTES_REQUIRES((long long)a + b > 0)
    CERASTES_ENSURES(r, r >= a && r >= b)
{
  return a > b ? a : b;
}

Constants

A constant the compiler has already folded is checked as you wrote it, so signed char c = 300; and return 300; from a function returning signed char are conversion errors, while unsigned u = -1; is fine:

#include <cerastes.h>

unsigned all_ones(void)
    CERASTES_ENSURES(r, r == 4294967295u)
{
  unsigned u = -1;
  return u;
}
#include <cerastes.h>

signed char too_big(void)
{
  return 300;
}

The compiler’s own warnings for these (overflow in a constant, a bad shift count, a division by zero, a sign change, a truncation, a missing return) are not shown by cerastes verify: the verifier reports each problem itself, once, with its category. A #pragma that changes a warning cannot hide a problem from it: the front end’s diagnostic pragmas are refused in the files it verifies.

A named constant, a const global, is checked the same way: its initializer as you wrote it, whether or not anything uses it, so const short limit = 70000; is a conversion error at its line (Named constants).

Enumerations

An enumeration and its enumerators are verified in both modes. Each enumeration has a range of values:

  • an enumeration whose underlying type is fixed (enum small : unsigned char, and every C++ enum class, whose underlying type is int unless you write another) has the values of that type;

  • any other enumeration has the values of the smallest bit-field that holds all its enumerators, as in C++: enum color { RED, GREEN, BLUE } has the values 0 to 3, enum sign { NEG = -1, ZERO, POS } the values -2 to 1.

A value of an enumeration is always in that range. A parameter is assumed to be in it, a result must be in it, and every conversion into an enumeration must give a value in it, or it is a conversion error: a cast you write, and in C an integer stored into an enumeration without a cast. A value in the range need not be an enumerator: (enum color)3 is fine. C itself lets an enumeration hold any value of an integer type the compiler picks for it, so this rule is stricter than C, and it is the same in both modes.

#include <cerastes.h>

enum color { RED, GREEN, BLUE };

enum color from_int(int x)
    CERASTES_REQUIRES(0 <= x && x <= 3)
    CERASTES_ENSURES(r, (int)r == x)
{
  return (enum color)x;
}

int weight(enum color c)
    CERASTES_ENSURES(r, r == (c == RED ? 10 : c == GREEN ? 20 : c == BLUE ? 30 : 0))
{
  switch (c) {
  case RED:
    return 10;
  case GREEN:
    return 20;
  case BLUE:
    return 30;
  }
  return 0;
}

int is_red(enum color c)
    CERASTES_ENSURES(r, r == (c == RED))
{
  if (c == RED) {
    return 1;
  }
  return 0;
}

Without the requires, the cast may not give one of the values:

#include <cerastes.h>

enum color { RED, GREEN, BLUE };

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

An enumerator is its value. In C an enumerator is an int and in C++ it has the enumeration’s type, but because every value of an enumeration lies in the range of int, comparing with == and !=, a switch, and storing an enumeration value into an integer variable, argument or result mean the same in both languages, and so does arithmetic on enumerators (GREEN + 1). An enumerator’s initializer is checked as you wrote it, like a named constant’s: enum { S = (signed char)300 }; is a conversion error at its line.

Arithmetic on an enumeration value is where the two languages part: C computes c - 1 in unsigned int for enum color (so 0 - 1 is the largest unsigned int), C++ in int (so it is -1). cerastes therefore rejects an enumeration value that the compiler converts to an integer for arithmetic, for a unary operator, for a shift or for an arm of ?:. Write the conversion yourself ((int)c - 1) to say which you mean. Compound assignment, ++ and -- on an enumeration are rejected too.

The order of two values of the same enumeration can be compared (<, ⇐, >, >=), and so can a value and one of its enumerators: both languages compare the same two integers. Comparing the order of an enumeration value with any other integer is rejected, even with a constant: C compares c < -1 in unsigned int for enum color, where it is true, and C++ in int, where it is false. Write the conversion ((int)c < 2). A C++ enum class has no implicit conversions; its values can be compared with each other, including with <.

#include <cerastes.h>

enum color { RED, GREEN, BLUE };

int warm(enum color c)
    CERASTES_ENSURES(r, r == (c < BLUE ? 1 : 0))
{
  if (c < BLUE) {
    return 1;
  }
  return 0;
}

int ordered(enum color a, enum color b)
    CERASTES_ENSURES(r, r == (a <= b ? 1 : 0))
{
  if (a <= b) {
    return 1;
  }
  return 0;
}

A switch on an enumeration is held to the two rules of the compilers' -Wswitch warning, which -Wall turns on: every case value must be the value of one of the enumeration’s enumerators, and a switch without default must have a case for every enumerator. The language allows both, but such a switch is almost always a mistake, and both clang and GCC refuse it under -Werror. cerastes rejects it at the case label, or at the switch for a missing enumerator:

#include <cerastes.h>

enum color { RED, GREEN, BLUE };

int classify(enum color c)
{
  switch (c) {
  case RED:
    return 1;
  case 4:
    return 2;
  default:
    return 0;
  }
}