From 58b2c237900d88ffba6224f59c862622e43fc234 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 12 Mar 2024 15:11:44 +0100
Subject: [PATCH] [alias] remove locals from function summaries

They are neither used nor particularly informative.
---
 src/plugins/alias/src/abstract_state.ml               |  5 +----
 .../alias/tests/basic/oracle/addrof.res.oracle        |  5 ++---
 .../alias/tests/basic/oracle/assignment1.res.oracle   |  3 +--
 .../alias/tests/basic/oracle/assignment2.res.oracle   |  3 +--
 .../alias/tests/basic/oracle/assignment3.res.oracle   |  3 +--
 .../alias/tests/basic/oracle/assignment4.res.oracle   |  3 +--
 .../alias/tests/basic/oracle/assignment5.res.oracle   |  3 +--
 src/plugins/alias/tests/basic/oracle/cast1.res.oracle |  3 +--
 .../alias/tests/basic/oracle/conditional1.res.oracle  |  3 +--
 .../alias/tests/basic/oracle/conditional2.res.oracle  |  5 ++---
 .../alias/tests/basic/oracle/conditional3.res.oracle  |  5 +----
 .../alias/tests/basic/oracle/function1.res.oracle     |  7 +++----
 .../alias/tests/basic/oracle/function2.res.oracle     |  6 +++---
 .../alias/tests/basic/oracle/function3.res.oracle     |  6 ++----
 .../alias/tests/basic/oracle/function4.res.oracle     |  5 ++---
 .../alias/tests/basic/oracle/function5.res.oracle     |  6 ++----
 .../alias/tests/basic/oracle/function6.res.oracle     |  3 +--
 .../alias/tests/basic/oracle/globctr.res.oracle       |  2 +-
 src/plugins/alias/tests/basic/oracle/loop.res.oracle  |  3 +--
 .../alias/tests/basic/oracle/steensgaard.res.oracle   |  4 +---
 .../alias/tests/basic/oracle/switch1.res.oracle       |  3 +--
 .../alias/tests/basic/oracle/switch2.res.oracle       |  3 +--
 .../alias/tests/basic/oracle/while_for1.res.oracle    |  2 +-
 .../alias/tests/basic/oracle/while_for2.res.oracle    |  3 +--
 .../alias/tests/basic/oracle/while_for3.res.oracle    |  3 +--
 .../alias/tests/fixed_bugs/oracle/arrays.res.oracle   |  2 +-
 .../tests/fixed_bugs/oracle/empty_nodes.res.oracle    |  4 ++--
 .../alias/tests/fixed_bugs/oracle/ex_jfla.res.oracle  | 11 ++++-------
 .../tests/fixed_bugs/oracle/ex_jfla_2.res.oracle      | 10 +++-------
 .../tests/fixed_bugs/oracle/ex_jfla_3.res.oracle      |  9 ++-------
 .../alias/tests/fixed_bugs/oracle/gzip124.res.oracle  |  3 +--
 .../alias/tests/fixed_bugs/oracle/origin.res.oracle   |  3 +--
 .../tests/fixed_bugs/oracle/origin_simpl.res.oracle   |  2 +-
 .../alias/tests/fixed_bugs/oracle/records.res.oracle  |  2 +-
 .../fixed_bugs/oracle/reduce_by_valid.res.oracle      |  3 +--
 .../alias/tests/fixed_bugs/oracle/semver.res.oracle   |  2 +-
 .../alias/tests/fixed_bugs/oracle/tkn-2.res.oracle    |  2 +-
 .../tests/fixed_bugs/oracle/union_readback.res.oracle |  3 +--
 .../tests/fixed_bugs/oracle/union_vmap.res.oracle     |  7 +++----
 .../alias/tests/offsets/oracle/array1.res.oracle      |  3 +--
 .../alias/tests/offsets/oracle/array2.res.oracle      |  3 +--
 .../alias/tests/offsets/oracle/array3.res.oracle      |  3 +--
 .../alias/tests/offsets/oracle/collapse1.res.oracle   |  3 +--
 .../alias/tests/offsets/oracle/collapse2.res.oracle   |  2 +-
 .../alias/tests/offsets/oracle/collapse3.res.oracle   |  2 +-
 .../tests/offsets/oracle/jfla_running_ex.res.oracle   |  9 ++-------
 .../alias/tests/offsets/oracle/nested1.res.oracle     |  3 +--
 .../alias/tests/offsets/oracle/nested2.res.oracle     |  2 +-
 .../alias/tests/offsets/oracle/structure1.res.oracle  |  3 +--
 .../alias/tests/offsets/oracle/structure2.res.oracle  |  3 +--
 .../alias/tests/offsets/oracle/structure3.res.oracle  |  3 +--
 .../alias/tests/offsets/oracle/structure4.res.oracle  |  3 +--
 .../alias/tests/offsets/oracle/structure5.res.oracle  |  3 +--
 .../alias/tests/real_world/oracle/example1.res.oracle |  9 +++------
 .../alias/tests/real_world/oracle/example2.res.oracle |  9 +++------
 .../tests/real_world/oracle/function1_v2.res.oracle   |  4 ++--
 56 files changed, 80 insertions(+), 147 deletions(-)

diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml
index ab6c344ace9..997c08eb829 100644
--- a/src/plugins/alias/src/abstract_state.ml
+++ b/src/plugins/alias/src/abstract_state.ml
@@ -710,7 +710,6 @@ module Summary = struct
   (* a type for summaries of functions *)
   type t = {state   : state option;
             formals : lval list;
-            locals  : lval list;
             return  : exp option}
 
   let make s (kf : kernel_function) =
@@ -735,7 +734,6 @@ module Summary = struct
     in
     {state = Some s;
      formals = List.map (fun v -> (Var v,NoOffset)) (Kernel_function.get_formals kf);
-     locals = List.map (fun v -> (Var v,NoOffset)) (Kernel_function.get_locals kf);
      return = exp_return}
 
   let pretty ?(debug=false) fmt summary =
@@ -759,9 +757,8 @@ module Summary = struct
     | None -> if debug then Format.fprintf fmt "not found"
     | Some s when is_empty s -> if debug then Format.fprintf fmt "empty"
     | Some s ->
-      Format.fprintf fmt "@[formals: @[%a@]@;<4>locals: @[%a@]@;<4>returns: @[%a@]@;<4>state: @[%a@] "
+      Format.fprintf fmt "@[formals: @[%a@]@;<4>returns: @[%a@]@;<4>state: @[%a@] "
         (pp_list_lval s) summary.formals
-        (pp_list_lval s) summary.locals
         (pp_option Exp.pretty) summary.return
         (pp_option @@ pretty ~debug) summary.state
 
diff --git a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
index 79e61cb0b0a..9d99ee3ec0c 100644
--- a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle
@@ -34,7 +34,6 @@
   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 }
+  formals:     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 4c31afc87e8..b1e3f774ca6 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -29,6 +29,5 @@
 [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 }
+  formals:     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 ee488debdbb..a584e695cb3 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -33,6 +33,5 @@
 [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 }
+  formals:     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 1a83b4c75ed..22605c19af0 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -24,6 +24,5 @@
 [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 }
+  formals:     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 3dec6c8a3c9..69175d2e930 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
@@ -33,6 +33,5 @@
 [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 }
+  formals:     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 21da14a9497..64a9a7de39a 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
@@ -34,6 +34,5 @@
 [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 }
+  formals:     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 6f28983041a..176c4f381f9 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -31,6 +31,5 @@
 [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 }
+  formals:     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 ede3b2e36f8..0fa0dba3a43 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -26,6 +26,5 @@
 [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 }
+  formals:     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 5972b2065a0..7fc2d29a8e6 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle
@@ -33,7 +33,6 @@
 [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 }
+  formals:     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 2bf30184b32..c6dbb35184a 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle
@@ -73,10 +73,7 @@
   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
+  formals:     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 }
diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
index 53a681adaf7..2d3bdc6d06a 100644
--- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
@@ -30,7 +30,7 @@
 [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 }
+  formals: x  y    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:{  }
@@ -49,8 +49,7 @@
   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 }
+  formals:     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>
@@ -59,5 +58,5 @@
 [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 }
