source: CIVL/examples/mem/mem_tests/mem_havoc_complex.cvl

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

struct T {
  int a[10];
  double b[10][10];
  struct T * t;
};

int main() {
  struct T t;
  
  for (int i = 0; i < 10; i++) {
    t.a[i] = i;
    for (int j = 0; j < 10; j++) {
      t.b[i][j] = i*10 + j;
    }
  }
  
  $mem m = &t.a[0 .. 5];
  
  m = $mem_union(m, &t.b[0..5][0..5]);
  $mem_havoc(m);
  $assert(t.a[6] == 6);
  $assert(t.b[6][0] == 60);
  t.t = (struct T *)malloc(sizeof(struct T));

  t.t->a[0] = 0;
  t.t->a[6] = 6;
  m = $mem_union(m, &t.t->a[0..5]);
  $mem_havoc(m);
  $assert(t.t->a[6] == 6);
  free(t.t);
}