source: CIVL/examples/mem/mem_tests/mem_havoc_malloced.cvl@ cc8e265

#include<mem.cvh>
#include<stdlib.h>

int main() {
  int *a = (int*)malloc(sizeof(int) * 10);
  $mem m = &a[1 .. 5];

  for (int i = 0; i < 10; i++)
    a[i] = i;

  $mem_havoc(m);
  
  $assert(a[0] == 0);
  $assert(a[6] == 6);
  free(a);
}