source: CIVL/mods/dev.civl.com/examples/mem/readset/structComplex2.cvl@ 8553be8

#include<mem.cvh>
struct S {      
  int a[10][10];
};

int main() {
  struct T {
   struct S s[10][10];
  } t[10][10];
  int x = 1;

  $read_set_push();
  t[0][x].s[2][3].a[4][5] = t[1][2].s[3][4].a[5][6];
  $mem m = $read_set_pop();
  $mem oracle = ($mem)&t[1][2].s[3][4].a[5][6];

  oracle = $mem_union(oracle, ($mem)&x);
  $assert($mem_equals(m, oracle));
}