Detect Overflows in Buffer Size Computation
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); }
Create a Polyspace® project and add
display.c
to the project.On the Configuration pane, select the following options:
Target & Compiler: From the Target processor type drop-down list, select a type with 16-bit
int
such asc167
.Check Behavior: From the Overflow mode for unsigned integer drop-down list, select
allow
.
Run the verification and 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 thefor
loop.This error follows from an earlier error. For a 16-bit
int
, there is an overflow on the computationnum_items * sizeof(int)
. Polyspace does not detect the overflow because it occurs in computation withunsigned
integers. Instead Polyspace wraps the result of the computation causing the Illegally dereferenced pointer error later.From the Overflow mode for unsigned integer drop-down list, select
forbid
.Polyspace detects a red Overflow error in the computation
num_items * sizeof(int)
.