[alias] print graphs in tests

src/plugins/alias/tests/basic/oracle/switch2.res.oracle

@@ -2,20 +2,39 @@
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *a = (int *)0;  is    <empty>
 [alias] analysing instruction: int *b = (int *)0;
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *b = (int *)0;  is    <empty>
 [alias] analysing instruction: int *c = (int *)0;
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *c = (int *)0;  is    <empty>
 [alias] analysing instruction: int *d = (int *)0;
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *d = (int *)0;  is    <empty>
 [alias] analysing instruction: int e = 0;
 [alias] May-aliases after instruction  int e = 0;  are  <none>
+[alias] May-alias graph after instruction  int e = 0;  is    <empty>
 [alias] analysing instruction: case 1: a = d;
 [alias] May-aliases after instruction  case 1: a = d;  are  { a; d }
+[alias] May-alias graph after instruction  case 1: a = d;  is
+  0:{ a; d } → 1:{  }
 [alias] analysing instruction: case 2: b = d;
 [alias] May-aliases after instruction  case 2: b = d;  are  { b; d }
+[alias] May-alias graph after instruction  case 2: b = d;  is
+  4:{ b; d } → 5:{  }
 [alias] analysing instruction: default: c = d;
 [alias] May-aliases after instruction  default: c = d;  are  { c; d }
+[alias] May-alias graph after instruction  default: c = d;  is
+  8:{ c; d } → 9:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b; c; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; b; c; d } → 1:{  }
 [alias] May-aliases at the end of function main: { a; b; c; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b; c; d } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  d  e  __retres    returns: __retres
+  state: { a; b; c; d }
+[alias] Analysis complete

src/plugins/alias/tests/basic/oracle/while_for1.res.oracle

 [kernel] Parsing while_for1.c (with preprocessing)
 [alias] analysing function: _Exit
 [alias] May-aliases at the end of function _Exit: ⊥
+[alias] May-alias graph at the end of function _Exit:
+  ⊥
 [alias] analysing function: abort
 [alias] May-aliases at the end of function abort: ⊥
+[alias] May-alias graph at the end of function abort:
+  ⊥
 [alias] analysing function: abs
 [alias] May-aliases at the end of function abs: ⊥
+[alias] May-alias graph at the end of function abs:
+  ⊥
 [alias] analysing function: at_quick_exit
 [alias] May-aliases at the end of function at_quick_exit: ⊥
+[alias] May-alias graph at the end of function at_quick_exit:
+  ⊥
 [alias] analysing function: atexit
 [alias] May-aliases at the end of function atexit: ⊥
+[alias] May-alias graph at the end of function atexit:
+  ⊥
 [alias] analysing function: atof
 [alias] May-aliases at the end of function atof: ⊥
+[alias] May-alias graph at the end of function atof:
+  ⊥
 [alias] analysing function: atoi
 [alias] May-aliases at the end of function atoi: ⊥
+[alias] May-alias graph at the end of function atoi:
+  ⊥
 [alias] analysing function: atol
 [alias] May-aliases at the end of function atol: ⊥
+[alias] May-alias graph at the end of function atol:
+  ⊥
 [alias] analysing function: atoll
 [alias] May-aliases at the end of function atoll: ⊥
+[alias] May-alias graph at the end of function atoll:
+  ⊥
 [alias] analysing function: bsearch
 [alias] May-aliases at the end of function bsearch: ⊥
+[alias] May-alias graph at the end of function bsearch:
+  ⊥
 [alias] analysing function: calloc
 [alias] May-aliases at the end of function calloc: ⊥
+[alias] May-alias graph at the end of function calloc:
+  ⊥
 [alias] analysing function: div
 [alias] May-aliases at the end of function div: ⊥
+[alias] May-alias graph at the end of function div:
+  ⊥
 [alias] analysing function: drand48
 [alias] May-aliases at the end of function drand48: ⊥
+[alias] May-alias graph at the end of function drand48:
+  ⊥
 [alias] analysing function: erand48
 [alias] May-aliases at the end of function erand48: ⊥
+[alias] May-alias graph at the end of function erand48:
+  ⊥
 [alias] analysing function: exit
 [alias] May-aliases at the end of function exit: ⊥
+[alias] May-alias graph at the end of function exit:
+  ⊥
 [alias] analysing function: free
 [alias] May-aliases at the end of function free: ⊥
+[alias] May-alias graph at the end of function free:
+  ⊥
 [alias] analysing function: getenv
 [alias] May-aliases at the end of function getenv: ⊥
+[alias] May-alias graph at the end of function getenv:
+  ⊥
 [alias] analysing function: jrand48
 [alias] May-aliases at the end of function jrand48: ⊥
+[alias] May-alias graph at the end of function jrand48:
+  ⊥
 [alias] analysing function: labs
 [alias] May-aliases at the end of function labs: ⊥
+[alias] May-alias graph at the end of function labs:
+  ⊥
 [alias] analysing function: lcong48
 [alias] May-aliases at the end of function lcong48: ⊥
+[alias] May-alias graph at the end of function lcong48:
+  ⊥
 [alias] analysing function: ldiv
 [alias] May-aliases at the end of function ldiv: ⊥
+[alias] May-alias graph at the end of function ldiv:
+  ⊥
 [alias] analysing function: llabs
 [alias] May-aliases at the end of function llabs: ⊥
+[alias] May-alias graph at the end of function llabs:
+  ⊥
 [alias] analysing function: lldiv
 [alias] May-aliases at the end of function lldiv: ⊥
+[alias] May-alias graph at the end of function lldiv:
+  ⊥
 [alias] analysing function: lrand48
 [alias] May-aliases at the end of function lrand48: ⊥
+[alias] May-alias graph at the end of function lrand48:
+  ⊥
 [alias] analysing function: main
 [alias] analysing instruction: int *s = (int *)0;
 [alias] May-aliases after instruction  int *s = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *s = (int *)0;  is    <empty>
 [alias] analysing instruction: int idx = 0;
 [alias] May-aliases after instruction  int idx = 0;  are  <none>
+[alias] May-alias graph after instruction  int idx = 0;  is    <empty>
 [alias] analysing instruction: s = (int *)malloc((size_t)idx);
 [alias] May-aliases after instruction  s = (int *)malloc((size_t)idx);  are  <none>
+[alias] May-alias graph after instruction  s = (int *)malloc((size_t)idx);  is
+  0:{ s } → 1:{  }
 [alias] analysing instruction: idx ++;
 [alias] May-aliases after instruction  idx ++;  are  <none>
+[alias] May-alias graph after instruction  idx ++;  is    0:{ s } → 1:{  }
 [alias] analysing instruction: s = (int *)malloc((size_t)idx);
 [alias] May-aliases after instruction  s = (int *)malloc((size_t)idx);  are  <none>
+[alias] May-alias graph after instruction  s = (int *)malloc((size_t)idx);  is
+  0:{ s } → 1:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is    0:{ s } → 1:{  }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  0:{ s } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: s  idx  __retres    returns: __retres    state: <none>
 [alias] analysing function: malloc
 [alias] May-aliases at the end of function malloc: ⊥
+[alias] May-alias graph at the end of function malloc:
+  ⊥
 [alias] analysing function: mblen
 [alias] May-aliases at the end of function mblen: ⊥
+[alias] May-alias graph at the end of function mblen:
+  ⊥
 [alias] analysing function: mbstowcs
 [alias] May-aliases at the end of function mbstowcs: ⊥
+[alias] May-alias graph at the end of function mbstowcs:
+  ⊥
 [alias] analysing function: mbtowc
 [alias] May-aliases at the end of function mbtowc: ⊥
+[alias] May-alias graph at the end of function mbtowc:
+  ⊥
 [alias] analysing function: mkstemp
 [alias] May-aliases at the end of function mkstemp: ⊥
+[alias] May-alias graph at the end of function mkstemp:
+  ⊥
 [alias] analysing function: mkstemps
 [alias] May-aliases at the end of function mkstemps: ⊥
+[alias] May-alias graph at the end of function mkstemps:
+  ⊥
 [alias] analysing function: mrand48
 [alias] May-aliases at the end of function mrand48: ⊥
+[alias] May-alias graph at the end of function mrand48:
+  ⊥
 [alias] analysing function: nrand48
 [alias] May-aliases at the end of function nrand48: ⊥
+[alias] May-alias graph at the end of function nrand48:
+  ⊥
 [alias] analysing function: posix_memalign
 [alias] May-aliases at the end of function posix_memalign: ⊥
+[alias] May-alias graph at the end of function posix_memalign:
+  ⊥
 [alias] analysing function: putenv
 [alias] May-aliases at the end of function putenv: ⊥
+[alias] May-alias graph at the end of function putenv:
+  ⊥
 [alias] analysing function: qsort
 [alias] May-aliases at the end of function qsort: ⊥
+[alias] May-alias graph at the end of function qsort:
+  ⊥
 [alias] analysing function: quick_exit
 [alias] May-aliases at the end of function quick_exit: ⊥
+[alias] May-alias graph at the end of function quick_exit:
+  ⊥
 [alias] analysing function: rand
 [alias] May-aliases at the end of function rand: ⊥
+[alias] May-alias graph at the end of function rand:
+  ⊥
 [alias] analysing function: random
 [alias] May-aliases at the end of function random: ⊥
+[alias] May-alias graph at the end of function random:
+  ⊥
 [alias] analysing function: realloc
 [alias] May-aliases at the end of function realloc: ⊥
+[alias] May-alias graph at the end of function realloc:
+  ⊥
 [alias] analysing function: reallocarray
 [alias] May-aliases at the end of function reallocarray: ⊥
