Если вы вычисляете размер буфера из 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).