Current situation
Goblint currently cannot find/analyze undefined behavior like:

-Array-Bounds (Index out of bounds access; Source: https://www.geeksforgeeks.org/accessing-array-bounds-ccpp/ )

There are 2 general ways this can happen:

1. Access non allocated location of memory: The program can access some piece of memory which is owned by it:

// Program to demonstrate 
// accessing array out of bounds
#include <stdio.h>
int main()
{
    int arr[] = {1,2,3,4,5};
    printf("arr [0] is %d\n", arr[0]);
      
    // arr[10] is out of bound
    printf("arr[10] is %d\n", arr[10]);
    return 0;
}

Output :

arr [0] is 1
arr[10] is -1786647872

2. Segmentation fault: The program can access some piece of memory which is not owned by it, which can cause crashing of program such as segmentation fault

// Program to demonstrate 
// accessing array out of bounds
#include <stdio.h>
int main()
{
    int arr[] = {1,2,3,4,5};
    printf("arr [0] is %d\n",arr[0]);
    printf("arr[10] is %d\n",arr[10]);
      
    // allocation memory to out of bound 
    // element
    arr[10] = 11;
    printf("arr[10] is %d\n",arr[10]);
    return 0;
}

Output :
Runtime Error : Segmentation Fault (SIGSEGV)

Situation after Resolving this Issue
Goblint can detect this undefined Behavior. This will be optional.

@vandah
@EdinCitaku