+[alias] May-alias graph at the end of function reallocarray:
+  ⊥
 [alias] analysing function: seed48
 [alias] May-aliases at the end of function seed48: ⊥
+[alias] May-alias graph at the end of function seed48:
+  ⊥
 [alias] analysing function: setenv
 [alias] May-aliases at the end of function setenv: ⊥
+[alias] May-alias graph at the end of function setenv:
+  ⊥
 [alias] analysing function: srand
 [alias] May-aliases at the end of function srand: ⊥
+[alias] May-alias graph at the end of function srand:
+  ⊥
 [alias] analysing function: srand48
 [alias] May-aliases at the end of function srand48: ⊥
+[alias] May-alias graph at the end of function srand48:
+  ⊥
 [alias] analysing function: srandom
 [alias] May-aliases at the end of function srandom: ⊥
+[alias] May-alias graph at the end of function srandom:
+  ⊥
 [alias] analysing function: strtod
 [alias] May-aliases at the end of function strtod: ⊥
+[alias] May-alias graph at the end of function strtod:
+  ⊥
 [alias] analysing function: strtof
 [alias] May-aliases at the end of function strtof: ⊥
+[alias] May-alias graph at the end of function strtof:
+  ⊥
 [alias] analysing function: strtol
 [alias] May-aliases at the end of function strtol: ⊥
+[alias] May-alias graph at the end of function strtol:
+  ⊥
 [alias] analysing function: strtold
 [alias] May-aliases at the end of function strtold: ⊥
+[alias] May-alias graph at the end of function strtold:
+  ⊥
 [alias] analysing function: strtoll
 [alias] May-aliases at the end of function strtoll: ⊥
+[alias] May-alias graph at the end of function strtoll:
+  ⊥
 [alias] analysing function: strtoul
 [alias] May-aliases at the end of function strtoul: ⊥
+[alias] May-alias graph at the end of function strtoul:
+  ⊥
 [alias] analysing function: strtoull
 [alias] May-aliases at the end of function strtoull: ⊥
+[alias] May-alias graph at the end of function strtoull:
+  ⊥
 [alias] analysing function: system
 [alias] May-aliases at the end of function system: ⊥
+[alias] May-alias graph at the end of function system:
+  ⊥
 [alias] analysing function: unsetenv
 [alias] May-aliases at the end of function unsetenv: ⊥
+[alias] May-alias graph at the end of function unsetenv:
+  ⊥
 [alias] analysing function: wcstombs
 [alias] May-aliases at the end of function wcstombs: ⊥
+[alias] May-alias graph at the end of function wcstombs:
+  ⊥
 [alias] analysing function: wctomb
 [alias] May-aliases at the end of function wctomb: ⊥
+[alias] May-alias graph at the end of function wctomb:
+  ⊥
+[alias] Analysis complete

src/plugins/alias/tests/basic/oracle/while_for2.res.oracle

@@ -2,12 +2,23 @@
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *a = (int *)0;  is    <empty>
 [alias] analysing instruction: int *b = (int *)0;
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *b = (int *)0;  is    <empty>
 [alias] analysing instruction: int *c = (int *)0;
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *c = (int *)0;  is    <empty>
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  { a; b }
+[alias] May-alias graph after instruction  a = b;  is    0:{ a; b } → 1:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b }
+[alias] May-alias graph after instruction  __retres = 0;  is    0:{ a; b } → 1:{  }
 [alias] May-aliases at the end of function main: { a; b }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  __retres    returns: __retres
+  state: { a; b }
+[alias] Analysis complete

src/plugins/alias/tests/basic/oracle/while_for3.res.oracle

@@ -2,18 +2,32 @@
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *a = (int *)0;  is    <empty>
 [alias] analysing instruction: int *b = (int *)0;
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *b = (int *)0;  is    <empty>
 [alias] analysing instruction: int *c = (int *)0;
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *c = (int *)0;  is    <empty>
 [alias] analysing instruction: int i = 0;
 [alias] May-aliases after instruction  int i = 0;  are  <none>
+[alias] May-alias graph after instruction  int i = 0;  is    <empty>
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  { a; b }
+[alias] May-alias graph after instruction  a = b;  is    0:{ a; b } → 1:{  }
 [alias] analysing instruction: __Cont: i ++;
 [alias] May-aliases after instruction  __Cont: i ++;  are  { a; b }
+[alias] May-alias graph after instruction  __Cont: i ++;  is    0:{ a; b } → 1:{  }
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  { a; b }
+[alias] May-alias graph after instruction  a = b;  is    0:{ a; b } → 1:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b }
+[alias] May-alias graph after instruction  __retres = 0;  is    0:{ a; b } → 1:{  }
 [alias] May-aliases at the end of function main: { a; b }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  i  __retres    returns: __retres
+  state: { a; b }
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle

@@ -2,13 +2,34 @@
 [alias] analysing function: f
 [alias] analysing instruction: *y = t + (*y - *x);
 [alias] May-aliases after instruction  *y = t + (*y - *x);  are  { *y; t }
+[alias] May-alias graph after instruction  *y = t + (*y - *x);  is
+  0:{ y } → 1:{ *y; t }   1:{ *y; t } → 3:{  }
 [alias] analysing instruction: *z = t + (*z - *x);
 [alias] May-aliases after instruction  *z = t + (*z - *x);  are
   { *y; *z; t }  { y; z }
+[alias] May-alias graph after instruction  *z = t + (*z - *x);  is
+  0:{ y } → 5:{ *y; *z; t }   4:{ z } → 5:{ *y; *z; t }
+  5:{ *y; *z; t } → 3:{  }
 [alias] analysing instruction: *x = t;
 [alias] May-aliases after instruction  *x = t;  are  { *x; *y; *z; t }  { x; y; z }
+[alias] May-alias graph after instruction  *x = t;  is
+  0:{ y } → 7:{ *x; *y; *z; t }   4:{ z } → 7:{ *x; *y; *z; t }
+  6:{ x } → 7:{ *x; *y; *z; t }   7:{ *x; *y; *z; t } → 3:{  }
 [alias] May-aliases at the end of function f: { *x; *y; *z; t }  { x; y; z }
+[alias] May-alias graph at the end of function f:
+  0:{ y } → 7:{ *x; *y; *z; t }   4:{ z } → 7:{ *x; *y; *z; t }
+  6:{ x } → 7:{ *x; *y; *z; t }   7:{ *x; *y; *z; t } → 3:{  }
+[alias] Summary of function f:
+  formals: x→{ *x; *y; *z; t }  y→{ *x; *y; *z; t }  z→{ *x; *y; *z; t }
+  locals: t    returns: <none>    state: { *x; *y; *z; t }  { x; y; z }
 [alias] analysing function: g
 [alias] analysing instruction: f(a,a,a);
 [alias] May-aliases after instruction  f(a,a,a);  are  <none>
+[alias] May-alias graph after instruction  f(a,a,a);  is
+  15:{  } → 11:{  }   16:{ a } → 15:{  }
 [alias] May-aliases at the end of function g: <none>
+[alias] May-alias graph at the end of function g:
+  15:{  } → 11:{  }   16:{ a } → 15:{  }
+[alias] Summary of function g:
+  formals: a    locals:     returns: <none>    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle

@@ -2,14 +2,29 @@
 [alias] analysing function: main
 [alias] analysing instruction: short tmp_0 = (short)0;
 [alias] May-aliases after instruction  short tmp_0 = (short)0;  are  <none>
+[alias] May-alias graph after instruction  short tmp_0 = (short)0;  is    <empty>
 [alias] analysing instruction: *(& prev[1] + 0) = tmp_0;
 [alias] May-aliases after instruction  *(& prev[1] + 0) = tmp_0;  are  <none>
+[alias] May-alias graph after instruction  *(& prev[1] + 0) = tmp_0;  is    <empty>
 [alias] analysing instruction: prev[0] = (short)0;
 [alias] May-aliases after instruction  prev[0] = (short)0;  are  <none>
+[alias] May-alias graph after instruction  prev[0] = (short)0;  is    <empty>
 [alias] analysing instruction: p = & prev[1] + (int)*p;
 [alias] May-aliases after instruction  p = & prev[1] + (int)*p;  are  <none>
+[alias] May-alias graph after instruction  p = & prev[1] + (int)*p;  is
+  0:{ p } → 1:{ prev[0..] }
 [alias] analysing instruction: p = & prev[*p];
 [alias] May-aliases after instruction  p = & prev[*p];  are  <none>
+[alias] May-alias graph after instruction  p = & prev[*p];  is
+  4:{ p } → 5:{ prev[0..] }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ p } → 1:{ prev[0..] }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  0:{ p } → 1:{ prev[0..] }
+[alias] Summary of function main:
+  formals:     locals: __retres  prev  p→{ prev[0..] }  tmp_0
+  returns: __retres    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle

@@ -4,11 +4,22 @@
 [alias] analysing function: f
 [alias] analysing instruction: tmp = & f;
 [alias] May-aliases after instruction  tmp = & f;  are  <none>
+[alias] May-alias graph after instruction  tmp = & f;  is    0:{ tmp } → 1:{ f }
 [alias] analysing instruction: tmp = (void (*)(void))*((char *)(v.t));
 [alias:unsafe-cast] origin.c:8: Warning: unsafe cast from char to void (*)(void)
 [alias:unsafe-cast] origin.c:8: Warning: unsafe cast from int * to char *
 [alias] May-aliases after instruction  tmp = (void (*)(void))*((char *)(v.t));  are
   { v.t; tmp }
