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