ESBMC (Efficient SMT-Based Bounded Model Checker)

ESBMC is a bounded model checker for embedded ANSI-C software based on SAT Modulo Theories (SMT) solver. It allows the verification engineer (i) to verify single- and multi-threaded software (with shared variables and locks); (ii) to reason about arithmetic under- and overflow, pointer safety, array bounds, atomicity and order violations, deadlock, data race, and user-specified assertions; (iii) to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic. ESBMC does not require the user to annotate the programs with pre/post-conditions. The distribution is split into three directories:

- bin
- licenses

The directory "bin" contains the binary file of ESBMC.

**** Tool usage ****

1 - To run ESBMC for a single C program, you should first set the environment variable PATH in your .bashrc file as follows:

"export PATH=$PATH:/home/lucas/esbmc/bin/

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

"$ esbmc file.c"

3 - In order to support the checking of arithmetic under- and overflow, memory leak, data race, and atomicity violation (which are 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 --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"		//check for out-of-bounds array indexing
"$ esbmc file_name.c --no-pointer-check"	//check for NULL-pointer dereferencing
"$ esbmc file_name.c --no-div-by-zero-check"	//check for divisions by zero

4 - 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.

5 - 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 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.

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

"$ esbmc file_name.c --function fun_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);
}


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

"$ esbmc --help".