+[alias] May-alias graph after instruction  tmp = (void (*)(void))*((char *)(v.t));
+  is    0:{ v.t; tmp } → 1:{ f }
 [alias] analysing instruction: int g = (int)tmp;
 [alias] May-aliases after instruction  int g = (int)tmp;  are  { v.t; tmp }
+[alias] May-alias graph after instruction  int g = (int)tmp;  is
+  0:{ v.t; tmp } → 1:{ f }
 [alias] May-aliases at the end of function f: { v.t; tmp }
+[alias] May-alias graph at the end of function f:
+  0:{ v.t; tmp } → 1:{ f }
+[alias] Summary of function f:
+  formals:     locals: g  tmp→{ f }    returns: <none>
+  state: { v.t; tmp }
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle

@@ -4,4 +4,11 @@
 [alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from int to void *
 [alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from char * to int *
 [alias] May-aliases after instruction  tmp = (void *)*((int *)(t));  are  { t; tmp }
+[alias] May-alias graph after instruction  tmp = (void *)*((int *)(t));  is
+  0:{ t; tmp } → 1:{  }
 [alias] May-aliases at the end of function f: { t; tmp }
+[alias] May-alias graph at the end of function f:
+  0:{ t; tmp } → 1:{  }
+[alias] Summary of function f:
+  formals:     locals: tmp    returns: <none>    state: { t; tmp }
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle

 [kernel] Parsing semver.c (with preprocessing)
 [alias] analysing function: f
 [alias] May-aliases at the end of function f: <none>
+[alias] May-alias graph at the end of function f:
+  <empty>
+[alias] Summary of function f:
 [alias] analysing function: main
 [alias] analysing instruction: f((int *)*("1" + 2));
 [alias:unsafe-cast] semver.c:6: Warning: unsafe cast from char to int *
 [alias:unsupported:addr] semver.c:6: Warning: 
   unsupported feature: explicit pointer address: (int *)*("1" + 2); analysis may be unsound
 [alias] May-aliases after instruction  f((int *)*("1" + 2));  are  <none>
+[alias] May-alias graph after instruction  f((int *)*("1" + 2));  is    <empty>
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is    <empty>
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  <empty>
+[alias] Summary of function main:
+  formals:     locals: __retres    returns: __retres    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle

@@ -4,6 +4,15 @@
 [alias:unsafe-cast] tkn-2.c:6: Warning: unsafe cast from int ** to int *
 [alias] tkn-2.c:6: Warning: ignoring assignment of the form: a = (int *)(& a)
 [alias] May-aliases after instruction  a = (int *)(& a);  are  <none>
+[alias] May-alias graph after instruction  a = (int *)(& a);  is
+  0:{ a } → 1:{  }   2:{  } → 0:{ a }
 [alias] analysing instruction: __retres = *a;
 [alias] May-aliases after instruction  __retres = *a;  are  <none>
+[alias] May-alias graph after instruction  __retres = *a;  is
+  0:{ a } → 1:{  }   2:{  } → 0:{ a }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 1:{  }   2:{  } → 0:{ a }
+[alias] Summary of function main:
+  formals:     locals: a  __retres    returns: __retres    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle

@@ -3,19 +3,43 @@
 [alias] analysing instruction: char *s2 = CPS_SplitWord((char *)"a");
 [alias] analysing function: CPS_SplitWord
 [alias] May-aliases at the end of function CPS_SplitWord: <none>
+[alias] May-alias graph at the end of function CPS_SplitWord:
+  <empty>
+[alias] Summary of function CPS_SplitWord:
+  formals: line    locals:     returns: line    state: <none>
 [alias:unsafe-cast] union_vmap.c:11: Warning: 
   unsafe cast from char const * to char *
 [alias] May-aliases after instruction  char *s2 = CPS_SplitWord((char *)"a");  are
   <none>
+[alias] May-alias graph after instruction  char *s2 = CPS_SplitWord((char *)"a");
+  is    4:{ s2 } → 3:{  }
 [alias] analysing instruction: char *s3 = CPS_SplitWord((char *)"b");
 [alias:unsafe-cast] union_vmap.c:12: Warning: 
   unsafe cast from char const * to char *
 [alias] May-aliases after instruction  char *s3 = CPS_SplitWord((char *)"b");  are
   <none>
+[alias] May-alias graph after instruction  char *s3 = CPS_SplitWord((char *)"b");
+  is    4:{ s2 } → 3:{  }   8:{ s3 } → 7:{  }
 [alias] analysing instruction: *key = s3;
 [alias] May-aliases after instruction  *key = s3;  are  { *key; s3 }
+[alias] May-alias graph after instruction  *key = s3;  is
+  4:{ s2 } → 3:{  }   10:{ key } → 11:{ *key; s3 }
+  11:{ *key; s3 } → 7:{  }
 [alias] analysing instruction: *key = s2;
 [alias] May-aliases after instruction  *key = s2;  are  { *key; s2 }
+[alias] May-alias graph after instruction  *key = s2;  is
+  8:{ s3 } → 7:{  }   12:{ key } → 13:{ *key; s2 }
+  13:{ *key; s2 } → 3:{  }
 [alias] May-aliases at the end of function CPS_ParseKey: { *key; s2; s3 }
+[alias] May-alias graph at the end of function CPS_ParseKey:
+  4:{ *key; s2; s3 } → 3:{  }   10:{ key } → 4:{ *key; s2; s3 }
+[alias] Summary of function CPS_ParseKey:
+  formals:     locals: key→{ *key; s2; s3 }  s2  s3    returns: <none>
+  state: { *key; s2; s3 }
 [alias] analysing function: CPS_SplitWord
 [alias] May-aliases at the end of function CPS_SplitWord: <none>
+[alias] May-alias graph at the end of function CPS_SplitWord:
+  <empty>
+[alias] Summary of function CPS_SplitWord:
+  formals: line    locals:     returns: line    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/array1.res.oracle

@@ -2,16 +2,33 @@
 [alias] analysing function: main
 [alias] analysing instruction: tab[0] = 0;
 [alias] May-aliases after instruction  tab[0] = 0;  are  <none>
+[alias] May-alias graph after instruction  tab[0] = 0;  is    <empty>
 [alias] analysing instruction: tab[1] = 1;
 [alias] May-aliases after instruction  tab[1] = 1;  are  <none>
+[alias] May-alias graph after instruction  tab[1] = 1;  is    <empty>
 [alias] analysing instruction: tab[2] = tab[1] + 1;
 [alias] May-aliases after instruction  tab[2] = tab[1] + 1;  are  <none>
+[alias] May-alias graph after instruction  tab[2] = tab[1] + 1;  is    <empty>
 [alias] analysing instruction: int *x = & tab[1];
 [alias] May-aliases after instruction  int *x = & tab[1];  are  <none>
+[alias] May-alias graph after instruction  int *x = & tab[1];  is
+  0:{ x } → 1:{ tab[0..] }
 [alias] analysing instruction: int *y = & tab[2];
 [alias] May-aliases after instruction  int *y = & tab[2];  are  { x; y }
+[alias] May-alias graph after instruction  int *y = & tab[2];  is
+  0:{ x } → 5:{ tab[0..] }   4:{ y } → 5:{ tab[0..] }
 [alias] analysing instruction: tab[3] = *x + *y;
 [alias] May-aliases after instruction  tab[3] = *x + *y;  are  { x; y }
+[alias] May-alias graph after instruction  tab[3] = *x + *y;  is
+  0:{ x } → 5:{ tab[0..] }   4:{ y } → 5:{ tab[0..] }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { x; y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ x } → 5:{ tab[0..] }   4:{ y } → 5:{ tab[0..] }
 [alias] May-aliases at the end of function main: { x; y }
+[alias] May-alias graph at the end of function main:
+  0:{ x } → 5:{ tab[0..] }   4:{ y } → 5:{ tab[0..] }
+[alias] Summary of function main:
+  formals:     locals: tab  x→{ tab[0..] }  y→{ tab[0..] }  __retres
+  returns: __retres    state: { x; y }
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/array2.res.oracle

@@ -2,12 +2,26 @@
 [alias] analysing function: main
 [alias] analysing instruction: mat[0][0] = 0;
 [alias] May-aliases after instruction  mat[0][0] = 0;  are  <none>
+[alias] May-alias graph after instruction  mat[0][0] = 0;  is    <empty>
 [alias] analysing instruction: mat[0][1] = 1;
 [alias] May-aliases after instruction  mat[0][1] = 1;  are  <none>
+[alias] May-alias graph after instruction  mat[0][1] = 1;  is    <empty>
 [alias] analysing instruction: *x = mat[1];
 [alias] May-aliases after instruction  *x = mat[1];  are  <none>
+[alias] May-alias graph after instruction  *x = mat[1];  is
+  0:{ x } → 1:{ *x }   1:{ *x } → 2:{ mat[0..] }
 [alias] analysing instruction: *y = *(*(x + 0));
 [alias] May-aliases after instruction  *y = *(*(x + 0));  are  <none>
+[alias] May-alias graph after instruction  *y = *(*(x + 0));  is
+  0:{ x } → 1:{ *x }   1:{ *x } → 2:{ mat[0..] }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ x } → 1:{ *x }   1:{ *x } → 2:{ mat[0..] }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  0:{ x } → 1:{ *x }   1:{ *x } → 2:{ mat[0..] }
+[alias] Summary of function main:
+  formals:     locals: mat  x→{ *x }  y  __retres    returns: __retres
+  state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/array3.res.oracle

 [kernel] Parsing array3.c (with preprocessing)
 [alias] analysing function: _Exit
 [alias] May-aliases at the end of function _Exit: ⊥
+[alias] May-alias graph at the end of function _Exit:
+  ⊥
 [alias] analysing function: abort
 [alias] May-aliases at the end of function abort: ⊥
+[alias] May-alias graph at the end of function abort:
+  ⊥
 [alias] analysing function: abs
 [alias] May-aliases at the end of function abs: ⊥
+[alias] May-alias graph at the end of function abs:
+  ⊥
 [alias] analysing function: at_quick_exit
 [alias] May-aliases at the end of function at_quick_exit: ⊥
+[alias] May-alias graph at the end of function at_quick_exit:
+  ⊥
 [alias] analysing function: atexit
 [alias] May-aliases at the end of function atexit: ⊥
+[alias] May-alias graph at the end of function atexit:
+  ⊥
 [alias] analysing function: atof
 [alias] May-aliases at the end of function atof: ⊥
+[alias] May-alias graph at the end of function atof:
+  ⊥
 [alias] analysing function: atoi
 [alias] May-aliases at the end of function atoi: ⊥
+[alias] May-alias graph at the end of function atoi:
+  ⊥
 [alias] analysing function: atol
 [alias] May-aliases at the end of function atol: ⊥
+[alias] May-alias graph at the end of function atol:
+  ⊥
 [alias] analysing function: atoll
 [alias] May-aliases at the end of function atoll: ⊥
+[alias] May-alias graph at the end of function atoll:
+  ⊥
 [alias] analysing function: bsearch
 [alias] May-aliases at the end of function bsearch: ⊥
+[alias] May-alias graph at the end of function bsearch:
+  ⊥
 [alias] analysing function: calloc
 [alias] May-aliases at the end of function calloc: ⊥
+[alias] May-alias graph at the end of function calloc:
+  ⊥
 [alias] analysing function: div
 [alias] May-aliases at the end of function div: ⊥
+[alias] May-alias graph at the end of function div:
+  ⊥
 [alias] analysing function: drand48
 [alias] May-aliases at the end of function drand48: ⊥
+[alias] May-alias graph at the end of function drand48:
+  ⊥
 [alias] analysing function: erand48
 [alias] May-aliases at the end of function erand48: ⊥
+[alias] May-alias graph at the end of function erand48:
+  ⊥
 [alias] analysing function: exit
 [alias] May-aliases at the end of function exit: ⊥
+[alias] May-alias graph at the end of function exit:
+  ⊥
 [alias] analysing function: free
 [alias] May-aliases at the end of function free: ⊥
+[alias] May-alias graph at the end of function free:
+  ⊥
 [alias] analysing function: getenv
 [alias] May-aliases at the end of function getenv: ⊥
+[alias] May-alias graph at the end of function getenv:
+  ⊥
 [alias] analysing function: jrand48
 [alias] May-aliases at the end of function jrand48: ⊥
+[alias] May-alias graph at the end of function jrand48:
+  ⊥
 [alias] analysing function: labs
 [alias] May-aliases at the end of function labs: ⊥
+[alias] May-alias graph at the end of function labs:
+  ⊥
 [alias] analysing function: lcong48
 [alias] May-aliases at the end of function lcong48: ⊥
+[alias] May-alias graph at the end of function lcong48:
+  ⊥
 [alias] analysing function: ldiv
 [alias] May-aliases at the end of function ldiv: ⊥
+[alias] May-alias graph at the end of function ldiv:
+  ⊥
 [alias] analysing function: llabs
 [alias] May-aliases at the end of function llabs: ⊥
+[alias] May-alias graph at the end of function llabs:
+  ⊥
 [alias] analysing function: lldiv
 [alias] May-aliases at the end of function lldiv: ⊥
+[alias] May-alias graph at the end of function lldiv:
+  ⊥
 [alias] analysing function: lrand48
 [alias] May-aliases at the end of function lrand48: ⊥
+[alias] May-alias graph at the end of function lrand48:
+  ⊥
 [alias] analysing function: main
 [alias] analysing instruction: int *x = malloc((unsigned long)4 * sizeof(int));
 [alias] May-aliases after instruction
   int *x = malloc((unsigned long)4 * sizeof(int));  are  <none>
+[alias] May-alias graph after instruction
+  int *x = malloc((unsigned long)4 * sizeof(int));  is    0:{ x } → 1:{  }
 [alias] analysing instruction: int *y = malloc((unsigned long)4 * sizeof(int));
 [alias] May-aliases after instruction
   int *y = malloc((unsigned long)4 * sizeof(int));  are  <none>
+[alias] May-alias graph after instruction
+  int *y = malloc((unsigned long)4 * sizeof(int));  is
+  0:{ x } → 1:{  }   2:{ y } → 3:{  }
 [alias] analysing instruction: x = mat[0];
 [alias] May-aliases after instruction  x = mat[0];  are  <none>
+[alias] May-alias graph after instruction  x = mat[0];  is
+  0:{ x } → 1:{ mat[0..] }   2:{ y } → 3:{  }
 [alias] analysing instruction: y = mat[1];
 [alias] May-aliases after instruction  y = mat[1];  are  { x; y }
+[alias] May-alias graph after instruction  y = mat[1];  is
+  0:{ x } → 3:{ mat[0..] }   2:{ y } → 3:{ mat[0..] }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { x; y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ x } → 3:{ mat[0..] }   2:{ y } → 3:{ mat[0..] }
 [alias] May-aliases at the end of function main: { x; y }
+[alias] May-alias graph at the end of function main:
+  0:{ x } → 3:{ mat[0..] }   2:{ y } → 3:{ mat[0..] }
+[alias] Summary of function main:
+  formals:     locals: mat  x→{ mat[0..] }  y→{ mat[0..] }  __retres
+  returns: __retres    state: { x; y }
 [alias] analysing function: malloc
 [alias] May-aliases at the end of function malloc: ⊥
+[alias] May-alias graph at the end of function malloc:
+  ⊥
 [alias] analysing function: mblen
 [alias] May-aliases at the end of function mblen: ⊥
+[alias] May-alias graph at the end of function mblen:
+  ⊥
 [alias] analysing function: mbstowcs
 [alias] May-aliases at the end of function mbstowcs: ⊥
+[alias] May-alias graph at the end of function mbstowcs:
+  ⊥
 [alias] analysing function: mbtowc
 [alias] May-aliases at the end of function mbtowc: ⊥
+[alias] May-alias graph at the end of function mbtowc:
+  ⊥
 [alias] analysing function: mkstemp
 [alias] May-aliases at the end of function mkstemp: ⊥
+[alias] May-alias graph at the end of function mkstemp:
+  ⊥
 [alias] analysing function: mkstemps
 [alias] May-aliases at the end of function mkstemps: ⊥
+[alias] May-alias graph at the end of function mkstemps:
+  ⊥
 [alias] analysing function: mrand48
 [alias] May-aliases at the end of function mrand48: ⊥
+[alias] May-alias graph at the end of function mrand48:
+  ⊥
 [alias] analysing function: nrand48
 [alias] May-aliases at the end of function nrand48: ⊥
+[alias] May-alias graph at the end of function nrand48:
+  ⊥
 [alias] analysing function: posix_memalign
 [alias] May-aliases at the end of function posix_memalign: ⊥
+[alias] May-alias graph at the end of function posix_memalign:
+  ⊥
 [alias] analysing function: putenv
 [alias] May-aliases at the end of function putenv: ⊥
+[alias] May-alias graph at the end of function putenv:
+  ⊥
 [alias] analysing function: qsort
 [alias] May-aliases at the end of function qsort: ⊥
+[alias] May-alias graph at the end of function qsort:
+  ⊥
 [alias] analysing function: quick_exit
 [alias] May-aliases at the end of function quick_exit: ⊥
+[alias] May-alias graph at the end of function quick_exit:
+  ⊥
 [alias] analysing function: rand
 [alias] May-aliases at the end of function rand: ⊥
+[alias] May-alias graph at the end of function rand:
+  ⊥
 [alias] analysing function: random
 [alias] May-aliases at the end of function random: ⊥
+[alias] May-alias graph at the end of function random:
+  ⊥
 [alias] analysing function: realloc
 [alias] May-aliases at the end of function realloc: ⊥
+[alias] May-alias graph at the end of function realloc:
+  ⊥
 [alias] analysing function: reallocarray
 [alias] May-aliases at the end of function reallocarray: ⊥
+[alias] May-alias graph at the end of function reallocarray:
+  ⊥
 [alias] analysing function: seed48
 [alias] May-aliases at the end of function seed48: ⊥
+[alias] May-alias graph at the end of function seed48:
+  ⊥
 [alias] analysing function: setenv
 [alias] May-aliases at the end of function setenv: ⊥
+[alias] May-alias graph at the end of function setenv:
+  ⊥
 [alias] analysing function: srand
 [alias] May-aliases at the end of function srand: ⊥
+[alias] May-alias graph at the end of function srand:
+  ⊥
 [alias] analysing function: srand48
 [alias] May-aliases at the end of function srand48: ⊥
+[alias] May-alias graph at the end of function srand48:
+  ⊥
 [alias] analysing function: srandom
 [alias] May-aliases at the end of function srandom: ⊥
+[alias] May-alias graph at the end of function srandom:
+  ⊥
 [alias] analysing function: strtod
 [alias] May-aliases at the end of function strtod: ⊥
+[alias] May-alias graph at the end of function strtod:
+  ⊥
 [alias] analysing function: strtof
 [alias] May-aliases at the end of function strtof: ⊥
+[alias] May-alias graph at the end of function strtof:
+  ⊥
 [alias] analysing function: strtol
 [alias] May-aliases at the end of function strtol: ⊥
+[alias] May-alias graph at the end of function strtol:
+  ⊥
 [alias] analysing function: strtold
 [alias] May-aliases at the end of function strtold: ⊥
+[alias] May-alias graph at the end of function strtold:
+  ⊥
 [alias] analysing function: strtoll
 [alias] May-aliases at the end of function strtoll: ⊥
+[alias] May-alias graph at the end of function strtoll:
+  ⊥
 [alias] analysing function: strtoul
 [alias] May-aliases at the end of function strtoul: ⊥
+[alias] May-alias graph at the end of function strtoul:
+  ⊥
 [alias] analysing function: strtoull
 [alias] May-aliases at the end of function strtoull: ⊥
+[alias] May-alias graph at the end of function strtoull:
+  ⊥
 [alias] analysing function: system
 [alias] May-aliases at the end of function system: ⊥
+[alias] May-alias graph at the end of function system:
+  ⊥
 [alias] analysing function: unsetenv
 [alias] May-aliases at the end of function unsetenv: ⊥
+[alias] May-alias graph at the end of function unsetenv:
+  ⊥
 [alias] analysing function: wcstombs
 [alias] May-aliases at the end of function wcstombs: ⊥
+[alias] May-alias graph at the end of function wcstombs:
+  ⊥
 [alias] analysing function: wctomb
 [alias] May-aliases at the end of function wctomb: ⊥
+[alias] May-alias graph at the end of function wctomb:
+  ⊥
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle

@@ -2,18 +2,32 @@
 [alias] analysing function: main
 [alias] analysing instruction: tab[0] = 0;
 [alias] May-aliases after instruction  tab[0] = 0;  are  <none>
+[alias] May-alias graph after instruction  tab[0] = 0;  is    <empty>
 [alias] analysing instruction: tab[1] = 1;
 [alias] May-aliases after instruction  tab[1] = 1;  are  <none>
+[alias] May-alias graph after instruction  tab[1] = 1;  is    <empty>
 [alias] analysing instruction: tab[2] = tab[1] + 1;
 [alias] May-aliases after instruction  tab[2] = tab[1] + 1;  are  <none>
+[alias] May-alias graph after instruction  tab[2] = tab[1] + 1;  is    <empty>
 [alias] analysing instruction: int x = 0;
 [alias] May-aliases after instruction  int x = 0;  are  <none>
+[alias] May-alias graph after instruction  int x = 0;  is    <empty>
 [alias] analysing instruction: int i = 0;
 [alias] May-aliases after instruction  int i = 0;  are  <none>
+[alias] May-alias graph after instruction  int i = 0;  is    <empty>
 [alias] analysing instruction: x = tab[i];
 [alias] May-aliases after instruction  x = tab[i];  are  <none>
+[alias] May-alias graph after instruction  x = tab[i];  is    <empty>
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  <none>
+[alias] May-alias graph after instruction  i ++;  is    <empty>
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is    <empty>
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  <empty>
+[alias] Summary of function main:
+  formals:     locals: tab  x  i  __retres    returns: __retres
+  state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle

@@ -2,16 +2,28 @@
 [alias] analysing function: main
 [alias] analysing instruction: mat[0][0] = 0;
 [alias] May-aliases after instruction  mat[0][0] = 0;  are  <none>
+[alias] May-alias graph after instruction  mat[0][0] = 0;  is    <empty>
 [alias] analysing instruction: mat[0][1] = 1;
 [alias] May-aliases after instruction  mat[0][1] = 1;  are  <none>
+[alias] May-alias graph after instruction  mat[0][1] = 1;  is    <empty>
 [alias] analysing instruction: int i = 2;
 [alias] May-aliases after instruction  int i = 2;  are  <none>
+[alias] May-alias graph after instruction  int i = 2;  is    <empty>
 [alias] analysing instruction: mat[1][i] = i;
 [alias] May-aliases after instruction  mat[1][i] = i;  are  <none>
+[alias] May-alias graph after instruction  mat[1][i] = i;  is    <empty>
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  <none>
+[alias] May-alias graph after instruction  i ++;  is    <empty>
 [alias] analysing instruction: mat[1][i] = 2;
 [alias] May-aliases after instruction  mat[1][i] = 2;  are  <none>
+[alias] May-alias graph after instruction  mat[1][i] = 2;  is    <empty>
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is    <empty>
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  <empty>
+[alias] Summary of function main:
+  formals:     locals: mat  i  __retres    returns: __retres    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle

@@ -2,16 +2,28 @@
 [alias] analysing function: main
 [alias] analysing instruction: mat[0][0] = 0;
 [alias] May-aliases after instruction  mat[0][0] = 0;  are  <none>
+[alias] May-alias graph after instruction  mat[0][0] = 0;  is    <empty>
 [alias] analysing instruction: mat[0][1] = 1;
 [alias] May-aliases after instruction  mat[0][1] = 1;  are  <none>
+[alias] May-alias graph after instruction  mat[0][1] = 1;  is    <empty>
 [alias] analysing instruction: int i = 2;
 [alias] May-aliases after instruction  int i = 2;  are  <none>
+[alias] May-alias graph after instruction  int i = 2;  is    <empty>
 [alias] analysing instruction: mat[i][1] = i;
 [alias] May-aliases after instruction  mat[i][1] = i;  are  <none>
+[alias] May-alias graph after instruction  mat[i][1] = i;  is    <empty>
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  <none>
+[alias] May-alias graph after instruction  i ++;  is    <empty>
 [alias] analysing instruction: mat[i][1] = 2;
 [alias] May-aliases after instruction  mat[i][1] = 2;  are  <none>
+[alias] May-alias graph after instruction  mat[i][1] = 2;  is    <empty>
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is    <empty>
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  <empty>
+[alias] Summary of function main:
+  formals:     locals: mat  i  __retres    returns: __retres    state: <none>
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/nested1.res.oracle

 [kernel] Parsing nested1.c (with preprocessing)
 [alias] analysing function: _Exit
 [alias] May-aliases at the end of function _Exit: ⊥
+[alias] May-alias graph at the end of function _Exit:
+  ⊥
 [alias] analysing function: abort
 [alias] May-aliases at the end of function abort: ⊥
+[alias] May-alias graph at the end of function abort:
+  ⊥
 [alias] analysing function: abs
 [alias] May-aliases at the end of function abs: ⊥
+[alias] May-alias graph at the end of function abs:
+  ⊥
 [alias] analysing function: at_quick_exit
 [alias] May-aliases at the end of function at_quick_exit: ⊥
+[alias] May-alias graph at the end of function at_quick_exit:
+  ⊥
 [alias] analysing function: atexit
 [alias] May-aliases at the end of function atexit: ⊥
+[alias] May-alias graph at the end of function atexit:
+  ⊥
 [alias] analysing function: atof
 [alias] May-aliases at the end of function atof: ⊥
+[alias] May-alias graph at the end of function atof:
+  ⊥
 [alias] analysing function: atoi
 [alias] May-aliases at the end of function atoi: ⊥
+[alias] May-alias graph at the end of function atoi:
+  ⊥
 [alias] analysing function: atol
 [alias] May-aliases at the end of function atol: ⊥
+[alias] May-alias graph at the end of function atol:
+  ⊥
 [alias] analysing function: atoll
 [alias] May-aliases at the end of function atoll: ⊥
+[alias] May-alias graph at the end of function atoll:
+  ⊥
 [alias] analysing function: bsearch
 [alias] May-aliases at the end of function bsearch: ⊥
+[alias] May-alias graph at the end of function bsearch:
+  ⊥
 [alias] analysing function: calloc
 [alias] May-aliases at the end of function calloc: ⊥
+[alias] May-alias graph at the end of function calloc:
+  ⊥
 [alias] analysing function: div
 [alias] May-aliases at the end of function div: ⊥
+[alias] May-alias graph at the end of function div:
+  ⊥
 [alias] analysing function: drand48
 [alias] May-aliases at the end of function drand48: ⊥
+[alias] May-alias graph at the end of function drand48:
+  ⊥
 [alias] analysing function: erand48
 [alias] May-aliases at the end of function erand48: ⊥
+[alias] May-alias graph at the end of function erand48:
+  ⊥
 [alias] analysing function: exit
 [alias] May-aliases at the end of function exit: ⊥
+[alias] May-alias graph at the end of function exit:
+  ⊥
 [alias] analysing function: free
 [alias] May-aliases at the end of function free: ⊥
+[alias] May-alias graph at the end of function free:
+  ⊥
 [alias] analysing function: getenv
 [alias] May-aliases at the end of function getenv: ⊥
+[alias] May-alias graph at the end of function getenv:
+  ⊥
 [alias] analysing function: jrand48
 [alias] May-aliases at the end of function jrand48: ⊥
+[alias] May-alias graph at the end of function jrand48:
+  ⊥
 [alias] analysing function: labs
 [alias] May-aliases at the end of function labs: ⊥
+[alias] May-alias graph at the end of function labs:
+  ⊥
 [alias] analysing function: lcong48
 [alias] May-aliases at the end of function lcong48: ⊥
+[alias] May-alias graph at the end of function lcong48:
+  ⊥
 [alias] analysing function: ldiv
 [alias] May-aliases at the end of function ldiv: ⊥
+[alias] May-alias graph at the end of function ldiv:
+  ⊥
 [alias] analysing function: llabs
 [alias] May-aliases at the end of function llabs: ⊥
+[alias] May-alias graph at the end of function llabs:
+  ⊥
 [alias] analysing function: lldiv
 [alias] May-aliases at the end of function lldiv: ⊥
+[alias] May-alias graph at the end of function lldiv:
+  ⊥
 [alias] analysing function: lrand48
 [alias] May-aliases at the end of function lrand48: ⊥
+[alias] May-alias graph at the end of function lrand48:
+  ⊥
 [alias] analysing function: main
 [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
 [alias] May-aliases after instruction  st_1_t x1 = {.a = 0, .b = 1};  are  <none>
+[alias] May-alias graph after instruction  st_1_t x1 = {.a = 0, .b = 1};  is
+  <empty>
 [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
 [alias] May-aliases after instruction  st_1_t x2 = {.a = 1, .b = 2};  are  <none>
+[alias] May-alias graph after instruction  st_1_t x2 = {.a = 1, .b = 2};  is
+  <empty>
 [alias] analysing instruction: tab_y[0] = & x1;
 [alias] May-aliases after instruction  tab_y[0] = & x1;  are  <none>
+[alias] May-alias graph after instruction  tab_y[0] = & x1;  is
+  0:{ tab_y[0..] } → 1:{ x1 }
 [alias] analysing instruction: tab_y[1] = & x2;
 [alias] May-aliases after instruction  tab_y[1] = & x2;  are  <none>
+[alias] May-alias graph after instruction  tab_y[1] = & x2;  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }
 [alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
 [alias] May-aliases after instruction  st_2_t *z1 = malloc(sizeof(st_2_t));  are
   <none>
+[alias] May-alias graph after instruction  st_2_t *z1 = malloc(sizeof(st_2_t));
+  is    0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
 [alias] analysing instruction: st_2_t *z2 = malloc(sizeof(st_2_t));
 [alias] May-aliases after instruction  st_2_t *z2 = malloc(sizeof(st_2_t));  are
   <none>
+[alias] May-alias graph after instruction  st_2_t *z2 = malloc(sizeof(st_2_t));
+  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }   7:{ z2 } → 8:{  }
 [alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t));
 [alias] May-aliases after instruction  st_3_t *t = malloc(sizeof(st_3_t));  are
   <none>
+[alias] May-alias graph after instruction  st_3_t *t = malloc(sizeof(st_3_t));  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
 [alias] analysing instruction: int *a = malloc(sizeof(int));
 [alias] May-aliases after instruction  int *a = malloc(sizeof(int));  are  <none>
+[alias] May-alias graph after instruction  int *a = malloc(sizeof(int));  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }   11:{ a } → 12:{  }
 [alias] analysing instruction: int *b = malloc(sizeof(int));
 [alias] May-aliases after instruction  int *b = malloc(sizeof(int));  are  <none>
