From 791a19b873f5e57b9aacfc84bc76999699c3a70c Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Thu, 29 Feb 2024 11:22:49 +0100
Subject: [PATCH] [alias] enable again printing of graphs for tests

This reverts 76735c2870 "disable printing of graphs for tests"
---
 .../tests/basic/oracle/addrof.res.oracle      |  22 ++
 .../tests/basic/oracle/assignment1.res.oracle |  15 ++
 .../tests/basic/oracle/assignment2.res.oracle |  19 ++
 .../tests/basic/oracle/assignment3.res.oracle |  14 ++
 .../tests/basic/oracle/assignment4.res.oracle |  19 ++
 .../tests/basic/oracle/assignment5.res.oracle |  18 ++
 .../alias/tests/basic/oracle/cast1.res.oracle |  15 ++
 .../basic/oracle/conditional1.res.oracle      |  14 ++
 .../basic/oracle/conditional2.res.oracle      |  20 ++
 .../basic/oracle/conditional3.res.oracle      |  42 ++++
 .../tests/basic/oracle/function1.res.oracle   |  32 +++
 .../tests/basic/oracle/function2.res.oracle   |  25 ++
 .../tests/basic/oracle/function3.res.oracle   |  30 +++
 .../tests/basic/oracle/function4.res.oracle   |  19 ++
 .../tests/basic/oracle/function5.res.oracle   |  23 ++
 .../tests/basic/oracle/function6.res.oracle   |  24 ++
 .../tests/basic/oracle/globctr.res.oracle     |  15 ++
 .../alias/tests/basic/oracle/loop.res.oracle  |  19 ++
 .../tests/basic/oracle/steensgaard.res.oracle |  24 ++
 .../tests/basic/oracle/switch1.res.oracle     |  17 ++
 .../tests/basic/oracle/switch2.res.oracle     |  19 ++
 .../tests/basic/oracle/while_for1.res.oracle  |  13 ++
 .../tests/basic/oracle/while_for2.res.oracle  |  11 +
 .../tests/basic/oracle/while_for3.res.oracle  |  14 ++
 .../fixed_bugs/oracle/empty_nodes.res.oracle  |  20 ++
 .../fixed_bugs/oracle/gzip124.res.oracle      |  15 ++
 .../tests/fixed_bugs/oracle/origin.res.oracle |  11 +
 .../fixed_bugs/oracle/origin_simpl.res.oracle |   7 +
 .../tests/fixed_bugs/oracle/semver.res.oracle |  10 +
 .../tests/fixed_bugs/oracle/tkn-2.res.oracle  |   9 +
 .../fixed_bugs/oracle/union_vmap.res.oracle   |  22 ++
 .../tests/offsets/oracle/array1.res.oracle    |  17 ++
 .../tests/offsets/oracle/array2.res.oracle    |  14 ++
 .../tests/offsets/oracle/array3.res.oracle    |  17 ++
 .../tests/offsets/oracle/collapse1.res.oracle |  14 ++
 .../tests/offsets/oracle/collapse2.res.oracle |  12 +
 .../tests/offsets/oracle/collapse3.res.oracle |  12 +
 .../offsets/oracle/jfla_running_ex.res.oracle |  79 +++++++
 .../tests/offsets/oracle/nested1.res.oracle   |  81 +++++++
 .../tests/offsets/oracle/nested2.res.oracle   |  45 ++++
 .../offsets/oracle/structure1.res.oracle      |  20 ++
 .../offsets/oracle/structure2.res.oracle      |  17 ++
 .../offsets/oracle/structure3.res.oracle      |  31 +++
 .../offsets/oracle/structure4.res.oracle      |  22 ++
 .../offsets/oracle/structure5.res.oracle      |  46 ++++
 .../real_world/oracle/example1.res.oracle     | 174 ++++++++++++++
 .../real_world/oracle/example2.res.oracle     | 218 ++++++++++++++++++
 .../real_world/oracle/function1_v2.res.oracle |  24 ++
 src/plugins/alias/tests/test_config           |   2 +-
 49 files changed, 1421 insertions(+), 1 deletion(-)

diff --git a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
index 621a2379c08..79e61cb0b0a 100644
--- a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
@@ -2,17 +2,39 @@
 [alias] analysing function: main
 [alias] analysing instruction: a = & x;
 [alias] May-aliases after instruction  a = & x;  are  { *a; x }
+[alias] May-alias graph after instruction  a = & x;  is
+  0:{ a } → 1:{ x }   1:{ x } → 2:{  }
 [alias] analysing instruction: b = & y;
 [alias] May-aliases after instruction  b = & y;  are
   { *a; x }  { *b; y }  { *(*b); *y }
+[alias] May-alias graph after instruction  b = & y;  is
+  0:{ a } → 1:{ x }   1:{ x } → 2:{  }   6:{ b } → 7:{ y }
+  7:{ y } → 8:{  }   8:{  } → 9:{  }
 [alias] analysing instruction: y = & z;
 [alias] May-aliases after instruction  y = & z;  are
   { *a; x }  { *b; y }  { *(*b); *y; z }
+[alias] May-alias graph after instruction  y = & z;  is
+  0:{ a } → 1:{ x }   1:{ x } → 2:{  }   6:{ b } → 7:{ y }
+  7:{ y } → 8:{ z }   8:{ z } → 9:{  }
 [alias] analysing instruction: *y = x;
 [alias] May-aliases after instruction  *y = x;  are
   { *b; a; y }  { *(*b); *a; *y; x }
