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

Use-After-Free

There are 2 general ways this can happen:

1. Runs alright but returns a random value

#include <stdio.h>
#include <stdlib.h>

int main() {
  int *a = malloc(sizeof(int));
  if (a != NULL) {
    *a = 1;
    int *b = a;
    free(b); // detects the free even when the pointer is aliased to b
    return *a; // use after ‘free’ of ‘a’
  }
  return 0;
}

Output:

2. First couple values are somewhat random and the last six are left at a set value

#include<stdio.h>
#include<stdlib.h>

int main() {
  int* a = malloc(10*sizeof(int));
  for(int i = 0; i < 10; i++) {
    a[i] = 0xff;
  }

  free(a);

  for(int i = 0; i < 10; i++) {
    printf("%d ", a[i]); // use after free
  }
  printf("\n");
  return 0;
}

Output:

1530302590 5 1762123792 21939 255 255 255 255 255 255

Situation after Resolving this Issue
Goblint can detect Use-After-Free

@vandah
@EdinCitaku