+[alias] May-alias graph after instruction  int *b = malloc(sizeof(int));  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }   11:{ a } → 12:{  }
+  13:{ b } → 14:{  }
 [alias] analysing instruction: *a = 0;
 [alias] May-aliases after instruction  *a = 0;  are  <none>
+[alias] May-alias graph after instruction  *a = 0;  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }   11:{ a } → 12:{  }
+  13:{ b } → 14:{  }
 [alias] analysing instruction: *b = 5;
 [alias] May-aliases after instruction  *b = 5;  are  <none>
+[alias] May-alias graph after instruction  *b = 5;  is
+  0:{ tab_y[0..] } → 1:{ x1; x2 }   5:{ z1 } → 6:{  }
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }   11:{ a } → 12:{  }
+  13:{ b } → 14:{  }
 [alias] analysing instruction: z1->s = (struct struct_1_t *)tab_y[0];
 [alias:unsafe-cast] nested1.c:47: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z1->s = (struct struct_1_t *)tab_y[0];  are
   { z1->s; tab_y[0..] }
+[alias] May-alias graph after instruction  z1->s = (struct struct_1_t *)tab_y[0];
+  is
+  5:{ z1 } → 6:{  }   7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  11:{ a } → 12:{  }   13:{ b } → 14:{  }
+  15:{ z1->s; tab_y[0..] } → 1:{ x1; x2 }
 [alias] analysing instruction: z2->s = (struct struct_1_t *)tab_y[1];
 [alias:unsafe-cast] nested1.c:48: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z2->s = (struct struct_1_t *)tab_y[1];  are
   { z1->s; z2->s; tab_y[0..] }
