Detect Overflows in Buffer Size Computation

R2026b

If you are computing the size of a buffer from unsigned integers, for the Overflow mode for unsigned integer option, instead of the default value allow, use forbid. Using this option helps you detect an overflow at the buffer computation stage. Otherwise, you might see an error later due to insufficient buffer. This option is available on the Check Behavior node under Code Prover Verification in the Configuration pane.

For this example, save the following C code in a file display.c:

#include <stdlib.h>
#include <stdio.h>

int get_value(void);
 
void display(unsigned int num_items) {
 int *array;
 array = (int *) malloc(num_items * sizeof(int)); // overflow error
  if (array) {
    for (unsigned int ctr = 0; ctr < num_items; ctr++)     {       
      array[ctr] = get_value();
    }
    for (unsigned int ctr = 0; ctr < num_items; ctr++)     {       
      printf("Value is %d.\n", ctr, array[ctr]);
    }
    free(array);
  }
}

void main() {
  display(33000);
}

1. Start a Polyspace^® Code Prover™ analysis using this command:

   polyspace-code-prover -sources display.c -target c-167

   This command starts a Polyspace Code Prover analysis assuming a c-167 target. This target uses 16-bit integers.

2. After the analysis ends, open the results.

   Polyspace detects an orange Illegally dereferenced pointer error on the line array[ctr] = get_value() and a red Non-terminating loop error on the for loop.

   This error follows from an earlier error. For a 16-bit int, there is an overflow on the computation num_items * sizeof(int). Polyspace does not detect the overflow because it occurs in computation with unsigned integers. Instead Polyspace wraps the result of the computation causing the Illegally dereferenced pointer error later.

3. Change the value of the option Overflow mode for unsigned integer to forbid and run a second analysis:

   polyspace-code-prover -sources display.c -target c-167 -unsigned-integer-overflows forbid 

   Polyspace detects a red Overflow error in the computation num_items * sizeof(int).