Просмотрите и исправьте проверки индекса за пределами массива

Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Out of bounds array index. Существует несколько способов исправить проверку. Для получения описания примеров проверки и кода смотрите Out of bounds array index.

Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.

Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.

Шаг 1: Интерпретируйте информацию о проверке

Поместите курсор на [ символ.

Получите следующую информацию из подсказки:

  • Размер массива. Допустимая область значений для индекса массива - от 0 до (размер массива - 1).

  • Фактическая область значений для индекса массива

В предыдущем примере размер массива равен 10. Поэтому допустимая область значений для индекса массива составляет от 0 до 9. Однако фактическая область значений значений от 0 до 10.

Возможное исправление: Чтобы избежать выхода за пределы индекса массива, доступ к массиву возможен только в том случае, если индекс находится между 0 и (размер массива - 1).

#define SIZE 100
int arr[SIZE];
.
.
if(i<SIZE)
	val = arr[i]
else
	/*Error handling */

Шаг 2: Определите первопричину проверки

Если необходимо знать или изменить размер массива, щелкните правой кнопкой мыши переменную массива и выберите Go To Definition, если опция существует. В противном случае проследите поток данных, начиная с массива индексной переменной. Определите точку, в которой можно ограничить индексную переменную.

Чтобы проследить поток данных, выберите проверку и отметьте информацию на панели Result Details.

  • Если на панели Result Details отображается последовательность команд, ведущих к проверке, выберите каждую инструкцию.

  • Если на панели Result Details отображается номер линии вероятной причины проверки, щелкните правой кнопкой мыши на панели Source. Выберите Go To Line.

  • В противном случае:

    1. Найдите предыдущие образцы индексной переменной массива.

    2. Просмотрите эти образцы. Найдите образец, где вы ограничиваете индексную переменную массива (размер массива - 1).

      Возможное исправление: Если вы не находите образца, в которой вы ограничиваете индексную переменную, задайте ограничение для переменной. Для примера:

      if(index<SIZE)
      	read(array[index]);

    3. Определите, применяется ли ограничение к образцу, где происходит Out of bounds array index ошибка.

      Для примера можно ограничить индексную переменную в for цикл с использованием for(index=0; index<SIZE; index++). Однако вы получаете доступ к массиву за пределами цикла, где ограничение не применяется.

      Возможное исправление: Исследуйте, почему ограничение не применяется. Проверьте, нужно ли снова ограничивать индексную переменную.

    4. Если индексная переменная получена из другой переменной, проследите поток данных для второй переменной. Определите, ограничили ли вы эту вторую переменную (размер массива - 1).

В зависимости от переменной используйте следующие навигационные ярлыки для поиска предыдущих образцов. Можно выполнить следующие шаги только в пользовательском интерфейсе Polyspace.

ПеременнаяКак найти предыдущие образцы переменной

Локальная переменная

Используйте один из следующих методов:

  • Поиск переменной.

    1. Щелкните правой кнопкой мыши переменную. Выберите Search For All References.

      Все образцы переменной отображаются на панели Search с выделенным текущим образцом.

    2. На панели Search выберите предыдущие образцы.

  • Просмотрите исходный код.

    1. Дважды кликните переменную на панели Source.

      Все образцы переменной подсвечиваются.

    2. Прокрутка вверх, чтобы найти предыдущие образцы.

Глобальная переменная

Щелкните правой кнопкой мыши переменную. Если появляется Show In Variable Access View опция, переменная является глобальной переменной.

  1. Выберите Show In Variable Access View опции.

    На панели Variable Access отображается текущий образец переменной.

  2. На этой панели выберите предыдущие образцы переменной.

    Операции записи переменной обозначаются и считываются с.

Функция возврата значение

ret=func();

  1. Найдите определение функции.

    Щелкните правой кнопкой мыши func на панели Source. Выберите Go To Definition, если опция существует. Если определение недоступно для Polyspace, выбор опции приводит вас к объявлению функции.

  2. В определении func, идентифицируйте каждую return оператор. Переменная, которую возвращает функция, является вашей новой переменной, которую можно отследить назад.

Можно также определить, связаны ли переменные в любой операции с какой-либо предыдущей операцией. См. Раздел «Поиск отношений между переменными в коде».

Шаг 3: Проверьте общие причины проверки

Проверьте общие причины проверки Out of bounds array index.

  • Проверьте, запускаете ли вы индексную переменную массива с 0.

  • В условии, которое ограничивает индексную переменную массива, смотрите, используете ли вы <= когда вы намеревались использовать <.

  • Если возврат происходит в или сразу после for или while цикл, определите, нужно ли уменьшать количество запусков цикла.

  • Если вы используете sizeof функция для ограничения массива, смотрите, делите ли вы sizeof(array) по sizeof(array[0]) для получения размера массива.

    sizeof(array) возвращает размер массива в байтах.

Шаг 4: Проверка трассировки на допущение Polyspace

Посмотрите, можно ли проследить оранжевую проверку до допущения Polyspace, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.

Например, вы ограничиваете индекс массива с помощью функции, определение которой вы не предоставляете. Затем:

  1. Polyspace не может определить, что индексная переменная массива ограничена.

  2. Когда вы используете эту переменную в качестве индекса массива, может возникнуть Out of bounds array index ошибка.

  3. Если вы знаете, что переменная ограничена размером массива, добавьте комментарий и обоснование, описывающие, почему вы не изменили код.

Для получения дополнительной информации смотрите Допущения анализа Code Prover.

Примечание

Прежде чем обосновывать оранжевую проверку, внимательно рассмотрим, сможете ли вы улучшить свои проекты кодирования.

Например, ограничение глобальной переменной в одной функции и использование ее в качестве индекса массива во второй функции вызывает уязвимости в вашем коде. Если между двумя предыдущими функциями вызывается новая функция и изменяет вашу глобальную переменную, ограничение больше не применяется.