+[alias] May-alias graph after instruction  z2->s = (struct struct_1_t *)tab_y[1];
+  is
+  5:{ z1 } → 6:{  }   7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  11:{ a } → 12:{  }   13:{ b } → 14:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
 [alias] analysing instruction: z1->c = a;
 [alias] May-aliases after instruction  z1->c = a;  are
   { z1->s; z2->s; tab_y[0..] }  { z1->c; a }
+[alias] May-alias graph after instruction  z1->c = a;  is
+  5:{ z1 } → 6:{  }   7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  13:{ b } → 14:{  }   16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  17:{ z1->c; a } → 12:{  }
 [alias] analysing instruction: z2->c = b;
 [alias] May-aliases after instruction  z2->c = b;  are
   { z1->s; z2->s; tab_y[0..] }  { z1->c; a }  { z2->c; b }
+[alias] May-alias graph after instruction  z2->c = b;  is
+  5:{ z1 } → 6:{  }   7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  17:{ z1->c; a } → 12:{  }   18:{ z2->c; b } → 14:{  }
 [alias] analysing instruction: t->t = (struct struct_2_t *)z1;
 [alias:unsafe-cast] nested1.c:51: Warning: 
   unsafe cast from st_2_t * to struct struct_2_t *
 [alias] May-aliases after instruction  t->t = (struct struct_2_t *)z1;  are
   { z1->s; z2->s; tab_y[0..] }  { t->t; z1 }  { z1->c; a }  { z2->c; b }
