Constructs

This page describes the verification constructs that ESBMC supports. These can be used in harness files to aid with the verification of ESBMC.

Non-Deterministic Functions

nondet_X() where X is a primitive C data type. This will mark the variable as non-deterministic, meaning it can have any value.

In this example, ESBMC will find a verification failed outcome because x is marked as being able to hold any value:

#include <assert.h>
int main() {
    unsigned int x = nondet_uint();
    assert(x < 10);
    return 0;
}

Assert and Assume

__ESBMC_assert(cond, reason) can be used instead of assert(), this brings the benefit of not needing to use #include <assert.h>.

int main() {
    unsigned int x = nondet_uint();
    __ESBMC_assert(x < 10, "X needs to be less than 10.");
    return 0;
}

__ESBMC_assume(int) can be used to narrow down the possible values of x. In this case the verification will succeed because it narrows the possible values of x to be less than 5.

#include <assert.h>
int main() {
    unsigned int x = nondet_uint();
    __ESBMC_assume(x < 5);
    assert(x < 10);
    return 0;
}

Ensure and Requires

The constructs __ESBMC_ensure(...), __ESBMC_requires(...), __ESBMC_return_value and __ESBMC_old(...) are detailed in the Function Contracts article.

Pragma Utils

The verification paramters can be modified using #pragma keyword. The following constructs are made available.

Unroll

Unroll can be used to set the loop unwind bound for a loop. This is equivalent to using --unwindset id:bound where id is the loop ID and bound is N. This inlining however, allows us to specify the paramter in a more stable manner as the id won’t shift as the code changes. It also frees us from needing to specify the loop bound when invoking ESBMC.

#pragma unroll [N] sets the next loop to be unwinded N times. In the following example, the loop will be unwound 80 times max.

int main() {
    unsigned int x = nondet_uint();
    __ESBMC_assume(x > 50 && x < 100);
    unsigned int y = 0;
    #pragma unroll 80
    for (int i = x - 1; x >= 0; x--) {
        y += x;
    }
    assert(y > 100);
    return 0;
}

You can also use #pragma unroll without N to make the loop unroll fully in the cases where --unwind is set. In this example, the loop will unroll fully regardless of the global unwind bound set.

int main() {
    unsigned int x = nondet_uint();
    __ESBMC_assume(x > 50 && x < 100);
    #pragma unroll
    for (int i = x - 1; x >= 0; x--) {
        y += x;
    }
    assert(y > 100);
    return 0;
}

N can also specified as a #define macro, however, if a value isn’t found, it will throw a parsing error.

#define LOOP_BOUND 80
int main() {
    unsigned int x = nondet_uint();
    __ESBMC_assume(x > 50 && x < 100);
    #pragma unroll LOOP_BOUND
    for (int i = x - 1; x >= 0; x--) {
        y += x;
    }
    assert(y > 100);
    return 0;
}