1 files changed, 500 insertions, 2 deletions

diff --git a/tests/trace_reference.txt b/tests/trace_reference.txt
index b816c763..f69eff48 100644
--- a/tests/trace_reference.txt
+++ b/tests/trace_reference.txt
@@ -174,7 +174,27 @@ fn test_neg1() {
   return
 }
 
-fn refs_test() {
+fn refs_test1() {
+  var@0 : ();
+  x : i32;
+  px : &'_ mut (i32);
+  ppx : &'_ mut (&'_ mut (i32));
+  var@4 : bool;
+  var@5 : bool;
+  var@6 : i32;
+
+  x := 0: i32
+  px := &mut x
+  ppx := &mut px
+  *(*(ppx)) := 1: i32
+  var@6 := copy x
+  var@5 := move var@6 == 1: i32
+  var@4 := ¬ move var@5
+  assert(¬move var@4)
+  return
+}
+
+fn refs_test2() {
   var@0 : ();
   x : i32;
   y : i32;
@@ -3684,7 +3704,485 @@ About to evaluate statement: y := -3: i32
 
 About to evaluate statement: return
 
-[Debug] test_unit_function: refs_test
+[Debug] test_unit_function: refs_test1
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⊥ : i32 ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: x := 0: i32
+px := &mut x
+ppx := &mut px
+*(*(ppx)) := 1: i32
+var@6 := copy x
+var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⊥ : i32 ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: x := 0: i32
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⊥ : i32 ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+0: i32
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 0: i32 ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: px := &mut x
+ppx := &mut px
+*(*(ppx)) := 1: i32
+var@6 := copy x
+var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 0: i32 ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: px := &mut x
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> &mut@0 (0: i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: ppx := &mut px
+*(*(ppx)) := 1: i32
+var@6 := copy x
+var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> &mut@0 (0: i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: ppx := &mut px
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (0: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: *(*(ppx)) := 1: i32
+var@6 := copy x
+var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (0: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: *(*(ppx)) := 1: i32
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (0: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+1: i32
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (1: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: var@6 := copy x
+var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (1: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: var@6 := copy x
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (1: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+copy x
+
+[Debug] end_borrow 0: context before:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> ⌊mut@0⌋ ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (&mut@0 (1: i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+[Debug] end_borrow 0: context after:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+[Debug] Value to copy:
+1: i32
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> 1: i32 ;
+}
+
+About to evaluate statement: var@5 := move var@6 == 1: i32
+var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> 1: i32 ;
+}
+
+About to evaluate statement: var@5 := move var@6 == 1: i32
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> 1: i32 ;
+}
+
+
+- op:
+move var@6
+
+[Debug] Value to move:
+1: i32
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+1: i32
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> true ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: var@4 := ¬ move var@5
+assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> true ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: var@4 := ¬ move var@5
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> true ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+move var@5
+
+[Debug] Value to move:
+true
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> false ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: assert(¬move var@4)
+return
+
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> false ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: assert(¬move var@4)
+
+[Debug] eval_operand:
+- ctx:
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> false ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+
+- op:
+move var@4
+
+[Debug] Value to move:
+false
+[Debug] 
+# 1 frame(s)
+
+# Frame 0:
+{
+  var@0 -> ⊥ : () ;
+  x -> 1: i32 ;
+  px -> ⌊mut@1⌋ ;
+  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  var@4 -> ⊥ : bool ;
+  var@5 -> ⊥ : bool ;
+  var@6 -> ⊥ : i32 ;
+}
+
+About to evaluate statement: return
+
+[Debug] test_unit_function: refs_test2
 [Debug] 
 # 1 frame(s)