+[alias] May-alias graph after instruction  t->t = (struct struct_2_t *)z1;  is
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  17:{ z1->c; a } → 12:{  }   18:{ z2->c; b } → 14:{  }
+  19:{ t->t; z1 } → 6:{  }
 [alias] analysing instruction: t->d = a;
 [alias] May-aliases after instruction  t->d = a;  are
   { z1->s; z2->s; tab_y[0..] }  { t->t; z1 }  { z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph after instruction  t->d = a;  is
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  18:{ z2->c; b } → 14:{  }   19:{ t->t; z1 } → 6:{  }
+  20:{ z1->c; t->d; a } → 12:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { z1->s; z2->s; tab_y[0..] }  { t->t; z1 }  { z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  18:{ z2->c; b } → 14:{  }   19:{ t->t; z1 } → 6:{  }
+  20:{ z1->c; t->d; a } → 12:{  }
 [alias] May-aliases at the end of function main:
   { z1->s; z2->s; tab_y[0..] }  { t->t; z1 }  { z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph at the end of function main:
+  7:{ z2 } → 8:{  }   9:{ t } → 10:{  }
+  16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 }
+  18:{ z2->c; b } → 14:{  }   19:{ t->t; z1 } → 6:{  }
+  20:{ z1->c; t->d; a } → 12:{  }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  tab_y  z1  z2  t  a  b  __retres
+  returns: __retres
+  state: { z1->s; z2->s; tab_y[0..] }  { t->t; z1 }  { z1->c; t->d; a }
+         { z2->c; b }
 [alias] analysing function: malloc
 [alias] May-aliases at the end of function malloc: ⊥
+[alias] May-alias graph at the end of function malloc:
+  ⊥
 [alias] analysing function: mblen
 [alias] May-aliases at the end of function mblen: ⊥
+[alias] May-alias graph at the end of function mblen:
+  ⊥
 [alias] analysing function: mbstowcs
 [alias] May-aliases at the end of function mbstowcs: ⊥
+[alias] May-alias graph at the end of function mbstowcs:
+  ⊥
 [alias] analysing function: mbtowc
 [alias] May-aliases at the end of function mbtowc: ⊥
+[alias] May-alias graph at the end of function mbtowc:
+  ⊥
 [alias] analysing function: mkstemp
 [alias] May-aliases at the end of function mkstemp: ⊥
+[alias] May-alias graph at the end of function mkstemp:
+  ⊥
 [alias] analysing function: mkstemps
 [alias] May-aliases at the end of function mkstemps: ⊥
+[alias] May-alias graph at the end of function mkstemps:
+  ⊥
 [alias] analysing function: mrand48
 [alias] May-aliases at the end of function mrand48: ⊥
+[alias] May-alias graph at the end of function mrand48:
+  ⊥
 [alias] analysing function: nrand48
 [alias] May-aliases at the end of function nrand48: ⊥
+[alias] May-alias graph at the end of function nrand48:
+  ⊥
 [alias] analysing function: posix_memalign
 [alias] May-aliases at the end of function posix_memalign: ⊥
+[alias] May-alias graph at the end of function posix_memalign:
+  ⊥
 [alias] analysing function: putenv
 [alias] May-aliases at the end of function putenv: ⊥
+[alias] May-alias graph at the end of function putenv:
+  ⊥
 [alias] analysing function: qsort
 [alias] May-aliases at the end of function qsort: ⊥
+[alias] May-alias graph at the end of function qsort:
+  ⊥
 [alias] analysing function: quick_exit
 [alias] May-aliases at the end of function quick_exit: ⊥
+[alias] May-alias graph at the end of function quick_exit:
+  ⊥
 [alias] analysing function: rand
 [alias] May-aliases at the end of function rand: ⊥
+[alias] May-alias graph at the end of function rand:
+  ⊥
 [alias] analysing function: random
 [alias] May-aliases at the end of function random: ⊥
+[alias] May-alias graph at the end of function random:
+  ⊥
 [alias] analysing function: realloc
 [alias] May-aliases at the end of function realloc: ⊥
+[alias] May-alias graph at the end of function realloc:
+  ⊥
 [alias] analysing function: reallocarray
 [alias] May-aliases at the end of function reallocarray: ⊥
+[alias] May-alias graph at the end of function reallocarray:
+  ⊥
 [alias] analysing function: seed48
 [alias] May-aliases at the end of function seed48: ⊥
+[alias] May-alias graph at the end of function seed48:
+  ⊥
 [alias] analysing function: setenv
 [alias] May-aliases at the end of function setenv: ⊥
+[alias] May-alias graph at the end of function setenv:
+  ⊥
 [alias] analysing function: srand
 [alias] May-aliases at the end of function srand: ⊥
+[alias] May-alias graph at the end of function srand:
+  ⊥
 [alias] analysing function: srand48
 [alias] May-aliases at the end of function srand48: ⊥
+[alias] May-alias graph at the end of function srand48:
+  ⊥
 [alias] analysing function: srandom
 [alias] May-aliases at the end of function srandom: ⊥
+[alias] May-alias graph at the end of function srandom:
+  ⊥
 [alias] analysing function: strtod
 [alias] May-aliases at the end of function strtod: ⊥
+[alias] May-alias graph at the end of function strtod:
+  ⊥
 [alias] analysing function: strtof
 [alias] May-aliases at the end of function strtof: ⊥
+[alias] May-alias graph at the end of function strtof:
+  ⊥
 [alias] analysing function: strtol
 [alias] May-aliases at the end of function strtol: ⊥
+[alias] May-alias graph at the end of function strtol:
+  ⊥
 [alias] analysing function: strtold
 [alias] May-aliases at the end of function strtold: ⊥
+[alias] May-alias graph at the end of function strtold:
+  ⊥
 [alias] analysing function: strtoll
 [alias] May-aliases at the end of function strtoll: ⊥
+[alias] May-alias graph at the end of function strtoll:
+  ⊥
 [alias] analysing function: strtoul
 [alias] May-aliases at the end of function strtoul: ⊥
+[alias] May-alias graph at the end of function strtoul:
+  ⊥
 [alias] analysing function: strtoull
 [alias] May-aliases at the end of function strtoull: ⊥
+[alias] May-alias graph at the end of function strtoull:
+  ⊥
 [alias] analysing function: system
 [alias] May-aliases at the end of function system: ⊥
+[alias] May-alias graph at the end of function system:
+  ⊥
 [alias] analysing function: unsetenv
 [alias] May-aliases at the end of function unsetenv: ⊥
+[alias] May-alias graph at the end of function unsetenv:
+  ⊥
 [alias] analysing function: wcstombs
 [alias] May-aliases at the end of function wcstombs: ⊥
+[alias] May-alias graph at the end of function wcstombs:
+  ⊥
 [alias] analysing function: wctomb
 [alias] May-aliases at the end of function wctomb: ⊥
+[alias] May-alias graph at the end of function wctomb:
+  ⊥
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/nested2.res.oracle

 [kernel] Parsing nested2.c (with preprocessing)
 [alias] analysing function: _Exit
 [alias] May-aliases at the end of function _Exit: ⊥
+[alias] May-alias graph at the end of function _Exit:
+  ⊥
 [alias] analysing function: abort
 [alias] May-aliases at the end of function abort: ⊥
+[alias] May-alias graph at the end of function abort:
+  ⊥
 [alias] analysing function: abs
 [alias] May-aliases at the end of function abs: ⊥
+[alias] May-alias graph at the end of function abs:
+  ⊥
 [alias] analysing function: at_quick_exit
 [alias] May-aliases at the end of function at_quick_exit: ⊥
+[alias] May-alias graph at the end of function at_quick_exit:
+  ⊥
 [alias] analysing function: atexit
 [alias] May-aliases at the end of function atexit: ⊥
+[alias] May-alias graph at the end of function atexit:
+  ⊥
 [alias] analysing function: atof
 [alias] May-aliases at the end of function atof: ⊥
+[alias] May-alias graph at the end of function atof:
+  ⊥
 [alias] analysing function: atoi
 [alias] May-aliases at the end of function atoi: ⊥
+[alias] May-alias graph at the end of function atoi:
+  ⊥
 [alias] analysing function: atol
 [alias] May-aliases at the end of function atol: ⊥
+[alias] May-alias graph at the end of function atol:
+  ⊥
 [alias] analysing function: atoll
 [alias] May-aliases at the end of function atoll: ⊥
+[alias] May-alias graph at the end of function atoll:
+  ⊥
 [alias] analysing function: bsearch
 [alias] May-aliases at the end of function bsearch: ⊥
+[alias] May-alias graph at the end of function bsearch:
+  ⊥
 [alias] analysing function: calloc
 [alias] May-aliases at the end of function calloc: ⊥
+[alias] May-alias graph at the end of function calloc:
+  ⊥
 [alias] analysing function: div
 [alias] May-aliases at the end of function div: ⊥
+[alias] May-alias graph at the end of function div:
+  ⊥
 [alias] analysing function: drand48
 [alias] May-aliases at the end of function drand48: ⊥
+[alias] May-alias graph at the end of function drand48:
+  ⊥
 [alias] analysing function: erand48
 [alias] May-aliases at the end of function erand48: ⊥
+[alias] May-alias graph at the end of function erand48:
+  ⊥
 [alias] analysing function: exit
 [alias] May-aliases at the end of function exit: ⊥
+[alias] May-alias graph at the end of function exit:
+  ⊥
 [alias] analysing function: free
 [alias] May-aliases at the end of function free: ⊥
+[alias] May-alias graph at the end of function free:
+  ⊥
 [alias] analysing function: getenv
 [alias] May-aliases at the end of function getenv: ⊥
+[alias] May-alias graph at the end of function getenv:
+  ⊥
 [alias] analysing function: jrand48
 [alias] May-aliases at the end of function jrand48: ⊥
+[alias] May-alias graph at the end of function jrand48:
+  ⊥
 [alias] analysing function: labs
 [alias] May-aliases at the end of function labs: ⊥
+[alias] May-alias graph at the end of function labs:
+  ⊥
 [alias] analysing function: lcong48
 [alias] May-aliases at the end of function lcong48: ⊥
+[alias] May-alias graph at the end of function lcong48:
+  ⊥
 [alias] analysing function: ldiv
 [alias] May-aliases at the end of function ldiv: ⊥
+[alias] May-alias graph at the end of function ldiv:
+  ⊥
 [alias] analysing function: llabs
 [alias] May-aliases at the end of function llabs: ⊥
+[alias] May-alias graph at the end of function llabs:
+  ⊥
 [alias] analysing function: lldiv
 [alias] May-aliases at the end of function lldiv: ⊥
+[alias] May-alias graph at the end of function lldiv:
+  ⊥
 [alias] analysing function: lrand48
 [alias] May-aliases at the end of function lrand48: ⊥
+[alias] May-alias graph at the end of function lrand48:
+  ⊥
 [alias] analysing function: main
 [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
 [alias] May-aliases after instruction  st_1_t x1 = {.a = 0, .b = 1};  are  <none>
+[alias] May-alias graph after instruction  st_1_t x1 = {.a = 0, .b = 1};  is
+  <empty>
 [alias] analysing instruction: st_1_t x2 = {.a = 2, .b = 3};
 [alias] May-aliases after instruction  st_1_t x2 = {.a = 2, .b = 3};  are  <none>
+[alias] May-alias graph after instruction  st_1_t x2 = {.a = 2, .b = 3};  is
+  <empty>
 [alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
 [alias] May-aliases after instruction  st_2_t *z1 = malloc(sizeof(st_2_t));  are
   <none>
+[alias] May-alias graph after instruction  st_2_t *z1 = malloc(sizeof(st_2_t));
+  is    0:{ z1 } → 1:{  }
 [alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t));
 [alias] May-aliases after instruction  st_3_t *t = malloc(sizeof(st_3_t));  are
   <none>
+[alias] May-alias graph after instruction  st_3_t *t = malloc(sizeof(st_3_t));  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }
 [alias] analysing instruction: int *a = malloc(sizeof(int));
 [alias] May-aliases after instruction  int *a = malloc(sizeof(int));  are  <none>
+[alias] May-alias graph after instruction  int *a = malloc(sizeof(int));  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }   4:{ a } → 5:{  }
 [alias] analysing instruction: *a = 0;
 [alias] May-aliases after instruction  *a = 0;  are  <none>
+[alias] May-alias graph after instruction  *a = 0;  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }   4:{ a } → 5:{  }
 [alias] analysing instruction: z1->s[0] = (struct struct_1_t *)(& x1);
 [alias:unsafe-cast] nested2.c:42: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z1->s[0] = (struct struct_1_t *)(& x1);  are
   <none>
