diff options
-rw-r--r-- | src/Interpreter.ml | 14 | ||||
-rw-r--r-- | 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 ; |