Exponenta Banner

Out of bounds array index

К массиву получают доступ вне области значений

расширьте все на странице

Описание

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

Примеры

развернуть все

#include <stdio.h>

void fibonacci(void)
{
  int i;
  int fib[10];
 
  for (i = 0; i < 10; i++) 
  {
    if (i < 2) 
      fib[i] = 1;
    else 
      fib[i] = fib[i-1] + fib[i-2];
    }

  printf("The 10-th Fibonacci number is %i .\n", fib[i]);   
}

int main(void) {
  fibonacci();
}

В этом примере, массив fib присвоен размер 10. Индекс массива для fib позволил значения [0,1,2..., 9]. Переменная i имеет значение 10, когда оно выходит из for- цикл. Поэтому, когда printf оператор пытается получить доступ к fib[10] через i, проверка Out of bounds array index производит красную ошибку.

Проверка также производит красную ошибку если printf использование *(fib+i) вместо fib[i].

Коррекция — Сохраняет индекс массива меньше, чем размер массивов

Одна возможная коррекция должна распечатать fib[i-1] вместо fib[i] после for- цикл. 

#include <stdio.h>

void fibonacci(void)
{
  int i;
  int fib[10];
 
  for (i = 0; i < 10; i++) 
  {
    if (i < 2) 
      fib[i] = 1;
    else 
      fib[i] = fib[i-1] + fib[i-2];
    }

  printf("The 10-th Fibonacci number is %i .\n", fib[i-1]);   
}

int main(void) {
  fibonacci();
}
extern int arr[];

int getFifthElement(void) {
   return arr[5];
}
int main(void){
	getFifthElement();
}

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

Чтобы удалить это предположение по умолчанию, используйте опцию -consider-external-array-access-unsafe. При использовании этой опции проверка Out of bounds array index является оранжевой.

extern int arr[];

int getFifthElement(void) {
   return arr[5];
}

Проверяйте информацию

Группа: Статическая память
Язык: C | C++
Акроним: OBAI

Смотрите также

|

Темы

Документация Polyspace Code Prover

Поддержка