+[alias] May-alias graph after instruction  z1->s[0] = (struct struct_1_t *)(& x1);
+  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }   4:{ a } → 5:{  }
+  6:{ z1->s[0..] } → 7:{ x1 }
 [alias] analysing instruction: z1->s[1] = (struct struct_1_t *)(& x2);
 [alias:unsafe-cast] nested2.c:43: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z1->s[1] = (struct struct_1_t *)(& x2);  are
   <none>
+[alias] May-alias graph after instruction  z1->s[1] = (struct struct_1_t *)(& x2);
+  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }   4:{ a } → 5:{  }
+  6:{ z1->s[0..] } → 7:{ x1; x2 }
 [alias] analysing instruction: z1->c = a;
 [alias] May-aliases after instruction  z1->c = a;  are  { z1->c; a }
+[alias] May-alias graph after instruction  z1->c = a;  is
+  0:{ z1 } → 1:{  }   2:{ t } → 3:{  }
+  6:{ z1->s[0..] } → 7:{ x1; x2 }   11:{ z1->c; a } → 5:{  }
 [alias] analysing instruction: t->t = (struct struct_2_t *)z1;
 [alias:unsafe-cast] nested2.c:45: Warning: 
   unsafe cast from st_2_t * to struct struct_2_t *
 [alias] May-aliases after instruction  t->t = (struct struct_2_t *)z1;  are
   { t->t; z1 }  { z1->c; a }
