При вычислении размера буфера из unsigned целые числа для параметра «Режим переполнения для целочисленных без знака» вместо значения по умолчанию allow, использовать forbid. Использование этой опции помогает обнаружить переполнение на этапе вычисления буфера. В противном случае позднее может появиться ошибка из-за недостатка буфера. Эта опция доступна в узле Проверить поведение (Check Behavior) в разделе Проверка проверочного кода (Code Prover Verification) на панели Конфигурация (Configuration).
Для этого примера сохраните следующий код C в файле 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 обнаружена оранжевая ошибка указателя «Незаконно» array[ctr] = get_value() и красная ошибка цикла Non-terminating в for цикл.
Эта ошибка вытекает из более ранней ошибки. Для 16-битного int, имеется переполнение в вычислениях num_items * sizeof(int). Polyspace не обнаруживает переполнение, поскольку оно происходит при вычислении с помощью unsigned целые числа. Вместо этого Polyspace переносит результат вычисления, вызвав ошибку указателя «Незаконно» позже.
В раскрывающемся списке Overflow mode for unsigned integer выберите forbid.
Polyspace обнаруживает красную ошибку переполнения в вычислениях num_items * sizeof(int).