Если вы вычисляете размер буфера от unsigned целые числа, для опции Overflow mode for unsigned integer, вместо значения по умолчанию allow, используйте forbid. Используя эту опцию помогает вам обнаружить переполнение на буферном этапе расчета. В противном случае вы можете видеть ошибку позже из-за недостаточного буфера. Эта опция доступна на узле Check Behavior под Code Prover Verification в панели Configuration.
В данном примере сохраните следующий код С в файле 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);
}Создайте проект Polyspace® и добавьте display.c к проекту.
На панели Configuration выберите следующие опции:
Target & Compiler: От Target processor type выпадающий список выберите тип с 16-битным int такой как c167.
Check Behavior: От Overflow mode for unsigned integer выпадающий список выберите allow.
Запустите верификацию и откройте результаты.
Polyspace обнаруживает оранжевую ошибку Illegally dereferenced pointer на линии array[ctr] = get_value() и красная ошибка Non-terminating loop на for цикл.
Эта ошибка следует из более ранней ошибки. Для 16-битного int, существует переполнение на расчете num_items * sizeof(int). Polyspace не обнаруживает переполнение, потому что это происходит в расчете с unsigned целые числа. Вместо этого Polyspace переносит результат расчета, вызывающего ошибку Illegally dereferenced pointer позже.
От Overflow mode for unsigned integer выпадающий список выберите forbid.
Polyspace обнаруживает красную ошибку Overflow в расчете num_items * sizeof(int).