+[alias] May-alias graph after instruction  t->t = (struct struct_2_t *)z1;  is
+  2:{ t } → 3:{  }   6:{ z1->s[0..] } → 7:{ x1; x2 }
+  11:{ z1->c; a } → 5:{  }   12:{ t->t; z1 } → 1:{  }
 [alias] analysing instruction: t->d = a;
 [alias] May-aliases after instruction  t->d = a;  are
   { t->t; z1 }  { z1->c; t->d; a }
+[alias] May-alias graph after instruction  t->d = a;  is
+  2:{ t } → 3:{  }   6:{ z1->s[0..] } → 7:{ x1; x2 }
+  12:{ t->t; z1 } → 1:{  }   13:{ z1->c; t->d; a } → 5:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { t->t; z1 }  { z1->c; t->d; a }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  2:{ t } → 3:{  }   6:{ z1->s[0..] } → 7:{ x1; x2 }
+  12:{ t->t; z1 } → 1:{  }   13:{ z1->c; t->d; a } → 5:{  }
 [alias] May-aliases at the end of function main: { t->t; z1 }  { z1->c; t->d; a }
+[alias] May-alias graph at the end of function main:
+  2:{ t } → 3:{  }   6:{ z1->s[0..] } → 7:{ x1; x2 }
+  12:{ t->t; z1 } → 1:{  }   13:{ z1->c; t->d; a } → 5:{  }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  z1  t  a  __retres    returns: __retres
+  state: { t->t; z1 }  { z1->c; t->d; a }
 [alias] analysing function: malloc
 [alias] May-aliases at the end of function malloc: ⊥
+[alias] May-alias graph at the end of function malloc:
+  ⊥
 [alias] analysing function: mblen
 [alias] May-aliases at the end of function mblen: ⊥
+[alias] May-alias graph at the end of function mblen:
+  ⊥
 [alias] analysing function: mbstowcs
 [alias] May-aliases at the end of function mbstowcs: ⊥
+[alias] May-alias graph at the end of function mbstowcs:
+  ⊥
 [alias] analysing function: mbtowc
 [alias] May-aliases at the end of function mbtowc: ⊥
+[alias] May-alias graph at the end of function mbtowc:
+  ⊥
 [alias] analysing function: mkstemp
 [alias] May-aliases at the end of function mkstemp: ⊥
+[alias] May-alias graph at the end of function mkstemp:
+  ⊥
 [alias] analysing function: mkstemps
 [alias] May-aliases at the end of function mkstemps: ⊥
+[alias] May-alias graph at the end of function mkstemps:
+  ⊥
 [alias] analysing function: mrand48
 [alias] May-aliases at the end of function mrand48: ⊥
+[alias] May-alias graph at the end of function mrand48:
+  ⊥
 [alias] analysing function: nrand48
 [alias] May-aliases at the end of function nrand48: ⊥
+[alias] May-alias graph at the end of function nrand48:
+  ⊥
 [alias] analysing function: posix_memalign
 [alias] May-aliases at the end of function posix_memalign: ⊥
+[alias] May-alias graph at the end of function posix_memalign:
+  ⊥
 [alias] analysing function: putenv
 [alias] May-aliases at the end of function putenv: ⊥
+[alias] May-alias graph at the end of function putenv:
+  ⊥
 [alias] analysing function: qsort
 [alias] May-aliases at the end of function qsort: ⊥
+[alias] May-alias graph at the end of function qsort:
+  ⊥
 [alias] analysing function: quick_exit
 [alias] May-aliases at the end of function quick_exit: ⊥
+[alias] May-alias graph at the end of function quick_exit:
+  ⊥
 [alias] analysing function: rand
 [alias] May-aliases at the end of function rand: ⊥
+[alias] May-alias graph at the end of function rand:
+  ⊥
 [alias] analysing function: random
 [alias] May-aliases at the end of function random: ⊥
+[alias] May-alias graph at the end of function random:
+  ⊥
 [alias] analysing function: realloc
 [alias] May-aliases at the end of function realloc: ⊥
+[alias] May-alias graph at the end of function realloc:
+  ⊥
 [alias] analysing function: reallocarray
 [alias] May-aliases at the end of function reallocarray: ⊥
+[alias] May-alias graph at the end of function reallocarray:
+  ⊥
 [alias] analysing function: seed48
 [alias] May-aliases at the end of function seed48: ⊥
+[alias] May-alias graph at the end of function seed48:
+  ⊥
 [alias] analysing function: setenv
 [alias] May-aliases at the end of function setenv: ⊥
+[alias] May-alias graph at the end of function setenv:
+  ⊥
 [alias] analysing function: srand
 [alias] May-aliases at the end of function srand: ⊥
+[alias] May-alias graph at the end of function srand:
+  ⊥
 [alias] analysing function: srand48
 [alias] May-aliases at the end of function srand48: ⊥
+[alias] May-alias graph at the end of function srand48:
+  ⊥
 [alias] analysing function: srandom
 [alias] May-aliases at the end of function srandom: ⊥
+[alias] May-alias graph at the end of function srandom:
+  ⊥
 [alias] analysing function: strtod
 [alias] May-aliases at the end of function strtod: ⊥
+[alias] May-alias graph at the end of function strtod:
+  ⊥
 [alias] analysing function: strtof
 [alias] May-aliases at the end of function strtof: ⊥
+[alias] May-alias graph at the end of function strtof:
+  ⊥
 [alias] analysing function: strtol
 [alias] May-aliases at the end of function strtol: ⊥
+[alias] May-alias graph at the end of function strtol:
+  ⊥
 [alias] analysing function: strtold
 [alias] May-aliases at the end of function strtold: ⊥
+[alias] May-alias graph at the end of function strtold:
+  ⊥
 [alias] analysing function: strtoll
 [alias] May-aliases at the end of function strtoll: ⊥
+[alias] May-alias graph at the end of function strtoll:
+  ⊥
 [alias] analysing function: strtoul
 [alias] May-aliases at the end of function strtoul: ⊥
+[alias] May-alias graph at the end of function strtoul:
+  ⊥
 [alias] analysing function: strtoull
 [alias] May-aliases at the end of function strtoull: ⊥
+[alias] May-alias graph at the end of function strtoull:
+  ⊥
 [alias] analysing function: system
 [alias] May-aliases at the end of function system: ⊥
+[alias] May-alias graph at the end of function system:
+  ⊥
 [alias] analysing function: unsetenv
 [alias] May-aliases at the end of function unsetenv: ⊥
+[alias] May-alias graph at the end of function unsetenv:
+  ⊥
 [alias] analysing function: wcstombs
 [alias] May-aliases at the end of function wcstombs: ⊥
+[alias] May-alias graph at the end of function wcstombs:
+  ⊥
 [alias] analysing function: wctomb
 [alias] May-aliases at the end of function wctomb: ⊥
+[alias] May-alias graph at the end of function wctomb:
+  ⊥
+[alias] Analysis complete

src/plugins/alias/tests/offsets/oracle/structure1.res.oracle

@@ -2,18 +2,38 @@
 [alias] analysing function: main
 [alias] analysing instruction: st_1_t x = {.a = 0, .b = 1};
 [alias] May-aliases after instruction  st_1_t x = {.a = 0, .b = 1};  are  <none>
+[alias] May-alias graph after instruction  st_1_t x = {.a = 0, .b = 1};  is
+  <empty>
 [alias] analysing instruction: st_2_t y = {.a = 3, .c = 4};
 [alias] May-aliases after instruction  st_2_t y = {.a = 3, .c = 4};  are  <none>
+[alias] May-alias graph after instruction  st_2_t y = {.a = 3, .c = 4};  is
+  <empty>
 [alias] analysing instruction: st_1_t *p_x = & x;
 [alias] May-aliases after instruction  st_1_t *p_x = & x;  are  <none>
+[alias] May-alias graph after instruction  st_1_t *p_x = & x;  is
+  0:{ p_x } → 1:{ x }
 [alias] analysing instruction: st_2_t *p_y = & y;
 [alias] May-aliases after instruction  st_2_t *p_y = & y;  are  <none>
+[alias] May-alias graph after instruction  st_2_t *p_y = & y;  is
+  0:{ p_x } → 1:{ x }   4:{ p_y } → 5:{ y }
 [alias] analysing instruction: p_x->a = 3;
 [alias] May-aliases after instruction  p_x->a = 3;  are  <none>
+[alias] May-alias graph after instruction  p_x->a = 3;  is
+  0:{ p_x } → 1:{ x }   4:{ p_y } → 5:{ y }
 [alias] analysing instruction: p_x = (st_1_t *)p_y;
 [alias:unsafe-cast] structure1.c:28: Warning: 
   unsafe cast from st_2_t * to st_1_t *
 [alias] May-aliases after instruction  p_x = (st_1_t *)p_y;  are  { p_x; p_y }
+[alias] May-alias graph after instruction  p_x = (st_1_t *)p_y;  is
+  0:{ p_x; p_y } → 1:{ x; y }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { p_x; p_y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ p_x; p_y } → 1:{ x; y }
 [alias] May-aliases at the end of function main: { p_x; p_y }
+[alias] May-alias graph at the end of function main:
+  0:{ p_x; p_y } → 1:{ x; y }
+[alias] Summary of function main:
+  formals:     locals: x  y  p_x→{ x; y }  p_y→{ x; y }  __retres
+  returns: __retres    state: { p_x; p_y }
+[alias] Analysis complete