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

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].

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

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];
}

int arr[10];

int main(int arg, char* argv[]) {
    int *ptr = &arr[10];
    int val_ptr = *ptr;
    return 0;
}

In this example, the pointer ptr is assigned an address past the memory allocated for the array arr. However, this assignment does not trigger the Out of bounds array index check. Instead, an Illegally dereferenced pointer check occurs only when the pointer is dereferenced and this check shows a definite error (red).