From db40e84ea6b888fefb6974f5635ac407aefef292 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 3 Jan 2022 09:12:20 +0100
Subject: Cleanup a bit and fix some issues

---
 src/Interpreter.ml        | 14 +++++++-------
 tests/trace_reference.txt | 44 ++++++++++++++++++++++----------------------
 2 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 0ce4ff99..464a7f5b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -935,7 +935,7 @@ let end_borrow_get_borrow (io : inner_outer)
               V.Bottom)
             else
               (* Update the outer borrows before diving into the borrowed value *)
-              let outer_borrows = update_outer_borrows io outer (Borrow l') in
+              let outer = update_outer_borrows io outer (Borrow l') in
               V.Borrow (super#visit_MutBorrow outer l' bv)
 
       method! visit_ALoan outer lc =
@@ -997,7 +997,7 @@ let end_borrow_get_borrow (io : inner_outer)
               V.ABottom)
             else
               (* Update the outer borrows before diving into the child avalue *)
-              let outer_borrows = update_outer_borrows io outer (Borrow bid) in
+              let outer = update_outer_borrows io outer (Borrow bid) in
               V.ABorrow (super#visit_AMutBorrow outer bid av)
         | V.ASharedBorrow bid ->
             (* Check if this is the borrow we are looking for *)
@@ -1347,7 +1347,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     loan is inside the same abstraction (in which case we don't need to end the whole
     abstraction).
  *)
-let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
+let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
     (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
@@ -1436,7 +1436,7 @@ let give_back_avalue (config : C.config) (bid : V.BorrowId.id)
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
+let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
     C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
@@ -1445,7 +1445,7 @@ let give_back_shared config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
     replaced := true
   in
   let obj =
-    object (self)
+    object
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Loan opt_abs lc =
@@ -1730,8 +1730,8 @@ and end_borrows (config : C.config) (io : inner_outer)
     (fun id ctx -> end_borrow config io allowed_abs id ctx)
     lset ctx
 
-and end_abstraction (config : C.config) (abs : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+and end_abstraction (_config : C.config) (_abs : V.AbstractionId.id)
+    (_ctx : C.eval_ctx) : C.eval_ctx =
   raise Unimplemented
 
 let end_outer_borrow config = end_borrow config Outer None
diff --git a/tests/trace_reference.txt b/tests/trace_reference.txt
index 4328c2c0..52edcc93 100644
--- a/tests/trace_reference.txt
+++ b/tests/trace_reference.txt
@@ -3961,8 +3961,8 @@ copy x
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> ⊥ : bool ;
   var@6 -> 1: i32 ;
@@ -3980,8 +3980,8 @@ return
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> ⊥ : bool ;
   var@6 -> 1: i32 ;
@@ -3997,8 +3997,8 @@ About to evaluate statement: var@5 := move var@6 == 1: i32
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> ⊥ : bool ;
   var@6 -> 1: i32 ;
@@ -4018,8 +4018,8 @@ move var@6
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> ⊥ : bool ;
   var@6 -> ⊥ : i32 ;
@@ -4036,8 +4036,8 @@ move var@6
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> true ;
   var@6 -> ⊥ : i32 ;
@@ -4054,8 +4054,8 @@ return
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> true ;
   var@6 -> ⊥ : i32 ;
@@ -4071,8 +4071,8 @@ About to evaluate statement: var@4 := ¬ move var@5
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> true ;
   var@6 -> ⊥ : i32 ;
@@ -4091,8 +4091,8 @@ true
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> false ;
   var@5 -> ⊥ : bool ;
   var@6 -> ⊥ : i32 ;
@@ -4108,8 +4108,8 @@ return
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> false ;
   var@5 -> ⊥ : bool ;
   var@6 -> ⊥ : i32 ;
@@ -4125,8 +4125,8 @@ About to evaluate statement: assert(¬move var@4)
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> false ;
   var@5 -> ⊥ : bool ;
   var@6 -> ⊥ : i32 ;
@@ -4145,8 +4145,8 @@ false
 {
   var@0 -> ⊥ : () ;
   x -> 1: i32 ;
-  px -> ⌊mut@1⌋ ;
-  ppx -> &mut@1 (⊥ : &'_ mut (i32)) ;
+  px -> ⊥ : &'_ mut (i32) ;
+  ppx -> ⊥ : &'_ mut (&'_ mut (i32)) ;
   var@4 -> ⊥ : bool ;
   var@5 -> ⊥ : bool ;
   var@6 -> ⊥ : i32 ;
-- 
cgit v1.2.3