+  formals: x  y    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 8a156f682a6..d7e607ebde1 100644
--- a/src/plugins/alias/tests/basic/oracle/function2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function2.res.oracle
@@ -20,7 +20,7 @@
 [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>
+  formals: size    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:{  }
@@ -36,7 +36,7 @@
 [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>
+  formals:     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>
@@ -45,5 +45,5 @@
 [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>
+  formals: size    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 4acd7896168..1642757d0b1 100644
--- a/src/plugins/alias/tests/basic/oracle/function3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function3.res.oracle
@@ -18,8 +18,7 @@
 [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 }
+  formals: x  y    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>
@@ -52,6 +51,5 @@
   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 }
+  formals:     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 8dbe90ab465..2b8bbf2b4c6 100644
--- a/src/plugins/alias/tests/basic/oracle/function4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function4.res.oracle
@@ -4,7 +4,7 @@
 [alias] May-alias graph at the end of function addr:
   <empty>
 [alias] Summary of function addr:
-  formals: x    locals:     returns: x    state: <none>
+  formals: x    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>
@@ -31,6 +31,5 @@
 [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 }
+  formals:     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 c7d33151e1a..cce128cc40e 100644
--- a/src/plugins/alias/tests/basic/oracle/function5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function5.res.oracle
@@ -15,8 +15,7 @@
 [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 }
+  formals: x  y    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>
@@ -39,6 +38,5 @@
 [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 }
+  formals:     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 74f1dd62b95..e60a5f1225e 100644
--- a/src/plugins/alias/tests/basic/oracle/function6.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function6.res.oracle
@@ -42,8 +42,7 @@
 [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>
+  formals:     returns: __retres    state: <none>
 [alias] analysing function: swap
 [alias] analysing instruction: int z = 0;
 [alias] May-aliases after instruction  int z = 0;  are  <none>
diff --git a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
index e5df545b132..3b942fd3aae 100644
--- a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
@@ -30,5 +30,5 @@
 [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>
+  formals:     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 74cdba557c8..e0dd21c5c92 100644
--- a/src/plugins/alias/tests/basic/oracle/loop.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/loop.res.oracle
@@ -33,6 +33,5 @@
 [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>
+  formals:     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 61305c305a0..45caffcae31 100644
--- a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
@@ -35,7 +35,5 @@
   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 }
+  formals:     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 5d4e7565c29..05300247fce 100644
--- a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
@@ -31,6 +31,5 @@
 [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 }
+  formals:     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 35c8cb7b5d7..ddad7609958 100644
--- a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
@@ -35,6 +35,5 @@
 [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 }
+  formals:     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 c389176d8e7..0db95fcf8a6 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -24,5 +24,5 @@
 [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>
+  formals:     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 d6cd6b220b4..14fd60cfa99 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
@@ -19,6 +19,5 @@
 [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 }
+  formals:     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 24560b86f6e..fa8a4fc601a 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
@@ -28,6 +28,5 @@
 [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 }
+  formals:     returns: __retres    state: { a; b }
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/arrays.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/arrays.res.oracle
index d126c7205b1..dc033719294 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/arrays.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/arrays.res.oracle
@@ -44,6 +44,6 @@
   10:{ z; q } → 11:{ t }   11:{ t } → 16:{ a; b; n }
   16:{ a; b; n } → 17:{  }
 [alias] Summary of function main:
-  formals:     locals: __retres    returns: __retres
+  formals:     returns: __retres
   state: { z; q }  { *z; *q; t }  { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
 [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 632370a683e..7141f4e9d65 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
@@ -19,7 +19,7 @@
   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>
+  formals: x→{ t }  y→{ t }  z→{ t }    returns: <none>
   state: { x; y; z }  { *x; *y; *z; t }
 [alias] analysing function: g
 [alias] analysing instruction: f(a,a,a);
@@ -30,5 +30,5 @@
 [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>
+  formals: a    returns: <none>    state: <none>
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla.res.oracle
index 1930c3168bd..96084ba3ad0 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla.res.oracle
@@ -32,7 +32,7 @@
   0:{ res } → 1:{  }   1:{  } -a→ 2:{  }   1:{  } -b→ 4:{ b }
   2:{  } → 3:{  }   4:{ b } → 5:{  }
 [alias] Summary of function create_str_t:
-  formals: va  b    locals: res    returns: res    state: { res->b; b }
+  formals: va  b    returns: res    state: { res->b; b }
 [alias] analysing function: jfla
 [alias] analysing instruction: *(s->b) = *(s->a);
 [alias] May-aliases after instruction  *(s->b) = *(s->a);  are  <none>
@@ -49,8 +49,7 @@
 [alias] May-alias graph at the end of function jfla:
   8:{ s } → 9:{  }   9:{  } -a→ 10:{ i1; i2 }   10:{ i1; i2 } → 12:{  }
 [alias] Summary of function jfla:
-  formals: s  i1  i2  b    locals:     returns: <none>
-  state: { s->a; i1; i2 }
+  formals: s  i1  i2  b    returns: <none>    state: { s->a; i1; i2 }
 [alias] analysing function: main
 [alias] analysing instruction: int u = 11;
 [alias] May-aliases after instruction  int u = 11;  are  <none>
@@ -172,8 +171,6 @@
   36:{  } -b→ 39:{  }   37:{  } → 28:{ v }   39:{  } → 24:{ u }
   41:{ s1 } → 36:{  }   48:{  } → 28:{ v }
 [alias] Summary of function main:
-  formals: 
-  locals: u  v  t→{ v }  a→{ v }  b→{ u }  c→{ v }  w→{ a }  
-          s1  __retres
-  returns: __retres    state: { s1->b; b }  { *w; s1->a; t; a; c }
+  formals:     returns: __retres
+  state: { s1->b; b }  { *w; s1->a; t; a; c }
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_2.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_2.res.oracle
index 80f9a772867..769efeed723 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_2.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_2.res.oracle
@@ -32,7 +32,7 @@
   0:{ res } → 1:{  }   1:{  } -fst→ 2:{  }   1:{  } -snd→ 4:{ b }
   2:{  } → 3:{  }   4:{ b } → 5:{  }
 [alias] Summary of function create_str_t:
-  formals: va  b    locals: res    returns: res    state: { res->snd; b }
+  formals: va  b    returns: res    state: { res->snd; b }
 [alias] analysing function: jfla
 [alias] analysing instruction: *(s->snd) = *(s->fst);
 [alias] May-aliases after instruction  *(s->snd) = *(s->fst);  are  <none>
@@ -49,8 +49,7 @@
 [alias] May-alias graph at the end of function jfla:
   8:{ s } → 9:{  }   9:{  } -fst→ 10:{ i1; i2 }   10:{ i1; i2 } → 12:{  }
 [alias] Summary of function jfla:
-  formals: s  i1  i2  b    locals:     returns: <none>
-  state: { s->fst; i1; i2 }
+  formals: s  i1  i2  b    returns: <none>    state: { s->fst; i1; i2 }
 [alias] analysing function: main
 [alias] analysing instruction: int u = 11;
 [alias] May-aliases after instruction  int u = 11;  are  <none>
@@ -215,9 +214,6 @@
   52:{  } -fst→ 53:{  }   52:{  } -snd→ 55:{  }   53:{  } → 54:{  }
   55:{  } → 33:{ v }   57:{ s2 } → 52:{  }   64:{  } → 33:{ v }
 [alias] Summary of function main:
-  formals: 
-  locals: u  v  t→{ v }  a→{ v }  b→{ u }  c→{ v }  x→{ a }
-           y→{ b }  z→{ c }  s1  s2  __retres
-  returns: __retres
+  formals:     returns: __retres
   state: { *x; *z; s1->fst; s2->snd; t; a; c }  { *y; s1->snd; b }
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_3.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_3.res.oracle
index e0708f5178f..5237ddd1cfe 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_3.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/ex_jfla_3.res.oracle
@@ -30,8 +30,7 @@
   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 }
+  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>
@@ -201,11 +200,7 @@
   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 }  __retres
-  returns: __retres
+  formals:     returns: __retres
   state: { x; y; z }
          { *x; *y; *z; s1->fst; s1->snd; s2->fst; s2->snd; t; a; b; c; 
            s.fst; s.snd }
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 c9b292917e6..2b5f051f79f 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle
@@ -25,6 +25,5 @@
 [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 }
+  formals:     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 be7875287ef..32f600115b8 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
@@ -24,6 +24,5 @@
 [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.t[0..]; tmp }
+  formals:     returns: <none>    state: { v.t[0..]; 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 a2bd76c05c8..c2c8ab976e0 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
@@ -13,5 +13,5 @@
 [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 }
+  formals:     returns: <none>    state: { t[0..]; tmp }
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/records.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/records.res.oracle
index 5050d1dd838..af00a8c8d95 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/records.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/records.res.oracle
@@ -47,6 +47,6 @@
   9:{ z; q } → 10:{ t }   10:{ t } -field→ 13:{ a; b; n }
   13:{ a; b; n } → 14:{ x }
 [alias] Summary of function main:
-  formals:     locals: __retres    returns: __retres
+  formals:     returns: __retres
   state: { z; q }  { z->field; q->field; a; b; n; t.field }
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
index 4578be9b905..df25a14949b 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
@@ -30,6 +30,5 @@
 [alias] May-alias graph at the end of function f:
   4:{ p } → 5:{ f; q }   5:{ f; q } → 5:{ f; q }
 [alias] Summary of function f:
-  formals:     locals: q→{ f; q }  p→{ f; q }    returns: <none>
-  state: { *p; f; q; p }
+  formals:     returns: <none>    state: { *p; f; q; p }
 [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 6e3f2b39e12..7bf7a22a6e9 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
@@ -19,5 +19,5 @@
 [alias] May-alias graph at the end of function main:
   <empty>
 [alias] Summary of function main:
-  formals:     locals: __retres    returns: __retres    state: <none>
+  formals:     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 35600d0739a..de858332e91 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
@@ -15,5 +15,5 @@
 [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>
+  formals:     returns: __retres    state: <none>
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
index 65fd01657cf..d22df63bf32 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
@@ -11,6 +11,5 @@
   0:{ flag } -r→ 1:{  }   1:{  } -v→ 2:{ o }   2:{ o } → 4:{  }
   4:{  } → 5:{  }
 [alias] Summary of function f:
-  formals: o    locals: flag    returns: <none>
-  state: { o; flag.r.v }  { *o; *(flag.r.v) }
+  formals: o    returns: <none>    state: { o; flag.r.v }  { *o; *(flag.r.v) }
 [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 3c37afd7149..ad021ebd893 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
@@ -6,7 +6,7 @@
 [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>
+  formals: line    returns: line    state: <none>
 [alias:unsafe-cast] union_vmap.c:11: Warning: 
   unsafe cast from char const * to char *; analysis may be unsound
 [alias] May-aliases after instruction  char *s2 = CPS_SplitWord((char *)"a");  are
@@ -32,12 +32,11 @@
 [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 }
+  formals:     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>
+  formals: line    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 ed3c157e85e..feef21de948 100644
--- a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
@@ -29,6 +29,5 @@
 [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 }
+  formals:     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 cf84f25b94e..175b930c1c3 100644
--- a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
@@ -25,6 +25,5 @@
 [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..] }
+  formals:     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 471e5d1851c..6a9db912e09 100644
--- a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
@@ -27,6 +27,5 @@
 [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 }
+  formals:     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 e4249a441ad..eb369e17667 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
@@ -28,6 +28,5 @@
 [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>
+  formals:     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 07d8fde2b7c..4cfb490989c 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
@@ -25,5 +25,5 @@
 [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>
+  formals:     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 225de1d3417..eefdb1052d6 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
@@ -25,5 +25,5 @@
 [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>
+  formals:     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 5e6496f281b..f7a7e1c869d 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
@@ -30,8 +30,7 @@
   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 }
+  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>
@@ -127,11 +126,7 @@
   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>
+  formals:     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 }
diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
index 8de6368366f..f9bd813190c 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
@@ -134,8 +134,7 @@
   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
+  formals:     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 70e6a01b0b6..85015cf9c50 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -84,7 +84,7 @@
   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
+  formals:     returns: __retres
   state: { t->t; z1 }  { (t->t)->c; z1->c; t->d; a }  { (t->t)->s; z1->s }
          { (t->t)->s[0..]; z1->s[0..] }
 [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 ec9e2cf954a..e637a626f9b 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
@@ -34,6 +34,5 @@
 [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 }
+  formals:     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 494d53e438c..b278d558f71 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
@@ -31,6 +31,5 @@
 [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>
+  formals:     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 c948e228972..2b7b2eb6949 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
@@ -43,6 +43,5 @@
   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 }
+  formals:     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 494f0550054..6a11ec706ed 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
@@ -41,6 +41,5 @@
 [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 }
+  formals:     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 93f0980905f..efd088f070c 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
@@ -81,7 +81,6 @@
   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
+  formals:     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 d0c1c5e7a0b..3adc34389ba 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -100,8 +100,7 @@
 [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>
+  formals: x    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 }
@@ -186,8 +185,7 @@
 [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>
+  formals: x    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>
@@ -317,8 +315,7 @@
   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 }
+  formals:     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:
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 768b61717d0..0ef06bd90ac 100644
--- a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
@@ -122,8 +122,7 @@
   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
+  formals: x    returns: __retres
   state: { x; tmp }  { x->t2; tmp->t2 }  { x->t2[0..]; tmp->t2[0..]; idata }
          { x->t1; tmp->t1 }  { x->t1[0..]; tmp->t1[0..]; odata }
 [alias] analysing function: f2
@@ -232,8 +231,7 @@
   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
+  formals: x    returns: __retres
   state: { x; tmp }  { x->t1; tmp->t1 }  { x->t1[0..]; tmp->t1[0..]; idata }
          { x->t2; tmp->t2 }  { x->t2[0..]; tmp->t2[0..]; odata }
 [alias] analysing function: main
@@ -379,8 +377,7 @@
   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 }
+  formals:     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:
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 4c9f5449cd5..23d94fe8cb7 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
@@ -8,7 +8,7 @@
 [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 }
+  formals: x  y    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>
@@ -41,5 +41,5 @@
 [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 }
+  formals:     returns: __retres    state: { a; b }
 [alias] Analysis complete
-- 
GitLab