summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-03 09:12:20 +0100
committerSon Ho2022-01-03 09:12:20 +0100
commitdb40e84ea6b888fefb6974f5635ac407aefef292 (patch)
tree4426a0460ed085e976860224b38f3527f3cb183d
parent71c7942870c8f6c849aef974f052f6037bbd44a7 (diff)
Cleanup a bit and fix some issues
-rw-r--r--src/Interpreter.ml14
-rw-r--r--tests/trace_reference.txt44
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 ;