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

#include<mem.cvh>

int a[10][10];

int main() {
  $mem m = &a[0][0 .. 3];
  
  m = $mem_union_widening(m, &a[0][4 .. 6]);
  /* If a set of references have diference in only one dimension, and
     ranges in every reference can be connected, the default widening
     operator will combine them precisely
   */
  $assert($mem_contains(m, &a[0][0 .. 6]));
  $assert(!$mem_contains(m, &a[0][7]));
  $assert(!$mem_contains(m, &a[1][0 .. 6]));
  
  m = &a[0 .. 3][1 .. 8];
  m = $mem_union_widening(&a[4 .. 6][1 .. 8], m);
  m = $mem_union_widening(&a[7 .. 8][1 .. 8], m);
  $assert($mem_contains(m, &a[0 .. 8][1 .. 8]));
  $assert(!$mem_contains(m, &a[9][1 .. 8]));
  $assert(!$mem_contains(m, &a[0 .. 6][0]));  

  /* if not all connected, the default widening operator will result
   *  in a reference that refers to the whole dimension
   */
  m = &a[0 .. 3][1 .. 8];
  m = $mem_union_widening(&a[5 .. 6][1 .. 8], m);
  $assert($mem_contains(m, &a[0 .. 6][1 .. 8]));
  $assert($mem_contains(m, &a[0 .. 9][1 .. 8]));
  $assert(!$mem_contains(m, &a[0 .. 3][0]));  

  /*If a set of references have diference in more than one dimensions,
    the default widening operator will result in a reference that
    refers to the whole multiple dimensional array*/
  m = &a[0 .. 3][0 .. 3];
  m = $mem_union_widening(&a[4 .. 6][4 .. 6], m);
  $assert($mem_contains(m, &a));
}