+[alias] May-alias graph after instruction  *y = x;  is
+  0:{ a } → 8:{ x }   6:{ b } → 7:{ y }   7:{ y } → 8:{ x }
+  8:{ x } → 9:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { *b; a; y }  { *(*b); *a; *y; x; z }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a } → 1:{ x; z }   1:{ x; z } → 2:{  }   6:{ b } → 7:{ y }
+  7:{ y } → 1:{ x; z }
 [alias] May-aliases at the end of function main:
   { *b; a; y }  { *(*b); *a; *y; x; z }
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 1:{ x; z }   1:{ x; z } → 2:{  }   6:{ b } → 7:{ y }
+  7:{ y } → 1:{ x; z }
+[alias] Summary of function main:
+  formals: 
+  locals: a→{ x; z }  b→{ y }  y→{ x; z }  x  z  p  __retres
+  returns: __retres    state: { *b; a; y }  { *(*b); *a; *y; x; z }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
index 0a62f46e5b1..4c31afc87e8 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -2,18 +2,33 @@
 [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: 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: b = c;
 [alias] May-aliases after instruction  b = c;  are  { a; b; c }
+[alias] May-alias graph after instruction  b = c;  is    0:{ a; b; c } → 1:{  }
 [alias] analysing instruction: a = d;
 [alias] May-aliases after instruction  a = d;  are  { a; b; c; d }
+[alias] May-alias graph after instruction  a = d;  is    0:{ a; b; c; d } → 1:{  }
 [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  __retres    returns: __retres
+  state: { a; b; c; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
index 02b7661040b..ee488debdbb 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -2,18 +2,37 @@
 [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: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  { *a; b }
+[alias] May-alias graph after instruction  *a = b;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{  }
 [alias] analysing instruction: *c = d;
 [alias] May-aliases after instruction  *c = d;  are  { *a; b }  { *c; d }
+[alias] May-alias graph after instruction  *c = d;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{  }   5:{ c } → 6:{ d }
+  6:{ d } → 7:{  }
 [alias] analysing instruction: a = c;
 [alias] May-aliases after instruction  a = c;  are  { a; c }  { *a; *c; b; d }
+[alias] May-alias graph after instruction  a = c;  is
+  0:{ a; c } → 1:{ b; d }   1:{ b; d } → 2:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; c }  { *a; *c; b; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; c } → 1:{ b; d }   1:{ b; d } → 2:{  }
 [alias] May-aliases at the end of function main: { a; c }  { *a; *c; b; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a; c } → 1:{ b; d }   1:{ b; d } → 2:{  }
+[alias] Summary of function main:
+  formals:     locals: a→{ b; d }  b  c→{ b; d }  d  __retres
+  returns: __retres    state: { a; c }  { *a; *c; b; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
index 38afe15b985..1a83b4c75ed 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -2,14 +2,28 @@
 [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 = 0;
 [alias] May-aliases after instruction  int b = 0;  are  <none>
+[alias] May-alias graph after instruction  int b = 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  <none>
+[alias] May-alias graph after instruction  a = & b;  is    0:{ a } → 1:{ b }
 [alias] analysing instruction: c = & b;
 [alias] May-aliases after instruction  c = & b;  are  { a; c }
+[alias] May-alias graph after instruction  c = & b;  is
+  0:{ a } → 5:{ b }   4:{ c } → 5:{ b }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; c }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a } → 5:{ b }   4:{ c } → 5:{ b }
 [alias] May-aliases at the end of function main: { a; c }
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 5:{ b }   4:{ c } → 5:{ b }
+[alias] Summary of function main:
+  formals:     locals: a→{ b }  b  c→{ b }  __retres
+  returns: __retres    state: { a; c }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
index 8d9d3556197..3dec6c8a3c9 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
@@ -2,18 +2,37 @@
 [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: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  { *a; b }
+[alias] May-alias graph after instruction  *a = b;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{  }
 [alias] analysing instruction: *c = d;
 [alias] May-aliases after instruction  *c = d;  are  { *a; b }  { *c; d }
+[alias] May-alias graph after instruction  *c = d;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{  }   5:{ c } → 6:{ d }
+  6:{ d } → 7:{  }
 [alias] analysing instruction: b = d;
 [alias] May-aliases after instruction  b = d;  are  { a; c }  { *a; *c; b; d }
+[alias] May-alias graph after instruction  b = d;  is
+  0:{ a } → 1:{ b; d }   1:{ b; d } → 2:{  }   5:{ c } → 1:{ b; d }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; c }  { *a; *c; b; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a } → 1:{ b; d }   1:{ b; d } → 2:{  }   5:{ c } → 1:{ b; d }
 [alias] May-aliases at the end of function main: { a; c }  { *a; *c; b; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 1:{ b; d }   1:{ b; d } → 2:{  }   5:{ c } → 1:{ b; d }
+[alias] Summary of function main:
+  formals:     locals: a→{ b; d }  b  c→{ b; d }  d  __retres
+  returns: __retres    state: { a; c }  { *a; *c; b; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
index d957cf1955d..21da14a9497 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
@@ -2,20 +2,38 @@
 [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: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  { *a; b }  { *(*a); *b }
+[alias] May-alias graph after instruction  *a = b;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{  }   2:{  } → 3:{  }
 [alias] analysing instruction: *b = c;
 [alias] May-aliases after instruction  *b = c;  are  { *a; b }  { *(*a); *b; c }
+[alias] May-alias graph after instruction  *b = c;  is
+  0:{ a } → 1:{ b }   1:{ b } → 2:{ c }   2:{ c } → 3:{  }
 [alias] analysing instruction: d = *(*a);
 [alias] May-aliases after instruction  d = *(*a);  are
   { *a; b }  { *(*a); *b; c; d }
+[alias] May-alias graph after instruction  d = *(*a);  is
+  0:{ a } → 1:{ b }   1:{ b } → 9:{ c; d }   9:{ c; d } → 10:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { *a; b }  { *(*a); *b; c; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a } → 1:{ b }   1:{ b } → 9:{ c; d }   9:{ c; d } → 10:{  }
 [alias] May-aliases at the end of function main: { *a; b }  { *(*a); *b; c; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 1:{ b }   1:{ b } → 9:{ c; d }   9:{ c; d } → 10:{  }
+[alias] Summary of function main:
+  formals:     locals: a→{ b }  b→{ c; d }  c  d  __retres
+  returns: __retres    state: { *a; b }  { *(*a); *b; c; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index 8a1dd1b9c58..2ff8f37ad86 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -2,18 +2,33 @@
 [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: float *c = (float *)0;
 [alias] May-aliases after instruction  float *c = (float *)0;  are  <none>
+[alias] May-alias graph after instruction  float *c = (float *)0;  is    <empty>
 [alias] analysing instruction: float *d = (float *)0;
 [alias] May-aliases after instruction  float *d = (float *)0;  are  <none>
+[alias] May-alias graph after instruction  float *d = (float *)0;  is    <empty>
 [alias] analysing instruction: a = (int *)c;
 [alias:unsafe-cast] cast1.c:10: Warning: unsafe cast from float * to int *
 [alias] May-aliases after instruction  a = (int *)c;  are  { a; c }
+[alias] May-alias graph after instruction  a = (int *)c;  is    0:{ a; c } → 1:{  }
 [alias] analysing instruction: d = (float *)b;
 [alias:unsafe-cast] cast1.c:11: Warning: unsafe cast from int * to float *
 [alias] May-aliases after instruction  d = (float *)b;  are  { a; c }  { b; d }
+[alias] May-alias graph after instruction  d = (float *)b;  is
+  0:{ a; c } → 1:{  }   4:{ b; d } → 5:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; c }  { b; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; c } → 1:{  }   4:{ b; d } → 5:{  }
 [alias] May-aliases at the end of function main: { a; c }  { b; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a; c } → 1:{  }   4:{ b; d } → 5:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  d  __retres    returns: __retres
+  state: { a; c }  { b; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
index 878ffd6070b..ede3b2e36f8 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -2,16 +2,30 @@
 [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: a = c;
 [alias] May-aliases after instruction  a = c;  are  { a; c }
+[alias] May-alias graph after instruction  a = c;  is    4:{ a; c } → 5:{  }
 [alias] analysing instruction: *a = 4;
 [alias] May-aliases after instruction  *a = 4;  are  { a; b; c }
+[alias] May-alias graph after instruction  *a = 4;  is    0:{ a; b; c } → 1:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b; c }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; b; c } → 1:{  }
 [alias] May-aliases at the end of function main: { a; b; c }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b; c } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  __retres    returns: __retres
+  state: { a; b; c }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle
index c50cd02e326..5972b2065a0 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle
@@ -2,18 +2,38 @@
 [alias] analysing function: main
 [alias] analysing instruction: b = & c;
 [alias] May-aliases after instruction  b = & c;  are  { *b; c }  { *(*b); *c }
+[alias] May-alias graph after instruction  b = & c;  is
+  0:{ b } → 1:{ c }   1:{ c } → 2:{  }   2:{  } → 3:{  }
 [alias] analysing instruction: c = & d;
 [alias] May-aliases after instruction  c = & d;  are  { *b; c }  { *(*b); *c; d }
+[alias] May-alias graph after instruction  c = & d;  is
+  0:{ b } → 1:{ c }   1:{ c } → 2:{ d }   2:{ d } → 3:{  }
 [alias] analysing instruction: d = & e;
 [alias] May-aliases after instruction  d = & e;  are  { *b; c }  { *(*b); *c; d }
+[alias] May-alias graph after instruction  d = & e;  is
+  0:{ b } → 1:{ c }   1:{ c } → 2:{ d }   2:{ d } → 3:{ e }
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are
   { a; b }  { *a; *b; c }  { *(*a); *(*b); *c; d }
+[alias] May-alias graph after instruction  a = b;  is
+  13:{ a; b } → 14:{ c }   14:{ c } → 15:{ d }   15:{ d } → 16:{ e }
 [alias] analysing instruction: a = & c;
 [alias] May-aliases after instruction  a = & c;  are
   { a; b }  { *a; *b; c }  { *(*a); *(*b); *c; d }
+[alias] May-alias graph after instruction  a = & c;  is
+  0:{ b } → 18:{ c }   17:{ a } → 18:{ c }   18:{ c } → 19:{ d }
+  19:{ d } → 20:{ e }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { a; b }  { *a; *b; c }  { *(*a); *(*b); *c; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  13:{ a; b } → 14:{ c }   14:{ c } → 15:{ d }   15:{ d } → 16:{ e }
 [alias] May-aliases at the end of function main:
   { a; b }  { *a; *b; c }  { *(*a); *(*b); *c; d }
+[alias] May-alias graph at the end of function main:
+  13:{ a; b } → 14:{ c }   14:{ c } → 15:{ d }   15:{ d } → 16:{ e }
+[alias] Summary of function main:
+  formals: 
+  locals: a→{ c }  b→{ c }  c→{ d }  d→{ e }  e  __retres
+  returns: __retres    state: { a; b }  { *a; *b; c }  { *(*a); *(*b); *c; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle
index 78497279d97..2bf30184b32 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle
@@ -3,39 +3,81 @@
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are
   { a; b }  { *a; *b }  { *(*a); *(*b) }  { *(*(*a)); *(*(*b)) }
+[alias] May-alias graph after instruction  a = b;  is
+  0:{ a; b } → 1:{  }   1:{  } → 2:{  }   2:{  } → 3:{  }
+  3:{  } → 4:{  }
 [alias] analysing instruction: b = & i;
 [alias] May-aliases after instruction  b = & i;  are
   { a; b }  { *a; *b; i }  { *(*a); *(*b); *i }  { *(*(*a)); *(*(*b)); *(*i) }
+[alias] May-alias graph after instruction  b = & i;  is
+  0:{ a; b } → 1:{ i }   1:{ i } → 2:{  }   2:{  } → 3:{  }
+  3:{  } → 4:{  }
 [alias] analysing instruction: i = & x;
 [alias] May-aliases after instruction  i = & x;  are
   { a; b }  { *a; *b; i }  { *(*a); *(*b); *i; x }
   { *(*(*a)); *(*(*b)); *(*i); *x }
+[alias] May-alias graph after instruction  i = & x;  is
+  0:{ a; b } → 1:{ i }   1:{ i } → 2:{ x }   2:{ x } → 3:{  }
+  3:{  } → 4:{  }
 [alias] analysing instruction: x = & t;
 [alias] May-aliases after instruction  x = & t;  are
   { a; b }  { *a; *b; i }  { *(*a); *(*b); *i; x }
   { *(*(*a)); *(*(*b)); *(*i); *x; t }
+[alias] May-alias graph after instruction  x = & t;  is
+  0:{ a; b } → 1:{ i }   1:{ i } → 2:{ x }   2:{ x } → 3:{ t }
+  3:{ t } → 4:{  }
 [alias] analysing instruction: a = c;
 [alias] May-aliases after instruction  a = c;  are
   { a; c }  { *a; *c }  { *(*a); *(*c) }  { *(*(*a)); *(*(*c)) }
+[alias] May-alias graph after instruction  a = c;  is
+  22:{ a; c } → 23:{  }   23:{  } → 24:{  }   24:{  } → 25:{  }
+  25:{  } → 26:{  }
 [alias] analysing instruction: c = & j;
 [alias] May-aliases after instruction  c = & j;  are
   { a; c }  { *a; *c; j }  { *(*a); *(*c); *j }  { *(*(*a)); *(*(*c)); *(*j) }
+[alias] May-alias graph after instruction  c = & j;  is
+  22:{ a; c } → 23:{ j }   23:{ j } → 24:{  }   24:{  } → 25:{  }
+  25:{  } → 26:{  }
 [alias] analysing instruction: j = & y;
 [alias] May-aliases after instruction  j = & y;  are
   { a; c }  { *a; *c; j }  { *(*a); *(*c); *j; y }
   { *(*(*a)); *(*(*c)); *(*j); *y }
+[alias] May-alias graph after instruction  j = & y;  is
+  22:{ a; c } → 23:{ j }   23:{ j } → 24:{ y }   24:{ y } → 25:{  }
+  25:{  } → 26:{  }
 [alias] analysing instruction: y = & u;
 [alias] May-aliases after instruction  y = & u;  are
   { a; c }  { *a; *c; j }  { *(*a); *(*c); *j; y }
   { *(*(*a)); *(*(*c)); *(*j); *y; u }
+[alias] May-alias graph after instruction  y = & u;  is
+  22:{ a; c } → 23:{ j }   23:{ j } → 24:{ y }   24:{ y } → 25:{ u }
+  25:{ u } → 26:{  }
 [alias] analysing instruction: p = 0;
 [alias] May-aliases after instruction  p = 0;  are
   { a; b; c }  { *a; *b; *c; i; j }  { *(*a); *(*b); *(*c); *i; *j; x; y }
   { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u }
+[alias] May-alias graph after instruction  p = 0;  is
+  0:{ a; b; c } → 1:{ i; j }   1:{ i; j } → 2:{ x; y }
+  2:{ x; y } → 3:{ t; u }   3:{ t; u } → 4:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { a; b; c }  { *a; *b; *c; i; j }  { *(*a); *(*b); *(*c); *i; *j; x; y }
   { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; b; c } → 1:{ i; j }   1:{ i; j } → 2:{ x; y }
+  2:{ x; y } → 3:{ t; u }   3:{ t; u } → 4:{  }
 [alias] May-aliases at the end of function main:
   { a; b; c }  { *a; *b; *c; i; j }  { *(*a); *(*b); *(*c); *i; *j; x; y }
   { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b; c } → 1:{ i; j }   1:{ i; j } → 2:{ x; y }
+  2:{ x; y } → 3:{ t; u }   3:{ t; u } → 4:{  }
+[alias] Summary of function main:
+  formals: 
+  locals: a→{ i; j }  b→{ i; j }  c→{ i; j }  i→{ x; y }  j→{ x; y }
+           x→{ t; u }  y→{ t; u }  t  u  p  __retres
+  returns: __retres
+  state: { a; b; c }  { *a; *b; *c; i; j }
+         { *(*a); *(*b); *(*c); *i; *j; x; y }
+         { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
index d97b433f717..53a681adaf7 100644
--- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
@@ -2,30 +2,62 @@
 [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: swap(a,b);
 [alias] analysing function: swap
 [alias] analysing instruction: int *z = (int *)0;
 [alias] May-aliases after instruction  int *z = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *z = (int *)0;  is    <empty>
 [alias] analysing instruction: z = x;
 [alias] May-aliases after instruction  z = x;  are  { x; z }
+[alias] May-alias graph after instruction  z = x;  is    0:{ x; z } → 1:{  }
 [alias] analysing instruction: x = y;
 [alias] May-aliases after instruction  x = y;  are  { x; y; z }
+[alias] May-alias graph after instruction  x = y;  is    0:{ x; y; z } → 1:{  }
 [alias] analysing instruction: y = z;
 [alias] May-aliases after instruction  y = z;  are  { x; y; z }
+[alias] May-alias graph after instruction  y = z;  is    0:{ x; y; z } → 1:{  }
 [alias] May-aliases at the end of function swap: { x; y; z }
+[alias] May-alias graph at the end of function swap:
+  0:{ x; y; z } → 1:{  }
+[alias] Summary of function swap:
+  formals: x  y    locals: z    returns: <none>    state: { x; y; z }
 [alias] May-aliases after instruction  swap(a,b);  are  { a; b }
+[alias] May-alias graph after instruction  swap(a,b);  is
+  8:{ a } → 7:{  }   10:{ b } → 7:{  }
 [alias] analysing instruction: swap(c,d);
 [alias] May-aliases after instruction  swap(c,d);  are  { a; b }  { c; d }
+[alias] May-alias graph after instruction  swap(c,d);  is
+  8:{ a } → 7:{  }   10:{ b } → 7:{  }   14:{ c } → 13:{  }
+  16:{ d } → 13:{  }
 [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
+  8:{ a } → 7:{  }   10:{ b } → 7:{  }   14:{ c } → 13:{  }
+  16:{ d } → 13:{  }
 [alias] May-aliases at the end of function main: { a; b }  { c; d }
+[alias] May-alias graph at the end of function main:
+  8:{ a } → 7:{  }   10:{ b } → 7:{  }   14:{ c } → 13:{  }
+  16:{ d } → 13:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  d  __retres    returns: __retres
+  state: { a; b }  { c; d }
 [alias] analysing function: swap
 [alias] analysing instruction: int *z = (int *)0;
 [alias] May-aliases after instruction  int *z = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *z = (int *)0;  is    <empty>
 [alias] May-aliases at the end of function swap: { x; y; z }
+[alias] May-alias graph at the end of function swap:
+  0:{ x; y; z } → 1:{  }
+[alias] Summary of function swap:
+  formals: x  y    locals: z    returns: <none>    state: { x; y; z }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function2.res.oracle b/src/plugins/alias/tests/basic/oracle/function2.res.oracle
index 1a770ac5390..8a156f682a6 100644
--- a/src/plugins/alias/tests/basic/oracle/function2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function2.res.oracle
@@ -2,23 +2,48 @@
 [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: a = my_malloc(2);
 [alias] analysing function: my_malloc
 [alias] analysing instruction: int *res = (int *)0;
 [alias] May-aliases after instruction  int *res = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *res = (int *)0;  is    <empty>
 [alias] analysing instruction: res = (int *)malloc((size_t)size);
 [alias] May-aliases after instruction  res = (int *)malloc((size_t)size);  are
   <none>
+[alias] May-alias graph after instruction  res = (int *)malloc((size_t)size);  is
+  0:{ res } → 1:{  }
 [alias] May-aliases at the end of function my_malloc: <none>
+[alias] May-alias graph at the end of function my_malloc:
+  0:{ res } → 1:{  }
+[alias] Summary of function my_malloc:
+  formals: size    locals: res    returns: res    state: <none>
 [alias] May-aliases after instruction  a = my_malloc(2);  are  <none>
+[alias] May-alias graph after instruction  a = my_malloc(2);  is
+  4:{ a } → 3:{  }
 [alias] analysing instruction: b = my_malloc(3);
 [alias] May-aliases after instruction  b = my_malloc(3);  are  <none>
+[alias] May-alias graph after instruction  b = my_malloc(3);  is
+  4:{ a } → 3:{  }   8:{ b } → 7:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is
+  4:{ a } → 3:{  }   8:{ b } → 7:{  }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  4:{ a } → 3:{  }   8:{ b } → 7:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  __retres    returns: __retres    state: <none>
 [alias] analysing function: my_malloc
 [alias] analysing instruction: int *res = (int *)0;
 [alias] May-aliases after instruction  int *res = (int *)0;  are  <none>
+[alias] May-alias graph after instruction  int *res = (int *)0;  is    <empty>
 [alias] May-aliases at the end of function my_malloc: <none>
+[alias] May-alias graph at the end of function my_malloc:
+  0:{ res } → 1:{  }
+[alias] Summary of function my_malloc:
+  formals: size    locals: res    returns: res    state: <none>
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function3.res.oracle b/src/plugins/alias/tests/basic/oracle/function3.res.oracle
index b45284aa949..4acd7896168 100644
--- a/src/plugins/alias/tests/basic/oracle/function3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function3.res.oracle
@@ -2,26 +2,56 @@
 [alias] analysing function: f1
 [alias] analysing instruction: int *tmp = x;
 [alias] May-aliases after instruction  int *tmp = x;  are  { x; tmp }
+[alias] May-alias graph after instruction  int *tmp = x;  is
+  0:{ x; tmp } → 1:{  }
 [alias] analysing instruction: x = y;
 [alias] May-aliases after instruction  x = y;  are  { x; y; tmp }
+[alias] May-alias graph after instruction  x = y;  is    0:{ x; y; tmp } → 1:{  }
 [alias] analysing instruction: y = tmp;
 [alias] May-aliases after instruction  y = tmp;  are  { x; y; tmp }
+[alias] May-alias graph after instruction  y = tmp;  is    0:{ x; y; tmp } → 1:{  }
 [alias] analysing instruction: __retres = (void *)0;
 [alias] May-aliases after instruction  __retres = (void *)0;  are  { x; y; tmp }
+[alias] May-alias graph after instruction  __retres = (void *)0;  is
+  0:{ x; y; tmp } → 1:{  }
 [alias] May-aliases at the end of function f1: { x; y; tmp }
+[alias] May-alias graph at the end of function f1:
+  0:{ x; y; tmp } → 1:{  }
+[alias] Summary of function f1:
+  formals: x  y    locals: tmp  __retres    returns: __retres
+  state: { x; y; tmp }
 [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: f1(a,b);
 [alias] May-aliases after instruction  f1(a,b);  are  { a; b }
+[alias] May-alias graph after instruction  f1(a,b);  is
+  16:{ a } → 9:{  }   18:{ b } → 9:{  }
 [alias] analysing instruction: f1(c,d);
 [alias] May-aliases after instruction  f1(c,d);  are  { a; b }  { c; d }
+[alias] May-alias graph after instruction  f1(c,d);  is
+  16:{ a } → 9:{  }   18:{ b } → 9:{  }   28:{ c } → 21:{  }
+  30:{ d } → 21:{  }
 [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
+  16:{ a } → 9:{  }   18:{ b } → 9:{  }   28:{ c } → 21:{  }
+  30:{ d } → 21:{  }
 [alias] May-aliases at the end of function main: { a; b }  { c; d }
+[alias] May-alias graph at the end of function main:
+  16:{ a } → 9:{  }   18:{ b } → 9:{  }   28:{ c } → 21:{  }
+  30:{ d } → 21:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  d  __retres    returns: __retres
+  state: { a; b }  { c; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function4.res.oracle b/src/plugins/alias/tests/basic/oracle/function4.res.oracle
index fb629f9683c..8dbe90ab465 100644
--- a/src/plugins/alias/tests/basic/oracle/function4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function4.res.oracle
@@ -1,17 +1,36 @@
 [kernel] Parsing function4.c (with preprocessing)
 [alias] analysing function: addr
 [alias] May-aliases at the end of function addr: <none>
+[alias] May-alias graph at the end of function addr:
+  <empty>
+[alias] Summary of function addr:
+  formals: x    locals:     returns: x    state: <none>
 [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 = 0;
 [alias] May-aliases after instruction  int c = 0;  are  <none>
+[alias] May-alias graph after instruction  int c = 0;  is    <empty>
 [alias] analysing instruction: a = addr(& c);
 [alias] May-aliases after instruction  a = addr(& c);  are  <none>
+[alias] May-alias graph after instruction  a = addr(& c);  is
+  4:{ a } → 3:{ c }   7:{  } → 3:{ c }
 [alias] analysing instruction: b = & c;
 [alias] May-aliases after instruction  b = & c;  are  { a; b }
+[alias] May-alias graph after instruction  b = & c;  is
+  4:{ a } → 9:{ c }   7:{  } → 9:{ c }   8:{ b } → 9:{ c }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  4:{ a } → 9:{ c }   7:{  } → 9:{ c }   8:{ b } → 9:{ c }
 [alias] May-aliases at the end of function main: { a; b }
+[alias] May-alias graph at the end of function main:
+  4:{ a } → 9:{ c }   7:{  } → 9:{ c }   8:{ b } → 9:{ c }
+[alias] Summary of function main:
+  formals:     locals: a→{ c }  b→{ c }  c  __retres
+  returns: __retres    state: { a; b }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function5.res.oracle b/src/plugins/alias/tests/basic/oracle/function5.res.oracle
index 53362c373d1..c7d33151e1a 100644
--- a/src/plugins/alias/tests/basic/oracle/function5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function5.res.oracle
@@ -2,20 +2,43 @@
 [alias] analysing function: choice
 [alias] analysing instruction: int c = 0;
 [alias] May-aliases after instruction  int c = 0;  are  <none>
+[alias] May-alias graph after instruction  int c = 0;  is    <empty>
 [alias] analysing instruction: __retres = x;
 [alias] May-aliases after instruction  __retres = x;  are  { x; __retres }
+[alias] May-alias graph after instruction  __retres = x;  is
+  0:{ x; __retres } → 1:{  }
 [alias] analysing instruction: __retres = y;
 [alias] May-aliases after instruction  __retres = y;  are  { y; __retres }
+[alias] May-alias graph after instruction  __retres = y;  is
+  4:{ y; __retres } → 5:{  }
 [alias] May-aliases at the end of function choice: { x; y; __retres }
+[alias] May-alias graph at the end of function choice:
+  0:{ x; y; __retres } → 1:{  }
+[alias] Summary of function choice:
+  formals: x  y    locals: c  __retres    returns: __retres
+  state: { x; y; __retres }
 [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: c = choice(a,b);
 [alias] May-aliases after instruction  c = choice(a,b);  are  { a; b; c }
+[alias] May-alias graph after instruction  c = choice(a,b);  is
+  10:{ c } → 9:{  }   12:{ a } → 9:{  }   14:{ b } → 9:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b; c }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  10:{ c } → 9:{  }   12:{ a } → 9:{  }   14:{ b } → 9:{  }
 [alias] May-aliases at the end of function main: { a; b; c }
+[alias] May-alias graph at the end of function main:
+  10:{ c } → 9:{  }   12:{ a } → 9:{  }   14:{ b } → 9:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  __retres    returns: __retres
+  state: { a; b; c }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function6.res.oracle b/src/plugins/alias/tests/basic/oracle/function6.res.oracle
index 4d8f8fa4a01..74f1dd62b95 100644
--- a/src/plugins/alias/tests/basic/oracle/function6.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function6.res.oracle
@@ -2,30 +2,54 @@
 [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: swap(a,b);
 [alias] analysing function: swap
 [alias] analysing instruction: int z = 0;
 [alias] May-aliases after instruction  int z = 0;  are  <none>
+[alias] May-alias graph after instruction  int z = 0;  is    <empty>
 [alias] analysing instruction: z = *x;
 [alias] May-aliases after instruction  z = *x;  are  <none>
+[alias] May-alias graph after instruction  z = *x;  is    <empty>
 [alias] analysing instruction: *x = *y;
 [alias] May-aliases after instruction  *x = *y;  are  <none>
+[alias] May-alias graph after instruction  *x = *y;  is    <empty>
 [alias] analysing instruction: *y = z;
 [alias] May-aliases after instruction  *y = z;  are  <none>
+[alias] May-alias graph after instruction  *y = z;  is    <empty>
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
 [alias] May-aliases after instruction  swap(a,b);  are  <none>
+[alias] May-alias graph after instruction  swap(a,b);  is    <empty>
 [alias] analysing instruction: swap(c,d);
 [alias] May-aliases after instruction  swap(c,d);  are  <none>
+[alias] May-alias graph after instruction  swap(c,d);  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: a  b  c  d  __retres    returns: __retres
+  state: <none>
 [alias] analysing function: swap
 [alias] analysing instruction: int z = 0;
 [alias] May-aliases after instruction  int z = 0;  are  <none>
+[alias] May-alias graph after instruction  int z = 0;  is    <empty>
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
index 64f2826db29..e5df545b132 100644
--- a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
@@ -2,18 +2,33 @@
 [alias] analysing function: f
 [alias] analysing instruction: int y = 0;
 [alias] May-aliases after instruction  int y = 0;  are  <none>
+[alias] May-alias graph after instruction  int y = 0;  is    <empty>
 [alias] analysing instruction: *x = y;
 [alias] May-aliases after instruction  *x = y;  are  <none>
+[alias] May-alias graph after instruction  *x = y;  is    <empty>
 [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: 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: f(a);
 [alias] May-aliases after instruction  f(a);  are  <none>
+[alias] May-alias graph after instruction  f(a);  is    <empty>
 [alias] analysing instruction: f(b);
 [alias] May-aliases after instruction  f(b);  are  <none>
+[alias] May-alias graph after instruction  f(b);  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: a  b  __retres    returns: __retres    state: <none>
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/loop.res.oracle b/src/plugins/alias/tests/basic/oracle/loop.res.oracle
index 5c9a393a033..74cdba557c8 100644
--- a/src/plugins/alias/tests/basic/oracle/loop.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/loop.res.oracle
@@ -2,18 +2,37 @@
 [alias] analysing function: main
 [alias] analysing instruction: int l[1] = {0};
 [alias] May-aliases after instruction  int l[1] = {0};  are  <none>
+[alias] May-alias graph after instruction  int l[1] = {0};  is    <empty>
 [alias] analysing instruction: int *n_0 = & l[1];
 [alias] May-aliases after instruction  int *n_0 = & l[1];  are  { l; n_0 }
+[alias] May-alias graph after instruction  int *n_0 = & l[1];  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias] analysing instruction: n_0 = & l[1] + 0;
 [alias] May-aliases after instruction  n_0 = & l[1] + 0;  are  { l; n_0 }
+[alias] May-alias graph after instruction  n_0 = & l[1] + 0;  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias] analysing instruction: int w = 0;
 [alias] May-aliases after instruction  int w = 0;  are  { l; n_0 }
+[alias] May-alias graph after instruction  int w = 0;  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias] analysing instruction: l[0] = *(& l[1] + 0);
 [alias] May-aliases after instruction  l[0] = *(& l[1] + 0);  are  { l; n_0 }
+[alias] May-alias graph after instruction  l[0] = *(& l[1] + 0);  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias] analysing instruction: int l[1] = {0};
 [alias] May-aliases after instruction  int l[1] = {0};  are  { l; n_0 }
+[alias] May-alias graph after instruction  int l[1] = {0};  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias] analysing instruction: int *n_0 = & l[1];
 [alias] May-aliases after instruction  int *n_0 = & l[1];  are  { l; n_0 }
+[alias] May-alias graph after instruction  int *n_0 = & l[1];  is
+  0:{ n_0 } → 1:{  }   2:{ l } → 1:{  }
 [alias:no-return] loop.c:4: Warning: 
   function main does not return; analysis may be unsound
 [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: l  n_0  w  __retres    returns: __retres
+  state: <none>
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
index cd2646bd316..61305c305a0 100644
--- a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
@@ -2,16 +2,40 @@
 [alias] analysing function: main
 [alias] analysing instruction: a = & x;
 [alias] May-aliases after instruction  a = & x;  are  <none>
+[alias] May-alias graph after instruction  a = & x;  is    0:{ a } → 1:{ x }
 [alias] analysing instruction: b = & y;
 [alias] May-aliases after instruction  b = & y;  are  { *b; y }
+[alias] May-alias graph after instruction  b = & y;  is
+  0:{ a } → 1:{ x }   4:{ b } → 5:{ y }   5:{ y } → 6:{  }
 [alias] analysing instruction: y = & z;
 [alias] May-aliases after instruction  y = & z;  are  { *b; y }
+[alias] May-alias graph after instruction  y = & z;  is
+  0:{ a } → 1:{ x }   4:{ b } → 5:{ y }   5:{ y } → 6:{ z }
 [alias] analysing instruction: y = & x;
 [alias] May-aliases after instruction  y = & x;  are  { *b; a; y }
+[alias] May-alias graph after instruction  y = & x;  is
+  0:{ a } → 6:{ x }   4:{ b } → 5:{ y }   5:{ y } → 6:{ x }
 [alias] analysing instruction: c = & y;
 [alias] May-aliases after instruction  c = & y;  are  { b; c }  { *b; *c; a; y }
+[alias] May-alias graph after instruction  c = & y;  is
+  0:{ a } → 15:{ x; z }   4:{ b } → 14:{ y }   13:{ c } → 14:{ y }
+  14:{ y } → 15:{ x; z }
 [alias] analysing instruction: *y = 4;
 [alias] May-aliases after instruction  *y = 4;  are  { b; c }  { *b; *c; a; y }
+[alias] May-alias graph after instruction  *y = 4;  is
+  0:{ a } → 15:{ x; z }   4:{ b } → 14:{ y }   13:{ c } → 14:{ y }
+  14:{ y } → 15:{ x; z }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { b; c }  { *b; *c; a; y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a } → 15:{ x; z }   4:{ b } → 14:{ y }   13:{ c } → 14:{ y }
+  14:{ y } → 15:{ x; z }
 [alias] May-aliases at the end of function main: { b; c }  { *b; *c; a; y }
+[alias] May-alias graph at the end of function main:
+  0:{ a } → 15:{ x; z }   4:{ b } → 14:{ y }   13:{ c } → 14:{ y }
+  14:{ y } → 15:{ x; z }
+[alias] Summary of function main:
+  formals: 
+  locals: a→{ x; z }  b→{ y }  c→{ y }  y→{ x; z }  x  z  p  __retres
+  returns: __retres    state: { b; c }  { *b; *c; a; y }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
index 1d3c1881fa9..5d4e7565c29 100644
--- a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
@@ -2,18 +2,35 @@
 [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: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b; d }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ a; b; d } → 1:{  }
 [alias] May-aliases at the end of function main: { a; b; d }
+[alias] May-alias graph at the end of function main:
+  0:{ a; b; d } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  c  d  e  __retres    returns: __retres
+  state: { a; b; d }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
index 8097b1a0db5..35c8cb7b5d7 100644
--- a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
index aa1b0b711b2..c389176d8e7 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -2,14 +2,27 @@
 [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] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
index c7c4c865fea..d6cd6b220b4 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
index 40720eb3def..24560b86f6e 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle
index 17322d69dee..632370a683e 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle
@@ -2,13 +2,33 @@
 [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:{ t }   1:{ t } → 2:{  }
 [alias] analysing instruction: *z = t + (*z - *x);
 [alias] May-aliases after instruction  *z = t + (*z - *x);  are
   { y; z }  { *y; *z; t }
+[alias] May-alias graph after instruction  *z = t + (*z - *x);  is
+  0:{ y } → 6:{ t }   5:{ z } → 6:{ t }   6:{ t } → 7:{  }
 [alias] analysing instruction: *x = t;
 [alias] May-aliases after instruction  *x = t;  are  { x; y; z }  { *x; *y; *z; t }
+[alias] May-alias graph after instruction  *x = t;  is
+  0:{ y } → 9:{ t }   5:{ z } → 9:{ t }   8:{ x } → 9:{ t }
+  9:{ t } → 10:{  }
 [alias] May-aliases at the end of function f: { x; y; z }  { *x; *y; *z; t }
+[alias] May-alias graph at the end of function f:
+  0:{ y } → 9:{ t }   5:{ z } → 9:{ t }   8:{ x } → 9:{ t }
+  9:{ t } → 10:{  }
+[alias] Summary of function f:
+  formals: x→{ t }  y→{ t }  z→{ t }    locals: t    returns: <none>
+  state: { x; y; z }  { *x; *y; *z; t }
 [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
+  20:{  } → 21:{  }   22:{ a } → 20:{  }
 [alias] May-aliases at the end of function g: <none>
+[alias] May-alias graph at the end of function g:
+  20:{  } → 21:{  }   22:{ a } → 20:{  }
+[alias] Summary of function g:
+  formals: a    locals:     returns: <none>    state: <none>
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle
index 6c8a3e49e6b..c9b292917e6 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle
+++ b/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  { prev; p }
+[alias] May-alias graph after instruction  p = & prev[1] + (int)*p;  is
+  0:{ p } → 1:{  }   2:{ prev } → 1:{  }
 [alias] analysing instruction: p = & prev[*p];
 [alias] May-aliases after instruction  p = & prev[*p];  are  { prev; p }
+[alias] May-alias graph after instruction  p = & prev[*p];  is
+  5:{ p } → 6:{  }   7:{ prev } → 6:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { prev; p }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ p } → 1:{  }   2:{ prev } → 1:{  }
 [alias] May-aliases at the end of function main: { prev; p }
+[alias] May-alias graph at the end of function main:
+  0:{ p } → 1:{  }   2:{ prev } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: __retres  prev  p  tmp_0    returns: __retres
+  state: { prev; p }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
index 3e3db5ff9b0..f3a0e1ed656 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
@@ -4,12 +4,23 @@
 [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[0..].t; tmp }
+[alias] May-alias graph after instruction  tmp = (void (*)(void))*((char *)(v.t));
+  is    0:{ tmp } → 1:{ f }   4:{ v } -t→ 5:{  }   5:{  } → 0:{ tmp }
 [alias] analysing instruction: int g = (int)tmp;
 [alias:unsafe-cast] origin.c:8: Warning: unsafe cast from void (*)(void) to int
 [alias] May-aliases after instruction  int g = (int)tmp;  are  { v[0..].t; tmp }
+[alias] May-alias graph after instruction  int g = (int)tmp;  is
+  0:{ tmp } → 1:{ f }   4:{ v } -t→ 5:{  }   5:{  } → 0:{ tmp }
 [alias] May-aliases at the end of function f: { v[0..].t; tmp }
+[alias] May-alias graph at the end of function f:
+  0:{ tmp } → 1:{ f }   4:{ v } -t→ 5:{  }   5:{  } → 0:{ tmp }
+[alias] Summary of function f:
+  formals:     locals: g  tmp→{ f }    returns: <none>
+  state: { v[0..].t; tmp }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
index 4d14eae5cf9..d2f26b8474a 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
@@ -5,4 +5,11 @@
 [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[0..]; tmp }
+[alias] May-alias graph after instruction  tmp = (void *)*((int *)(t));  is
+  0:{ tmp } → 1:{  }   2:{ t } → 0:{ tmp }
 [alias] May-aliases at the end of function f: { t[0..]; tmp }
+[alias] May-alias graph at the end of function f:
+  0:{ tmp } → 1:{  }   2:{ t } → 0:{ tmp }
+[alias] Summary of function f:
+  formals:     locals: tmp    returns: <none>    state: { t[0..]; tmp }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
index bdc3f9de654..14786295a9e 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
@@ -1,12 +1,22 @@
 [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
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle
index 7843cab1557..6718bf0c370 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
index 7ea35d5b5b0..d26bef08517 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
@@ -3,19 +3,41 @@
 [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:{ s3 }   11:{ s3 } → 12:{  }
 [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:{  }   13:{ key } → 14:{ s2 }   14:{ s2 } → 15:{  }
 [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:{ s2; s3 } → 3:{  }   10:{ key } → 4:{ s2; s3 }
+[alias] Summary of function CPS_ParseKey:
+  formals:     locals: 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
diff --git a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
index 129439b988a..ed3c157e85e 100644
--- a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
+++ b/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  { tab; x }
+[alias] May-alias graph after instruction  int *x = & tab[1];  is
+  0:{ x } → 1:{  }   2:{ tab } → 1:{  }
 [alias] analysing instruction: int *y = & tab[2];
 [alias] May-aliases after instruction  int *y = & tab[2];  are  { tab; x; y }
+[alias] May-alias graph after instruction  int *y = & tab[2];  is
+  0:{ x } → 6:{  }   2:{ tab } → 6:{  }   5:{ y } → 6:{  }
 [alias] analysing instruction: tab[3] = *x + *y;
 [alias] May-aliases after instruction  tab[3] = *x + *y;  are  { tab; x; y }
+[alias] May-alias graph after instruction  tab[3] = *x + *y;  is
+  0:{ x } → 6:{  }   2:{ tab } → 6:{  }   5:{ y } → 6:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { tab; x; y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ x } → 6:{  }   2:{ tab } → 6:{  }   5:{ y } → 6:{  }
 [alias] May-aliases at the end of function main: { tab; x; y }
+[alias] May-alias graph at the end of function main:
+  0:{ x } → 6:{  }   2:{ tab } → 6:{  }   5:{ y } → 6:{  }
+[alias] Summary of function main:
+  formals:     locals: tab  x  y  __retres    returns: __retres
+  state: { tab; x; y }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
index 1e9417d8042..cf84f25b94e 100644
--- a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
@@ -2,15 +2,29 @@
 [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
   { mat; x }  { *x; mat[0..] }
+[alias] May-alias graph after instruction  *x = mat[1];  is
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ mat } → 1:{  }
 [alias] analysing instruction: *y = *(*(x + 0));
 [alias] May-aliases after instruction  *y = *(*(x + 0));  are
   { mat; x }  { *x; mat[0..] }
+[alias] May-alias graph after instruction  *y = *(*(x + 0));  is
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ mat } → 1:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { mat; x }  { *x; mat[0..] }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ mat } → 1:{  }
 [alias] May-aliases at the end of function main: { mat; x }  { *x; mat[0..] }
+[alias] May-alias graph at the end of function main:
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ mat } → 1:{  }
+[alias] Summary of function main:
+  formals:     locals: mat  x  y  __retres    returns: __retres
+  state: { mat; x }  { *x; mat[0..] }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
index baf0207ce25..471e5d1851c 100644
--- a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
@@ -3,13 +3,30 @@
 [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  { mat[0..]; x }
+[alias] May-alias graph after instruction  x = mat[0];  is
+  0:{ x } → 1:{  }   2:{ y } → 3:{  }   4:{ mat } → 0:{ x }
 [alias] analysing instruction: y = mat[1];
 [alias] May-aliases after instruction  y = mat[1];  are  { mat[0..]; x; y }
+[alias] May-alias graph after instruction  y = mat[1];  is
+  2:{ x; y } → 3:{  }   4:{ mat } → 2:{ x; y }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { mat[0..]; x; y }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  2:{ x; y } → 3:{  }   4:{ mat } → 2:{ x; y }
 [alias] May-aliases at the end of function main: { mat[0..]; x; y }
+[alias] May-alias graph at the end of function main:
+  2:{ x; y } → 3:{  }   4:{ mat } → 2:{ x; y }
+[alias] Summary of function main:
+  formals:     locals: mat→{ x; y }  x  y  __retres    returns: __retres
+  state: { mat[0..]; x; y }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
index 9b588f2f8f2..e4249a441ad 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
index 34b8bd11975..07d8fde2b7c 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
index 4193c3f90a2..225de1d3417 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle b/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle
index a8dd965bbd8..5e6496f281b 100644
--- a/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle
@@ -2,59 +2,138 @@
 [alias] analysing function: jfla
 [alias] analysing instruction: *snd = *fst;
 [alias] May-aliases after instruction  *snd = *fst;  are  <none>
+[alias] May-alias graph after instruction  *snd = *fst;  is    <empty>
 [alias] analysing instruction: fst = *i1;
 [alias] May-aliases after instruction  fst = *i1;  are  { *i1; fst }
+[alias] May-alias graph after instruction  fst = *i1;  is
+  0:{ fst } → 1:{  }   2:{ i1 } → 0:{ fst }
 [alias] analysing instruction: __retres = *i2;
 [alias] May-aliases after instruction  __retres = *i2;  are
   { *i1; fst }  { *i2; __retres }
+[alias] May-alias graph after instruction  __retres = *i2;  is
+  0:{ fst } → 1:{  }   2:{ i1 } → 0:{ fst }   5:{ __retres } → 6:{  }
+  7:{ i2 } → 5:{ __retres }
 [alias] analysing instruction: fst = *i2;
 [alias] May-aliases after instruction  fst = *i2;  are  { *i2; fst }
+[alias] May-alias graph after instruction  fst = *i2;  is
+  10:{ fst } → 11:{  }   12:{ i2 } → 10:{ fst }
 [alias] analysing instruction: __retres = *i1;
 [alias] May-aliases after instruction  __retres = *i1;  are
   { *i2; fst }  { *i1; __retres }
+[alias] May-alias graph after instruction  __retres = *i1;  is
+  10:{ fst } → 11:{  }   12:{ i2 } → 10:{ fst }
+  15:{ __retres } → 16:{  }   17:{ i1 } → 15:{ __retres }
 [alias] May-aliases at the end of function jfla:
   { i1; i2 }  { *i1; *i2; fst; __retres }
+[alias] May-alias graph at the end of function jfla:
+  0:{ fst; __retres } → 1:{  }   2:{ i1 } → 0:{ fst; __retres }
+  7:{ i2 } → 0:{ fst; __retres }
+[alias] Summary of function jfla:
+  formals: fst  snd  i1→{ fst; __retres }  i2→{ fst; __retres }  bo
+  locals: __retres    returns: __retres
+  state: { i1; i2 }  { *i1; *i2; fst; __retres }
 [alias] analysing function: main
 [alias] analysing instruction: int u = 11;
 [alias] May-aliases after instruction  int u = 11;  are  <none>
+[alias] May-alias graph after instruction  int u = 11;  is    <empty>
 [alias] analysing instruction: int v = 12;
 [alias] May-aliases after instruction  int v = 12;  are  <none>
+[alias] May-alias graph after instruction  int v = 12;  is    <empty>
 [alias] analysing instruction: int t[3] = {0, 1, 2};
 [alias] May-aliases after instruction  int t[3] = {0, 1, 2};  are  <none>
+[alias] May-alias graph after instruction  int t[3] = {0, 1, 2};  is    <empty>
 [alias] analysing instruction: int *a = & t[1];
 [alias] May-aliases after instruction  int *a = & t[1];  are  { t; a }
+[alias] May-alias graph after instruction  int *a = & t[1];  is
+  20:{ a } → 21:{  }   22:{ t } → 21:{  }
 [alias] analysing instruction: int *b = & u;
 [alias] May-aliases after instruction  int *b = & u;  are  { t; a }
+[alias] May-alias graph after instruction  int *b = & u;  is
+  20:{ a } → 21:{  }   22:{ t } → 21:{  }   25:{ b } → 26:{ u }
 [alias] analysing instruction: int *c = & v;
 [alias] May-aliases after instruction  int *c = & v;  are  { t; a }
+[alias] May-alias graph after instruction  int *c = & v;  is
+  20:{ a } → 21:{  }   22:{ t } → 21:{  }   25:{ b } → 26:{ u }
+  29:{ c } → 30:{ v }
 [alias] analysing instruction: int **x = & a;
 [alias] May-aliases after instruction  int **x = & a;  are  { *x; t; a }
+[alias] May-alias graph after instruction  int **x = & a;  is
+  22:{ t } → 35:{  }   25:{ b } → 26:{ u }   29:{ c } → 30:{ v }
+  33:{ x } → 34:{ a }   34:{ a } → 35:{  }
 [alias] analysing instruction: int **y = & b;
 [alias] May-aliases after instruction  int **y = & b;  are  { *x; t; a }  { *y; b }
+[alias] May-alias graph after instruction  int **y = & b;  is
+  22:{ t } → 35:{  }   29:{ c } → 30:{ v }   33:{ x } → 34:{ a }
+  34:{ a } → 35:{  }   37:{ y } → 38:{ b }   38:{ b } → 39:{ u }
 [alias] analysing instruction: int **z = & c;
 [alias] May-aliases after instruction  int **z = & c;  are
   { *x; t; a }  { *y; b }  { *z; c }
+[alias] May-alias graph after instruction  int **z = & c;  is
+  22:{ t } → 35:{  }   33:{ x } → 34:{ a }   34:{ a } → 35:{  }
+  37:{ y } → 38:{ b }   38:{ b } → 39:{ u }   41:{ z } → 42:{ c }
+  42:{ c } → 43:{ v }
 [alias] analysing instruction: struct str_t s = {.fst = c, .snd = t};
 [alias] May-aliases after instruction  struct str_t s = {.fst = c, .snd = t};  are
   { *x; t; a; s.snd }  { *y; b }  { *z; c; s.fst }
+[alias] May-alias graph after instruction  struct str_t s = {.fst = c, .snd = t};
+  is
+  33:{ x } → 34:{ a }   34:{ a } → 35:{  }   37:{ y } → 38:{ b }
+  38:{ b } → 39:{ u }   41:{ z } → 46:{ c }   45:{ s } -fst→ 46:{ c }
+  45:{ s } -snd→ 47:{ t }   46:{ c } → 43:{ v }   47:{ t } → 35:{  }
 [alias] analysing instruction: struct str_t *s1 = & s;
 [alias] May-aliases after instruction  struct str_t *s1 = & s;  are
   { *x; s1->snd; t; a; s.snd }  { *y; b }  { *z; s1->fst; c; s.fst }
+[alias] May-alias graph after instruction  struct str_t *s1 = & s;  is
+  33:{ x } → 34:{ a }   34:{ a } → 35:{  }   37:{ y } → 38:{ b }
+  38:{ b } → 39:{ u }   41:{ z } → 46:{ c }   46:{ c } → 43:{ v }
+  47:{ t } → 35:{  }   48:{ s1 } → 49:{ s }   49:{ s } -fst→ 46:{ c }
+  49:{ s } -snd→ 47:{ t }
 [alias] analysing instruction: struct str_t *s2 = & s;
 [alias] May-aliases after instruction  struct str_t *s2 = & s;  are
   { *x; s1->snd; s2->snd; t; a; s.snd }  { *y; b }
   { *z; s1->fst; s2->fst; c; s.fst }  { s1; s2 }
+[alias] May-alias graph after instruction  struct str_t *s2 = & s;  is
+  33:{ x } → 34:{ a }   34:{ a } → 35:{  }   37:{ y } → 38:{ b }
+  38:{ b } → 39:{ u }   41:{ z } → 46:{ c }   46:{ c } → 43:{ v }
+  47:{ t } → 35:{  }   48:{ s1 } → 52:{ s }   51:{ s2 } → 52:{ s }
+  52:{ s } -fst→ 46:{ c }   52:{ s } -snd→ 47:{ t }
 [alias] analysing instruction: c = jfla(s1->fst,s1->snd,x,y,0);
 [alias] May-aliases after instruction  c = jfla(s1->fst,s1->snd,x,y,0);  are
   { x; y }
   { *x; *y; *z; s1->fst; s1->snd; s2->fst; s2->snd; t; a; b; c; s.fst; s.snd }
   { s1; s2 }
+[alias] May-alias graph after instruction  c = jfla(s1->fst,s1->snd,x,y,0);  is
+  33:{ x } → 34:{ a; b }   34:{ a; b } → 35:{ u; v }
+  37:{ y } → 34:{ a; b }   41:{ z } → 46:{ c }   46:{ c } → 35:{ u; v }
+  47:{ t } → 35:{ u; v }   48:{ s1 } → 52:{ s }   51:{ s2 } → 52:{ s }
+  52:{ s } -fst→ 46:{ c }   52:{ s } -snd→ 47:{ t }
 [alias] analysing instruction: a = jfla(s2->fst,s2->snd,y,z,1);
 [alias] May-aliases after instruction  a = jfla(s2->fst,s2->snd,y,z,1);  are
   { x; y; z }
   { *x; *y; *z; s1->fst; s1->snd; s2->fst; s2->snd; t; a; b; c; s.fst; s.snd }
   { s1; s2 }
+[alias] May-alias graph after instruction  a = jfla(s2->fst,s2->snd,y,z,1);  is
+  33:{ x } → 34:{ a; b; c }   34:{ a; b; c } → 35:{ u; v }
+  37:{ y } → 34:{ a; b; c }   41:{ z } → 34:{ a; b; c }
+  47:{ t } → 35:{ u; v }   48:{ s1 } → 52:{ s }   51:{ s2 } → 52:{ s }
+  52:{ s } -fst→ 34:{ a; b; c }   52:{ s } -snd→ 47:{ t }
 [alias] May-aliases at the end of function main:
   { x; y; z }
   { *x; *y; *z; s1->fst; s1->snd; s2->fst; s2->snd; t; a; b; c; s.fst; s.snd }
   { s1; s2 }
+[alias] May-alias graph at the end of function main:
+  33:{ x } → 34:{ a; b; c }   34:{ a; b; c } → 35:{ u; v }
+  37:{ y } → 34:{ a; b; c }   41:{ z } → 34:{ a; b; c }
+  47:{ t } → 35:{ u; v }   48:{ s1 } → 52:{ s }   51:{ s2 } → 52:{ s }
+  52:{ s } -fst→ 34:{ a; b; c }   52:{ s } -snd→ 47:{ t }
+[alias] Summary of function main:
+  formals: 
+  locals: u  v  t→{ u; v }  a→{ u; v }  b→{ u; v }  c→{ u; v }
+           x→{ a; b; c }  y→{ a; b; c }  z→{ a; b; c }  s  s1→{ s }
+           s2→{ s }
+  returns: <none>
+  state: { x; y; z }
+         { *x; *y; *z; s1->fst; s1->snd; s2->fst; s2->snd; t; a; b; c; 
+           s.fst; s.snd }
+         { s1; s2 }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
index 081d7931334..205196a3f3b 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
@@ -2,59 +2,140 @@
 [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 } → 1:{  }   1:{  } → 2:{ 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 } → 1:{  }   1:{  } → 2:{ 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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }   13:{ a } → 14:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }   13:{ a } → 14:{  }
+  15:{ b } → 16:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }   13:{ a } → 14:{  }
+  15:{ b } → 16:{  }
 [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 } → 1:{  }   1:{  } → 2:{ x1; x2 }   7:{ z1 } → 8:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }   13:{ a } → 14:{  }
+  15:{ b } → 16:{  }
 [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
+  0:{ tab_y } → 17:{  }   7:{ z1 } → 8:{  }   8:{  } -s→ 17:{  }
+  9:{ z2 } → 10:{  }   11:{ t } → 12:{  }   13:{ a } → 14:{  }
+  15:{ b } → 16:{  }   17:{  } → 2:{ 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
+  0:{ tab_y } → 18:{  }   7:{ z1 } → 8:{  }   8:{  } -s→ 18:{  }
+  9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }   11:{ t } → 12:{  }
+  13:{ a } → 14:{  }   15:{ b } → 16:{  }   18:{  } → 2:{ 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
+  0:{ tab_y } → 18:{  }   7:{ z1 } → 8:{  }   8:{  } -s→ 18:{  }
+  8:{  } -c→ 19:{ a }   9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }
+  11:{ t } → 12:{  }   15:{ b } → 16:{  }   18:{  } → 2:{ x1; x2 }
+  19:{ a } → 14:{  }
 [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
+  0:{ tab_y } → 18:{  }   7:{ z1 } → 8:{  }   8:{  } -s→ 18:{  }
+  8:{  } -c→ 19:{ a }   9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }
+  10:{  } -c→ 20:{ b }   11:{ t } → 12:{  }   18:{  } → 2:{ x1; x2 }
+  19:{ a } → 14:{  }   20:{ b } → 16:{  }
 [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
   { (t->t)->s; z1->s; z2->s; tab_y[0..] }  { t->t; z1 }
   { (t->t)->c; z1->c; a }  { z2->c; b }
+[alias] May-alias graph after instruction  t->t = (struct struct_2_t *)z1;  is
+  0:{ tab_y } → 18:{  }   8:{  } -s→ 18:{  }   8:{  } -c→ 19:{ a }
+  9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }   10:{  } -c→ 20:{ b }
+  11:{ t } → 12:{  }   12:{  } -t→ 21:{ z1 }   18:{  } → 2:{ x1; x2 }
+  19:{ a } → 14:{  }   20:{ b } → 16:{  }   21:{ z1 } → 8:{  }
 [alias] analysing instruction: t->d = a;
 [alias] May-aliases after instruction  t->d = a;  are
   { (t->t)->s; z1->s; z2->s; tab_y[0..] }  { t->t; z1 }
   { (t->t)->c; z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph after instruction  t->d = a;  is
+  0:{ tab_y } → 18:{  }   8:{  } -s→ 18:{  }   8:{  } -c→ 22:{ a }
+  9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }   10:{  } -c→ 20:{ b }
+  11:{ t } → 12:{  }   12:{  } -t→ 21:{ z1 }   12:{  } -d→ 22:{ a }
+  18:{  } → 2:{ x1; x2 }   20:{ b } → 16:{  }   21:{ z1 } → 8:{  }
+  22:{ a } → 14:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { (t->t)->s; z1->s; z2->s; tab_y[0..] }  { t->t; z1 }
   { (t->t)->c; z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ tab_y } → 18:{  }   8:{  } -s→ 18:{  }   8:{  } -c→ 22:{ a }
+  9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }   10:{  } -c→ 20:{ b }
+  11:{ t } → 12:{  }   12:{  } -t→ 21:{ z1 }   12:{  } -d→ 22:{ a }
+  18:{  } → 2:{ x1; x2 }   20:{ b } → 16:{  }   21:{ z1 } → 8:{  }
+  22:{ a } → 14:{  }
 [alias] May-aliases at the end of function main:
   { (t->t)->s; z1->s; z2->s; tab_y[0..] }  { t->t; z1 }
   { (t->t)->c; z1->c; t->d; a }  { z2->c; b }
+[alias] May-alias graph at the end of function main:
+  0:{ tab_y } → 18:{  }   8:{  } -s→ 18:{  }   8:{  } -c→ 22:{ a }
+  9:{ z2 } → 10:{  }   10:{  } -s→ 18:{  }   10:{  } -c→ 20:{ b }
+  11:{ t } → 12:{  }   12:{  } -t→ 21:{ z1 }   12:{  } -d→ 22:{ a }
+  18:{  } → 2:{ x1; x2 }   20:{ b } → 16:{  }   21:{ z1 } → 8:{  }
+  22:{ a } → 14:{  }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  tab_y  z1  z2  t  a  b  __retres
+  returns: __retres
+  state: { (t->t)->s; z1->s; z2->s; tab_y[0..] }  { t->t; z1 }
+         { (t->t)->c; z1->c; t->d; a }  { z2->c; b }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
index a34b8a8f522..c141c4f0975 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -2,44 +2,89 @@
 [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:{  }   1:{  } -s→ 6:{  }   2:{ t } → 3:{  }
+  4:{ a } → 5:{  }   6:{  } → 7:{  }   7:{  } → 8:{ 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:{  }   1:{  } -s→ 6:{  }   2:{ t } → 3:{  }
+  4:{ a } → 5:{  }   6:{  } → 7:{  }   7:{  } → 8:{ 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:{  }   1:{  } -s→ 6:{  }   1:{  } -c→ 12:{ a }
+  2:{ t } → 3:{  }   6:{  } → 7:{  }   7:{  } → 8:{ x1; x2 }
+  12:{ 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 }  { (t->t)->c; z1->c; a }  { (t->t)->s; z1->s }
   { (*(t->t))[0..].s; (*z1)[0..].s }
+[alias] May-alias graph after instruction  t->t = (struct struct_2_t *)z1;  is
+  1:{  } -s→ 6:{  }   1:{  } -c→ 12:{ a }   2:{ t } → 3:{  }
+  3:{  } -t→ 13:{ z1 }   6:{  } → 7:{  }   7:{  } → 8:{ x1; x2 }
+  12:{ a } → 5:{  }   13:{ z1 } → 1:{  }
 [alias] analysing instruction: t->d = a;
 [alias] May-aliases after instruction  t->d = a;  are
   { t->t; z1 }  { (t->t)->c; z1->c; t->d; a }  { (t->t)->s; z1->s }
   { (*(t->t))[0..].s; (*z1)[0..].s }
+[alias] May-alias graph after instruction  t->d = a;  is
+  1:{  } -s→ 6:{  }   1:{  } -c→ 14:{ a }   2:{ t } → 3:{  }
+  3:{  } -t→ 13:{ z1 }   3:{  } -d→ 14:{ a }   6:{  } → 7:{  }
+  7:{  } → 8:{ x1; x2 }   13:{ z1 } → 1:{  }   14:{ a } → 5:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { t->t; z1 }  { (t->t)->c; z1->c; t->d; a }  { (t->t)->s; z1->s }
   { (*(t->t))[0..].s; (*z1)[0..].s }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  1:{  } -s→ 6:{  }   1:{  } -c→ 14:{ a }   2:{ t } → 3:{  }
+  3:{  } -t→ 13:{ z1 }   3:{  } -d→ 14:{ a }   6:{  } → 7:{  }
+  7:{  } → 8:{ x1; x2 }   13:{ z1 } → 1:{  }   14:{ a } → 5:{  }
 [alias] May-aliases at the end of function main:
   { t->t; z1 }  { (t->t)->c; z1->c; t->d; a }  { (t->t)->s; z1->s }
   { (*(t->t))[0..].s; (*z1)[0..].s }
+[alias] May-alias graph at the end of function main:
+  1:{  } -s→ 6:{  }   1:{  } -c→ 14:{ a }   2:{ t } → 3:{  }
+  3:{  } -t→ 13:{ z1 }   3:{  } -d→ 14:{ a }   6:{  } → 7:{  }
+  7:{  } → 8:{ x1; x2 }   13:{ z1 } → 1:{  }   14:{ a } → 5:{  }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  z1  t  a  __retres    returns: __retres
+  state: { t->t; z1 }  { (t->t)->c; z1->c; t->d; a }  { (t->t)->s; z1->s }
+         { (*(t->t))[0..].s; (*z1)[0..].s }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
index b325558af32..668bf60c584 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
+++ b/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
diff --git a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
index 2b2f7ecd4e5..562ebe1bde8 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
@@ -2,18 +2,35 @@
 [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: st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4};
 [alias:unsafe-cast] structure2.c:21: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction
   st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4};  are  <none>
+[alias] May-alias graph after instruction
+  st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4};  is
+  0:{ y } -s→ 1:{  }   1:{  } → 2:{ x1 }
 [alias] analysing instruction: y.s = (struct struct_1_t *)(& x2);
 [alias:unsafe-cast] structure2.c:23: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  y.s = (struct struct_1_t *)(& x2);  are
   <none>
+[alias] May-alias graph after instruction  y.s = (struct struct_1_t *)(& x2);  is
+  0:{ y } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  <none>
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ y } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }
 [alias] May-aliases at the end of function main: <none>
+[alias] May-alias graph at the end of function main:
+  0:{ y } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  y  __retres    returns: __retres
+  state: <none>
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
index f6d3384a8cb..4b1783ea694 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
@@ -2,33 +2,64 @@
 [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:
   st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3};
 [alias:unsafe-cast] structure3.c:31: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction
   st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3};  are  <none>
+[alias] May-alias graph after instruction
+  st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3};  is
+  0:{ y1 } -s→ 1:{  }   1:{  } → 2:{ x1 }
 [alias] analysing instruction:
   st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4};
 [alias:unsafe-cast] structure3.c:32: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction
   st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4};  are  <none>
+[alias] May-alias graph after instruction
+  st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4};  is
+  0:{ y1 } -s→ 1:{  }   1:{  } → 2:{ x1 }   4:{ y2 } -s→ 5:{  }
+  5:{  } → 6:{ x2 }
 [alias] analysing instruction: st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5};
 [alias:unsafe-cast] structure3.c:33: Warning: 
   unsafe cast from st_2_t * to struct struct_2_t *
 [alias] May-aliases after instruction
   st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5};  are
   { (z.t)->s; y1.s }
+[alias] May-alias graph after instruction
+  st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5};  is
+  0:{ y1 } -s→ 1:{  }   1:{  } → 2:{ x1 }   4:{ y2 } -s→ 5:{  }
+  5:{  } → 6:{ x2 }   8:{ z } -t→ 9:{  }   9:{  } → 0:{ y1 }
 [alias] analysing instruction: z.t = (struct struct_2_t *)(& y2);
 [alias:unsafe-cast] structure3.c:35: Warning: 
   unsafe cast from st_2_t * to struct struct_2_t *
 [alias] May-aliases after instruction  z.t = (struct struct_2_t *)(& y2);  are
   { (z.t)->s; y1.s; y2.s }
+[alias] May-alias graph after instruction  z.t = (struct struct_2_t *)(& y2);  is
+  0:{ y1; y2 } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }   8:{ z } -t→ 9:{  }
+  9:{  } → 0:{ y1; y2 }
 [alias] analysing instruction: y1.c = z.d;
 [alias] May-aliases after instruction  y1.c = z.d;  are  { (z.t)->s; y1.s; y2.s }
+[alias] May-alias graph after instruction  y1.c = z.d;  is
+  0:{ y1; y2 } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }   8:{ z } -t→ 9:{  }
+  9:{  } → 0:{ y1; y2 }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { (z.t)->s; y1.s; y2.s }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  0:{ y1; y2 } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }   8:{ z } -t→ 9:{  }
+  9:{  } → 0:{ y1; y2 }
 [alias] May-aliases at the end of function main: { (z.t)->s; y1.s; y2.s }
+[alias] May-alias graph at the end of function main:
+  0:{ y1; y2 } -s→ 1:{  }   1:{  } → 2:{ x1; x2 }   8:{ z } -t→ 9:{  }
+  9:{  } → 0:{ y1; y2 }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  y1  y2  z  __retres    returns: __retres
+  state: { (z.t)->s; y1.s; y2.s }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
index f4bf90f2a09..eaf97b2e49d 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
@@ -2,23 +2,45 @@
 [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: st_1_t *y1 = malloc(sizeof(st_1_t));
 [alias] May-aliases after instruction  st_1_t *y1 = malloc(sizeof(st_1_t));  are
   <none>
+[alias] May-alias graph after instruction  st_1_t *y1 = malloc(sizeof(st_1_t));
+  is    0:{ y1 } → 1:{  }
 [alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t));
 [alias] May-aliases after instruction  st_2_t *z = malloc(sizeof(st_2_t));  are
   <none>
+[alias] May-alias graph after instruction  st_2_t *z = malloc(sizeof(st_2_t));  is
+  0:{ y1 } → 1:{  }   2:{ z } → 3:{  }
 [alias] analysing instruction: y1 = & x1;
 [alias] May-aliases after instruction  y1 = & x1;  are  <none>
+[alias] May-alias graph after instruction  y1 = & x1;  is
+  0:{ y1 } → 1:{ x1 }   2:{ z } → 3:{  }
 [alias] analysing instruction: z->s = (struct struct_1_t *)y1;
 [alias:unsafe-cast] structure4.c:37: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z->s = (struct struct_1_t *)y1;  are
   { z->s; y1 }
+[alias] May-alias graph after instruction  z->s = (struct struct_1_t *)y1;  is
+  2:{ z } → 3:{  }   3:{  } -s→ 6:{ y1 }   6:{ y1 } → 1:{ x1 }
 [alias] analysing instruction: z->c = 6;
 [alias] May-aliases after instruction  z->c = 6;  are  { z->s; y1 }
+[alias] May-alias graph after instruction  z->c = 6;  is
+  2:{ z } → 3:{  }   3:{  } -s→ 6:{ y1 }   6:{ y1 } → 1:{ x1 }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { z->s; y1 }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  2:{ z } → 3:{  }   3:{  } -s→ 6:{ y1 }   6:{ y1 } → 1:{ x1 }
 [alias] May-aliases at the end of function main: { z->s; y1 }
+[alias] May-alias graph at the end of function main:
+  2:{ z } → 3:{  }   3:{  } -s→ 6:{ y1 }   6:{ y1 } → 1:{ x1 }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  y1→{ x1 }  z  __retres    returns: __retres
+  state: { z->s; y1 }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
index 0d59e58c4b3..a056387b5c5 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
@@ -2,40 +2,86 @@
 [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: st_1_t *y1 = malloc(sizeof(st_1_t));
 [alias] May-aliases after instruction  st_1_t *y1 = malloc(sizeof(st_1_t));  are
   <none>
+[alias] May-alias graph after instruction  st_1_t *y1 = malloc(sizeof(st_1_t));
+  is    0:{ y1 } → 1:{  }
 [alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t));
 [alias] May-aliases after instruction  st_2_t *z = malloc(sizeof(st_2_t));  are
   <none>
+[alias] May-alias graph after instruction  st_2_t *z = malloc(sizeof(st_2_t));  is
+  0:{ y1 } → 1:{  }   2:{ z } → 3:{  }
 [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:{ y1 } → 1:{  }   2:{ z } → 3:{  }   4:{ t } → 5:{  }
 [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:{ y1 } → 1:{  }   2:{ z } → 3:{  }   4:{ t } → 5:{  }
+  6:{ a } → 7:{  }
 [alias] analysing instruction: *a = 0;
 [alias] May-aliases after instruction  *a = 0;  are  <none>
+[alias] May-alias graph after instruction  *a = 0;  is
+  0:{ y1 } → 1:{  }   2:{ z } → 3:{  }   4:{ t } → 5:{  }
+  6:{ a } → 7:{  }
 [alias] analysing instruction: y1 = & x1;
 [alias] May-aliases after instruction  y1 = & x1;  are  <none>
+[alias] May-alias graph after instruction  y1 = & x1;  is
+  0:{ y1 } → 1:{ x1 }   2:{ z } → 3:{  }   4:{ t } → 5:{  }
+  6:{ a } → 7:{  }
 [alias] analysing instruction: z->s = (struct struct_1_t *)y1;
 [alias:unsafe-cast] structure5.c:41: Warning: 
   unsafe cast from st_1_t * to struct struct_1_t *
 [alias] May-aliases after instruction  z->s = (struct struct_1_t *)y1;  are
   { z->s; y1 }
+[alias] May-alias graph after instruction  z->s = (struct struct_1_t *)y1;  is
+  2:{ z } → 3:{  }   3:{  } -s→ 10:{ y1 }   4:{ t } → 5:{  }
+  6:{ a } → 7:{  }   10:{ y1 } → 1:{ x1 }
 [alias] analysing instruction: z->c = a;
 [alias] May-aliases after instruction  z->c = a;  are  { z->s; y1 }  { z->c; a }
+[alias] May-alias graph after instruction  z->c = a;  is
+  2:{ z } → 3:{  }   3:{  } -s→ 10:{ y1 }   3:{  } -c→ 11:{ a }
+  4:{ t } → 5:{  }   10:{ y1 } → 1:{ x1 }   11:{ a } → 7:{  }
 [alias] analysing instruction: t->t = (struct struct_2_t *)z;
 [alias:unsafe-cast] structure5.c:43: Warning: 
   unsafe cast from st_2_t * to struct struct_2_t *
 [alias] May-aliases after instruction  t->t = (struct struct_2_t *)z;  are
   { (t->t)->s; z->s; y1 }  { t->t; z }  { (t->t)->c; z->c; a }
+[alias] May-alias graph after instruction  t->t = (struct struct_2_t *)z;  is
+  3:{  } -s→ 10:{ y1 }   3:{  } -c→ 11:{ a }   4:{ t } → 5:{  }
+  5:{  } -t→ 12:{ z }   10:{ y1 } → 1:{ x1 }   11:{ a } → 7:{  }
+  12:{ z } → 3:{  }
 [alias] analysing instruction: t->d = a;
 [alias] May-aliases after instruction  t->d = a;  are
   { (t->t)->s; z->s; y1 }  { t->t; z }  { (t->t)->c; z->c; t->d; a }
+[alias] May-alias graph after instruction  t->d = a;  is
+  3:{  } -s→ 10:{ y1 }   3:{  } -c→ 13:{ a }   4:{ t } → 5:{  }
+  5:{  } -t→ 12:{ z }   5:{  } -d→ 13:{ a }   10:{ y1 } → 1:{ x1 }
+  12:{ z } → 3:{  }   13:{ a } → 7:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { (t->t)->s; z->s; y1 }  { t->t; z }  { (t->t)->c; z->c; t->d; a }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  3:{  } -s→ 10:{ y1 }   3:{  } -c→ 13:{ a }   4:{ t } → 5:{  }
+  5:{  } -t→ 12:{ z }   5:{  } -d→ 13:{ a }   10:{ y1 } → 1:{ x1 }
+  12:{ z } → 3:{  }   13:{ a } → 7:{  }
 [alias] May-aliases at the end of function main:
   { (t->t)->s; z->s; y1 }  { t->t; z }  { (t->t)->c; z->c; t->d; a }
+[alias] May-alias graph at the end of function main:
+  3:{  } -s→ 10:{ y1 }   3:{  } -c→ 13:{ a }   4:{ t } → 5:{  }
+  5:{  } -t→ 12:{ z }   5:{  } -d→ 13:{ a }   10:{ y1 } → 1:{ x1 }
+  12:{ z } → 3:{  }   13:{ a } → 7:{  }
+[alias] Summary of function main:
+  formals:     locals: x1  x2  y1→{ x1 }  z  t  a  __retres
+  returns: __retres
+  state: { (t->t)->s; z->s; y1 }  { t->t; z }  { (t->t)->c; z->c; t->d; a }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
index 63b621d8053..a83fa243f1a 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -2,152 +2,326 @@
 [alias] analysing function: f1
 [alias] analysing instruction: ty *tmp = x;
 [alias] May-aliases after instruction  ty *tmp = x;  are  { x; tmp }
+[alias] May-alias graph after instruction  ty *tmp = x;  is
+  0:{ x; tmp } → 1:{  }
 [alias] analysing instruction:
   idata = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   idata = (double *)malloc((unsigned long)10 * sizeof(double));  are
   { x; tmp }
+[alias] May-alias graph after instruction
+  idata = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  0:{ x; tmp } → 1:{  }   4:{ idata } → 5:{  }
 [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  idata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
+[alias] May-alias graph after instruction  idata = tmp->t2[*(tmp->n2)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   4:{ idata } → 5:{  }
+  6:{  } → 4:{ idata }
 [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  odata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  odata = tmp->t1[*(tmp->n1)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idx = 0;
 [alias] May-aliases after instruction  idx = 0;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idx = 0;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: tmp_1 = sin(*(idata + idx));
 [alias:undefined:fn] example1.c:45: Warning: function sin has no definition
 [alias] May-aliases after instruction  tmp_1 = sin(*(idata + idx));  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  tmp_1 = sin(*(idata + idx));  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1;
 [alias] May-aliases after instruction  *(odata + idx) = 0.5 * tmp_1;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  *(odata + idx) = 0.5 * tmp_1;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idx ++;
 [alias] May-aliases after instruction  idx ++;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idx ++;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: swap(tmp->n1);
 [alias] analysing function: swap
 [alias] analysing instruction: *n = 0;
 [alias] May-aliases after instruction  *n = 0;  are  <none>
+[alias] May-alias graph after instruction  *n = 0;  is    <empty>
 [alias] analysing instruction: (*n) ++;
 [alias] May-aliases after instruction  (*n) ++;  are  <none>
+[alias] May-alias graph after instruction  (*n) ++;  is    <empty>
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
 [alias] May-aliases after instruction  swap(tmp->n1);  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  swap(tmp->n1);  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  idata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idata = tmp->t2[*(tmp->n2)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  odata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  odata = tmp->t1[*(tmp->n1)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias:no-return] example1.c:29: Warning: 
   function f1 does not return; analysis may be unsound
 [alias] May-aliases at the end of function f1: <none>
+[alias] May-alias graph at the end of function f1:
+  <empty>
+[alias] Summary of function f1:
+  formals: x    locals: tmp  idata  odata  idx  tmp_1  __retres
+  returns: __retres    state: <none>
 [alias] analysing function: f2
 [alias] analysing instruction: ty *tmp = x;
 [alias] May-aliases after instruction  ty *tmp = x;  are  { x; tmp }
+[alias] May-alias graph after instruction  ty *tmp = x;  is
+  14:{ x; tmp } → 15:{  }
 [alias] analysing instruction:
   idata = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   idata = (double *)malloc((unsigned long)10 * sizeof(double));  are
   { x; tmp }
+[alias] May-alias graph after instruction
+  idata = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  14:{ x; tmp } → 15:{  }   18:{ idata } → 19:{  }
 [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  idata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
+[alias] May-alias graph after instruction  idata = tmp->t1[*(tmp->n1)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
 [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  odata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  odata = tmp->t2[*(tmp->n2)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idx = 0;
 [alias] May-aliases after instruction  idx = 0;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idx = 0;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction:
   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
 [alias] May-aliases after instruction
   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction
+  *(odata + idx) = (double)3 * *(idata + idx) + (double)1;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idx ++;
 [alias] May-aliases after instruction  idx ++;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idx ++;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: swap(tmp->n2);
 [alias] May-aliases after instruction  swap(tmp->n2);  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  swap(tmp->n2);  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  idata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idata = tmp->t1[*(tmp->n1)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  odata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  odata = tmp->t2[*(tmp->n2)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias:no-return] example1.c:53: Warning: 
   function f2 does not return; analysis may be unsound
 [alias] May-aliases at the end of function f2: <none>
+[alias] May-alias graph at the end of function f2:
+  <empty>
+[alias] Summary of function f2:
+  formals: x    locals: tmp  idx  idata  odata  __retres
+  returns: __retres    state: <none>
 [alias] analysing function: main
 [alias] analysing instruction: a = (ty *)malloc(sizeof(ty));
 [alias] May-aliases after instruction  a = (ty *)malloc(sizeof(ty));  are  <none>
+[alias] May-alias graph after instruction  a = (ty *)malloc(sizeof(ty));  is
+  28:{ a } → 29:{  }
 [alias] analysing instruction: b = (ty *)malloc(sizeof(ty));
 [alias] May-aliases after instruction  b = (ty *)malloc(sizeof(ty));  are  <none>
+[alias] May-alias graph after instruction  b = (ty *)malloc(sizeof(ty));  is
+  28:{ a } → 29:{  }   30:{ b } → 31:{  }
 [alias] analysing instruction: i = 0;
 [alias] May-aliases after instruction  i = 0;  are  <none>
+[alias] May-alias graph after instruction  i = 0;  is
+  28:{ a } → 29:{  }   30:{ b } → 31:{  }
 [alias] analysing instruction:
   a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));  are  
   <none>
+[alias] May-alias graph after instruction
+  a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   30:{ b } → 31:{  }
+  32:{  } → 33:{  }   33:{  } → 34:{  }
 [alias] analysing instruction:
   a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));  are  
   <none>
+[alias] May-alias graph after instruction
+  a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   29:{  } -t2→ 35:{  }
+  30:{ b } → 31:{  }   32:{  } → 33:{  }   33:{  } → 34:{  }
+  35:{  } → 36:{  }   36:{  } → 37:{  }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  <none>
+[alias] May-alias graph after instruction  i ++;  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   29:{  } -t2→ 35:{  }
+  30:{ b } → 31:{  }   32:{  } → 33:{  }   33:{  } → 34:{  }
+  35:{  } → 36:{  }   36:{  } → 37:{  }
 [alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int));
 [alias] May-aliases after instruction  a->n1 = (int *)malloc(sizeof(int));  are
   <none>
+[alias] May-alias graph after instruction  a->n1 = (int *)malloc(sizeof(int));  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   30:{ b } → 31:{  }
+  38:{  } → 39:{  }
 [alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int));
 [alias] May-aliases after instruction  a->n2 = (int *)malloc(sizeof(int));  are
   <none>
+[alias] May-alias graph after instruction  a->n2 = (int *)malloc(sizeof(int));  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: *(a->n1) = 1;
 [alias] May-aliases after instruction  *(a->n1) = 1;  are  <none>
+[alias] May-alias graph after instruction  *(a->n1) = 1;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: *(a->n2) = 1;
 [alias] May-aliases after instruction  *(a->n2) = 1;  are  <none>
+[alias] May-alias graph after instruction  *(a->n2) = 1;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: i = 0;
 [alias] May-aliases after instruction  i = 0;  are  <none>
+[alias] May-alias graph after instruction  i = 0;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: b->t1[i] = a->t1[i];
 [alias] May-aliases after instruction  b->t1[i] = a->t1[i];  are  { a->t1; b->t1 }
+[alias] May-alias graph after instruction  b->t1[i] = a->t1[i];  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   30:{ b } → 31:{  }   31:{  } -t1→ 42:{  }
+  38:{  } → 39:{  }   40:{  } → 41:{  }   42:{  } → 43:{  }
+  44:{  } → 43:{  }
 [alias] analysing instruction: b->t2[i] = a->t2[i];
 [alias] May-aliases after instruction  b->t2[i] = a->t2[i];  are
   { a->t1; b->t1 }  { a->t2; b->t2 }
+[alias] May-alias graph after instruction  b->t2[i] = a->t2[i];  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   29:{  } -t2→ 48:{  }   30:{ b } → 31:{  }
+  31:{  } -t1→ 42:{  }   31:{  } -t2→ 46:{  }   38:{  } → 39:{  }
+  40:{  } → 41:{  }   42:{  } → 43:{  }   44:{  } → 43:{  }
+  46:{  } → 47:{  }   48:{  } → 47:{  }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  { a->t1; b->t1 }  { a->t2; b->t2 }
+[alias] May-alias graph after instruction  i ++;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   29:{  } -t2→ 48:{  }   30:{ b } → 31:{  }
+  31:{  } -t1→ 42:{  }   31:{  } -t2→ 46:{  }   38:{  } → 39:{  }
+  40:{  } → 41:{  }   42:{  } → 43:{  }   44:{  } → 43:{  }
+  46:{  } → 47:{  }   48:{  } → 47:{  }
 [alias] analysing instruction: b->n1 = a->n1;
 [alias] May-aliases after instruction  b->n1 = a->n1;  are  { a->n1; b->n1 }
+[alias] May-alias graph after instruction  b->n1 = a->n1;  is
+  28:{ a } → 29:{  }   29:{  } -n2→ 40:{  }   29:{  } -n1→ 50:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   40:{  } → 41:{  }
+  50:{  } → 39:{  }
 [alias] analysing instruction: b->n2 = a->n2;
 [alias] May-aliases after instruction  b->n2 = a->n2;  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  b->n2 = a->n2;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
 [alias] analysing instruction: f1(a);
 [alias] May-aliases after instruction  f1(a);  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  f1(a);  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
 [alias] analysing instruction: f2(b);
 [alias] May-aliases after instruction  f2(b);  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  f2(b);  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
 [alias] May-aliases at the end of function main: { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph at the end of function main:
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  i  __retres    returns: __retres
+  state: { a->n1; b->n1 }  { a->n2; b->n2 }
 [alias] analysing function: swap
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
index 3ec39c89608..f1b9a01af08 100644
--- a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
@@ -2,172 +2,390 @@
 [alias] analysing function: f1
 [alias] analysing instruction: ty *tmp = x;
 [alias] May-aliases after instruction  ty *tmp = x;  are  { x; tmp }
+[alias] May-alias graph after instruction  ty *tmp = x;  is
+  0:{ x; tmp } → 1:{  }
 [alias] analysing instruction:
   idata = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   idata = (double *)malloc((unsigned long)10 * sizeof(double));  are
   { x; tmp }
+[alias] May-alias graph after instruction
+  idata = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  0:{ x; tmp } → 1:{  }   4:{ idata } → 5:{  }
 [alias] analysing instruction: int i = 0;
 [alias] May-aliases after instruction  int i = 0;  are  { x; tmp }
+[alias] May-alias graph after instruction  int i = 0;  is
+  0:{ x; tmp } → 1:{  }   4:{ idata } → 5:{  }
 [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  idata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
+[alias] May-alias graph after instruction  idata = tmp->t2[*(tmp->n2)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   4:{ idata } → 5:{  }
+  6:{  } → 4:{ idata }
 [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  odata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  odata = tmp->t1[*(tmp->n1)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idx = 0;
 [alias] May-aliases after instruction  idx = 0;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idx = 0;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: tmp_1 = sin(*(idata + idx));
 [alias:undefined:fn] example2.c:45: Warning: function sin has no definition
 [alias] May-aliases after instruction  tmp_1 = sin(*(idata + idx));  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  tmp_1 = sin(*(idata + idx));  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1;
 [alias] May-aliases after instruction  *(odata + idx) = 0.5 * tmp_1;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  *(odata + idx) = 0.5 * tmp_1;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idx ++;
 [alias] May-aliases after instruction  idx ++;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idx ++;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: swap(tmp->n1);
 [alias] analysing function: swap
 [alias] analysing instruction: *n = 0;
 [alias] May-aliases after instruction  *n = 0;  are  <none>
+[alias] May-alias graph after instruction  *n = 0;  is    <empty>
 [alias] analysing instruction: (*n) ++;
 [alias] May-aliases after instruction  (*n) ++;  are  <none>
+[alias] May-alias graph after instruction  (*n) ++;  is    <empty>
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
 [alias] May-aliases after instruction  swap(tmp->n1);  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  swap(tmp->n1);  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  i ++;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  idata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  idata = tmp->t2[*(tmp->n2)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  odata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  odata = tmp->t1[*(tmp->n1)];  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] analysing instruction: __retres = (void *)0;
 [alias] May-aliases after instruction  __retres = (void *)0;  are
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph after instruction  __retres = (void *)0;  is
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
 [alias] May-aliases at the end of function f1:
   { x; tmp }  { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; idata }
   { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+[alias] May-alias graph at the end of function f1:
+  0:{ x; tmp } → 1:{  }   1:{  } -t2→ 6:{  }   1:{  } -t1→ 10:{  }
+  4:{ idata } → 5:{  }   6:{  } → 4:{ idata }   8:{ odata } → 9:{  }
+  10:{  } → 8:{ odata }
+[alias] Summary of function f1:
+  formals: x    locals: tmp  idata  odata  idx  i  tmp_1  __retres
+  returns: __retres
+  state: { x; tmp }  { x->t2; tmp->t2 }
+         { (*x)[0..].t2; (*tmp)[0..].t2; idata }  { x->t1; tmp->t1 }
+         { (*x)[0..].t1; (*tmp)[0..].t1; odata }
 [alias] analysing function: f2
 [alias] analysing instruction: ty *tmp = x;
 [alias] May-aliases after instruction  ty *tmp = x;  are  { x; tmp }
+[alias] May-alias graph after instruction  ty *tmp = x;  is
+  14:{ x; tmp } → 15:{  }
 [alias] analysing instruction:
   idata = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   idata = (double *)malloc((unsigned long)10 * sizeof(double));  are
   { x; tmp }
+[alias] May-alias graph after instruction
+  idata = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  14:{ x; tmp } → 15:{  }   18:{ idata } → 19:{  }
 [alias] analysing instruction: int i = 0;
 [alias] May-aliases after instruction  int i = 0;  are  { x; tmp }
+[alias] May-alias graph after instruction  int i = 0;  is
+  14:{ x; tmp } → 15:{  }   18:{ idata } → 19:{  }
 [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  idata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
+[alias] May-alias graph after instruction  idata = tmp->t1[*(tmp->n1)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
 [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  odata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  odata = tmp->t2[*(tmp->n2)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idx = 0;
 [alias] May-aliases after instruction  idx = 0;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idx = 0;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction:
   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
 [alias] May-aliases after instruction
   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction
+  *(odata + idx) = (double)3 * *(idata + idx) + (double)1;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idx ++;
 [alias] May-aliases after instruction  idx ++;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idx ++;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: swap(tmp->n2);
 [alias] May-aliases after instruction  swap(tmp->n2);  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  swap(tmp->n2);  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  i ++;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
 [alias] May-aliases after instruction  idata = tmp->t1[*(tmp->n1)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  idata = tmp->t1[*(tmp->n1)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
 [alias] May-aliases after instruction  odata = tmp->t2[*(tmp->n2)];  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  odata = tmp->t2[*(tmp->n2)];  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] analysing instruction: __retres = (void *)0;
 [alias] May-aliases after instruction  __retres = (void *)0;  are
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph after instruction  __retres = (void *)0;  is
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
 [alias] May-aliases at the end of function f2:
   { x; tmp }  { x->t1; tmp->t1 }  { (*x)[0..].t1; (*tmp)[0..].t1; idata }
   { x->t2; tmp->t2 }  { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+[alias] May-alias graph at the end of function f2:
+  14:{ x; tmp } → 15:{  }   15:{  } -t1→ 20:{  }   15:{  } -t2→ 24:{  }
+  18:{ idata } → 19:{  }   20:{  } → 18:{ idata }
+  22:{ odata } → 23:{  }   24:{  } → 22:{ odata }
+[alias] Summary of function f2:
+  formals: x    locals: tmp  idx  idata  odata  i  __retres
+  returns: __retres
+  state: { x; tmp }  { x->t1; tmp->t1 }
+         { (*x)[0..].t1; (*tmp)[0..].t1; idata }  { x->t2; tmp->t2 }
+         { (*x)[0..].t2; (*tmp)[0..].t2; odata }
 [alias] analysing function: main
 [alias] analysing instruction: a = (ty *)malloc(sizeof(ty));
 [alias] May-aliases after instruction  a = (ty *)malloc(sizeof(ty));  are  <none>
+[alias] May-alias graph after instruction  a = (ty *)malloc(sizeof(ty));  is
+  28:{ a } → 29:{  }
 [alias] analysing instruction: b = (ty *)malloc(sizeof(ty));
 [alias] May-aliases after instruction  b = (ty *)malloc(sizeof(ty));  are  <none>
+[alias] May-alias graph after instruction  b = (ty *)malloc(sizeof(ty));  is
+  28:{ a } → 29:{  }   30:{ b } → 31:{  }
 [alias] analysing instruction: i = 0;
 [alias] May-aliases after instruction  i = 0;  are  <none>
+[alias] May-alias graph after instruction  i = 0;  is
+  28:{ a } → 29:{  }   30:{ b } → 31:{  }
 [alias] analysing instruction:
   a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));  are  
   <none>
+[alias] May-alias graph after instruction
+  a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   30:{ b } → 31:{  }
+  32:{  } → 33:{  }   33:{  } → 34:{  }
 [alias] analysing instruction:
   a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
 [alias] May-aliases after instruction
   a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));  are  
   <none>
+[alias] May-alias graph after instruction
+  a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   29:{  } -t2→ 35:{  }
+  30:{ b } → 31:{  }   32:{  } → 33:{  }   33:{  } → 34:{  }
+  35:{  } → 36:{  }   36:{  } → 37:{  }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  <none>
+[alias] May-alias graph after instruction  i ++;  is
+  28:{ a } → 29:{  }   29:{  } -t1→ 32:{  }   29:{  } -t2→ 35:{  }
+  30:{ b } → 31:{  }   32:{  } → 33:{  }   33:{  } → 34:{  }
+  35:{  } → 36:{  }   36:{  } → 37:{  }
 [alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int));
 [alias] May-aliases after instruction  a->n1 = (int *)malloc(sizeof(int));  are
   <none>
+[alias] May-alias graph after instruction  a->n1 = (int *)malloc(sizeof(int));  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   30:{ b } → 31:{  }
+  38:{  } → 39:{  }
 [alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int));
 [alias] May-aliases after instruction  a->n2 = (int *)malloc(sizeof(int));  are
   <none>
+[alias] May-alias graph after instruction  a->n2 = (int *)malloc(sizeof(int));  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: *(a->n1) = 1;
 [alias] May-aliases after instruction  *(a->n1) = 1;  are  <none>
+[alias] May-alias graph after instruction  *(a->n1) = 1;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: *(a->n2) = 1;
 [alias] May-aliases after instruction  *(a->n2) = 1;  are  <none>
+[alias] May-alias graph after instruction  *(a->n2) = 1;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: i = 0;
 [alias] May-aliases after instruction  i = 0;  are  <none>
+[alias] May-alias graph after instruction  i = 0;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  30:{ b } → 31:{  }   38:{  } → 39:{  }   40:{  } → 41:{  }
 [alias] analysing instruction: b->t1[i] = a->t1[i];
 [alias] May-aliases after instruction  b->t1[i] = a->t1[i];  are  { a->t1; b->t1 }
+[alias] May-alias graph after instruction  b->t1[i] = a->t1[i];  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   30:{ b } → 31:{  }   31:{  } -t1→ 42:{  }
+  38:{  } → 39:{  }   40:{  } → 41:{  }   42:{  } → 43:{  }
+  44:{  } → 43:{  }
 [alias] analysing instruction: b->t2[i] = a->t2[i];
 [alias] May-aliases after instruction  b->t2[i] = a->t2[i];  are
   { a->t1; b->t1 }  { a->t2; b->t2 }
+[alias] May-alias graph after instruction  b->t2[i] = a->t2[i];  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   29:{  } -t2→ 48:{  }   30:{ b } → 31:{  }
+  31:{  } -t1→ 42:{  }   31:{  } -t2→ 46:{  }   38:{  } → 39:{  }
+  40:{  } → 41:{  }   42:{  } → 43:{  }   44:{  } → 43:{  }
+  46:{  } → 47:{  }   48:{  } → 47:{  }
 [alias] analysing instruction: i ++;
 [alias] May-aliases after instruction  i ++;  are  { a->t1; b->t1 }  { a->t2; b->t2 }
+[alias] May-alias graph after instruction  i ++;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 38:{  }   29:{  } -n2→ 40:{  }
+  29:{  } -t1→ 44:{  }   29:{  } -t2→ 48:{  }   30:{ b } → 31:{  }
+  31:{  } -t1→ 42:{  }   31:{  } -t2→ 46:{  }   38:{  } → 39:{  }
+  40:{  } → 41:{  }   42:{  } → 43:{  }   44:{  } → 43:{  }
+  46:{  } → 47:{  }   48:{  } → 47:{  }
 [alias] analysing instruction: b->n1 = a->n1;
 [alias] May-aliases after instruction  b->n1 = a->n1;  are  { a->n1; b->n1 }
+[alias] May-alias graph after instruction  b->n1 = a->n1;  is
+  28:{ a } → 29:{  }   29:{  } -n2→ 40:{  }   29:{  } -n1→ 50:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   40:{  } → 41:{  }
+  50:{  } → 39:{  }
 [alias] analysing instruction: b->n2 = a->n2;
 [alias] May-aliases after instruction  b->n2 = a->n2;  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  b->n2 = a->n2;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  30:{ b } → 31:{  }   31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }
+  50:{  } → 39:{  }   51:{  } → 41:{  }
 [alias] analysing instruction: f1(a);
 [alias] May-aliases after instruction  f1(a);  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  f1(a);  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  29:{  } -t2→ 58:{  }   29:{  } -t1→ 62:{  }   30:{ b } → 31:{  }
+  31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }   50:{  } → 39:{  }
+  51:{  } → 41:{  }   56:{  } → 57:{  }   58:{  } → 56:{  }
+  60:{  } → 61:{  }   62:{  } → 60:{  }
 [alias] analysing instruction: f2(b);
 [alias] May-aliases after instruction  f2(b);  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  f2(b);  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  29:{  } -t2→ 58:{  }   29:{  } -t1→ 62:{  }   30:{ b } → 31:{  }
+  31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }   31:{  } -t1→ 72:{  }
+  31:{  } -t2→ 76:{  }   50:{  } → 39:{  }   51:{  } → 41:{  }
+  56:{  } → 57:{  }   58:{  } → 56:{  }   60:{  } → 61:{  }
+  62:{  } → 60:{  }   70:{  } → 71:{  }   72:{  } → 70:{  }
+  74:{  } → 75:{  }   76:{  } → 74:{  }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are
   { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  29:{  } -t2→ 58:{  }   29:{  } -t1→ 62:{  }   30:{ b } → 31:{  }
+  31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }   31:{  } -t1→ 72:{  }
+  31:{  } -t2→ 76:{  }   50:{  } → 39:{  }   51:{  } → 41:{  }
+  56:{  } → 57:{  }   58:{  } → 56:{  }   60:{  } → 61:{  }
+  62:{  } → 60:{  }   70:{  } → 71:{  }   72:{  } → 70:{  }
+  74:{  } → 75:{  }   76:{  } → 74:{  }
 [alias] May-aliases at the end of function main: { a->n1; b->n1 }  { a->n2; b->n2 }
+[alias] May-alias graph at the end of function main:
+  28:{ a } → 29:{  }   29:{  } -n1→ 50:{  }   29:{  } -n2→ 51:{  }
+  29:{  } -t2→ 58:{  }   29:{  } -t1→ 62:{  }   30:{ b } → 31:{  }
+  31:{  } -n1→ 50:{  }   31:{  } -n2→ 51:{  }   31:{  } -t1→ 72:{  }
+  31:{  } -t2→ 76:{  }   50:{  } → 39:{  }   51:{  } → 41:{  }
+  56:{  } → 57:{  }   58:{  } → 56:{  }   60:{  } → 61:{  }
+  62:{  } → 60:{  }   70:{  } → 71:{  }   72:{  } → 70:{  }
+  74:{  } → 75:{  }   76:{  } → 74:{  }
+[alias] Summary of function main:
+  formals:     locals: a  b  i  __retres    returns: __retres
+  state: { a->n1; b->n1 }  { a->n2; b->n2 }
 [alias] analysing function: swap
 [alias] May-aliases at the end of function swap: <none>
+[alias] May-alias graph at the end of function swap:
+  <empty>
+[alias] Summary of function swap:
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle b/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle
index 85ec8d0acb7..4c9f5449cd5 100644
--- a/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle
@@ -2,20 +2,44 @@
 [alias] analysing function: alias
 [alias] analysing instruction: *x = *y;
 [alias] May-aliases after instruction  *x = *y;  are  { x; y }  { *x; *y }
+[alias] May-alias graph after instruction  *x = *y;  is
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ y } → 1:{  }
 [alias] May-aliases at the end of function alias: { x; y }  { *x; *y }
+[alias] May-alias graph at the end of function alias:
+  0:{ x } → 1:{  }   1:{  } → 2:{  }   3:{ y } → 1:{  }
+[alias] Summary of function alias:
+  formals: x  y    locals:     returns: <none>    state: { x; y }  { *x; *y }
 [alias] analysing function: main
 [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
+  6:{ a } → 7:{  }
 [alias] analysing instruction: *a = 0;
 [alias] May-aliases after instruction  *a = 0;  are  <none>
+[alias] May-alias graph after instruction  *a = 0;  is    6:{ a } → 7:{  }
 [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
+  6:{ a } → 7:{  }   8:{ b } → 9:{  }
 [alias] analysing instruction: *b = 42;
 [alias] May-aliases after instruction  *b = 42;  are  <none>
+[alias] May-alias graph after instruction  *b = 42;  is
+  6:{ a } → 7:{  }   8:{ b } → 9:{  }
 [alias] analysing instruction: alias(& a,& b);
 [alias] May-aliases after instruction  alias(& a,& b);  are  { a; b }
+[alias] May-alias graph after instruction  alias(& a,& b);  is
+  6:{ a; b } → 7:{  }   14:{  } → 6:{ a; b }   15:{  } → 6:{ a; b }
 [alias] analysing instruction: *a = 7;
 [alias] May-aliases after instruction  *a = 7;  are  { a; b }
+[alias] May-alias graph after instruction  *a = 7;  is
+  6:{ a; b } → 7:{  }   14:{  } → 6:{ a; b }   15:{  } → 6:{ a; b }
 [alias] analysing instruction: __retres = 0;
 [alias] May-aliases after instruction  __retres = 0;  are  { a; b }
+[alias] May-alias graph after instruction  __retres = 0;  is
+  6:{ a; b } → 7:{  }   14:{  } → 6:{ a; b }   15:{  } → 6:{ a; b }
 [alias] May-aliases at the end of function main: { a; b }
+[alias] May-alias graph at the end of function main:
+  6:{ a; b } → 7:{  }   14:{  } → 6:{ a; b }   15:{  } → 6:{ a; b }
+[alias] Summary of function main:
+  formals:     locals: a  b  __retres    returns: __retres    state: { a; b }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/test_config b/src/plugins/alias/tests/test_config
index e14c0a6d247..80976f50aac 100644
--- a/src/plugins/alias/tests/test_config
+++ b/src/plugins/alias/tests/test_config
@@ -1,2 +1,2 @@
 PLUGIN: alias
-OPT: -alias -alias-verbose 3
+OPT: -alias -alias-verbose 3 -alias-debug 3
-- 
GitLab