ESBMC (Efficient SMT-Based Context-Bounded Model Checker)
line decor
line decor

DOCUMENTATION
 

How to install ESBMC

In order to install ESBMC on your machine, you should download the archive (e.g., esbmc-v1.21-linux-64-static.tgz) and save it on your disk. After that, you should type the following command:

$tar xfz esbmc-v1.21-linux-64-static.tgz

The ESBMC distribution is split into three directories:

- bin

- smoke-tests

- licenses

The directory bin contains the binary file of ESBMC. The directory smoke-tests contains some ANSI-C programs and also includes a shell script that can be used to collect experimental results for different ANSI-C benchmarks (e.g., check the encoding time, decision procedure time, total number of lines of code, total number of properties to be verified, how many properties passed, violated and failed during the verification process).

In order to run the examples located at the directory smoke-tests, you should type the following command:

$./run_experiments.sh

The makefile inside the directory smoke-tests can also serve as an example to use the goto-cc tool (http://www.cprover.org/goto-cc/) in order to compile C/C++ programs into equivalent GOTO-programs. The directory licenses contains the ESBMC, CProver, Z3 and Boolector licenses.

How to run ESBMC

1 - To run ESBMC for a single C program, e.g., crc.c located at the directory smoke-tests, you should first set the environment variable PATH in your .bashrc file as follows:

export PATH=$PATH:$HOME/esbmc-v1.21/bin/

2 - After that, you can run ESBMC from the command line by calling:

$esbmc crc.c

3 - If you want to model check the GOTO files generated by the goto-cc tool (after you type "$ make" inside the directory "smoke-tests"), then you should enter:

$esbmc --binary crc

4 - In order to support the checking of arithmetic under- and overflow, memory leak, data race, deadlock-check and atomicity violation (which are all disabled by default), you should type:

$esbmc file_name.c --overflow-check //check for arithmetic under- and overflow

$esbmc file_name.c --memory-leak-check //check for memory leaks

$esbmc file_name.c --data-races-check //check for data race conditions

$esbmc file_name.c --deadlock-check //check for deadlock

$esbmc file_name.c --atomicity-check //check for atomicity violations at visible statements

ESBMC enables by default the checking of array bounds, division by zero, and pointer safety, which can also be disabled via command line by typing:

$esbmc file_name.c --no-bounds-check //does not check for out-of-bounds array indexing

$esbmc file_name.c --no-pointer-check //does not check for NULL-pointer dereferencing

$esbmc file_name.c --no-div-by-zero-check //does not check for divisions by zero

5 - If your program calls functions from other libraries, you can set the path of the libraries by typing:

$esbmc file_name.c -I pathA -I pathB -I pathN

where path1 means the path of library A, path2 means the path of library B, and so on.

6 - If ESBMC does not detect automatically the bounds of the program, then you can enter:

$esbmc --unwind 36 fir_new.c

where 36 is the maximum number of the loop unwinding bound. Note that if ESBMC reports unwinding loop assertions, it means that the property holds until this bound. You can thus increase the number of the bound until ESBMC proves that the property holds or the SMT solver explodes.

7 - ESBMC is also able to check each function of your C program individually by typing:

$esbmc file_name.c --function func_name

where fun_name is the name of your C function. As example, consider the sqrt function of the fir_new.c program:

static float sqrt(float val) {

val = nondet_float(); //assign a non-deterministic value to the variable val

__ESBMC_assume(val>0 && val<1000);

float x = val/10;

float dx;

double diff;

double min_tol = 0.00001;

int i, flag;

flag = 0;

if (val == 0 ) x = 0;

else {

for (i=1;i<20;i++) {

if (!flag) {

dx = (val - (x*x)) / (2.0 * x);

x = x + dx;

diff = val - (x*x);

if (fabs(diff) <= min_tol) flag = 1;

}

else

x =x;

}

}

return (x);

}

In order to allow ESBMC to verify this C function, we assign a non-deterministic value to the variable val (e.g., val=nondet_float()). If the sqrt function is only called with deterministic values, we can thus use the function __ESBMC_asume(expr) to limit the possible values of the variable val (e.g., __ESBMC_assume(val>0 && val<1000)). However, if your C function contains pointer as argument, then you should explicitly allocate and initialize the block of memory to that pointer, as follows:

float fir_filter(float input,float *coef,int n,float *history) {

input=nondet_float(); // non-deterministic input

coef = fir_lpf35; // fir_lp35 is an array of constants used by the filter

n=35; // number of coeficients

history = (float *) malloc(sizeof(float)*35); //allocate an array of 35 elements

memset (history,0,35); // initialize memory block

int i;

float *hist_ptr,*hist1_ptr,*coef_ptr;

float output;

hist_ptr = history;

hist1_ptr = hist_ptr; /* use for history update */

coef_ptr = coef + n - 1; /* point to last coef */

/* form output accumulation */

output = *hist_ptr++ * (*coef_ptr--);

#ifdef DEBUG

if (n > Cnt2) Cnt2 = n;

#endif

for(i = 2 ; i < n ; i++) {

*hist1_ptr++ = *hist_ptr; /* update history array */

output += (*hist_ptr++) * (*coef_ptr--);

}

output += input * (*coef_ptr); /* input tap */

*hist1_ptr = input; /* last history */

return(output);

}

8 - ESBMC is able to model check multi-threaded C programs. If you want to bound the total number of context-switches, you should type:

$esbmc file_name.c --context-switch nr

where nr indicates the total number of allowed context-switches.

To check all available options of the ESBMC tool, type:

$esbmc --help

We are still increasing the robustness of ESBMC tool and also implementing new features (e.g., support for verifying concurrent software), more optimizations and experiencing new encodings. For any question about ESBMC, contact esbmc@ecs.soton.ac.uk.