Out of bounds array index

Array is accessed outside range

Description

This check on an array element access determines whether the element is outside the array range. The check occurs only when you read an array element using the index notation and not when you take the address of the array element.

Diagnosing This Check

Review and Fix Out of Bounds Array Index Checks

Examples

Array index is equal to array size

#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();
}

In this example, the array fib is assigned a size of 10. An array index for fib has allowed values of [0,1,2,...,9]. The variable i has a value 10 when it comes out of the for-loop. Therefore, when the printf statement attempts to access fib[10] through i, the Out of bounds array index check produces a red error.

The check also produces a red error if printf uses *(fib+i) instead of fib[i].

Correction — Keep array index less than array size

One possible correction is to print fib[i-1] instead of fib[i] after the for-loop.

#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();
}

Accessing external arrays with undefined size

extern int arr[];

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

Code Prover assumes by default that external arrays of undefined size can be safely accessed at any index. The Out of bounds array index check on the external array access is green.

To remove this default assumption, use the option -consider-external-array-access-unsafe. With this option, the Out of bounds array index check is orange.

extern int arr[];

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

Check Information

Group: Static memory

Language: C | C++

Acronym: OBAI