diff options
| author | Son Ho | 2022-01-26 23:26:29 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-26 23:26:29 +0100 |
| commit | db1ebd1f10eaba7627d50272ec3191f470089ee3 (patch) | |
| tree | 37bace04b8bd40cdad97abf4420039c499fdea83 /src | |
| parent | b1105c75ea54f38155ca86c62711082ce0bc325d (diff) | |
Fix a bug in the end borrows/abs loop detection
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index d2964c90..20314120 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1083,8 +1083,8 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) (* End the corresponding borrows *) let cc : cm_fun = match bids with - | Borrow bid -> end_outer_borrow config bid - | Borrows bids -> end_outer_borrows config bids + | Borrow bid -> end_borrow config chain None bid + | Borrows bids -> end_borrows config chain None bids in (* Reexplore, looking for loans *) let cc = comp cc (end_abstraction_loans config chain abs_id) in @@ -1387,10 +1387,10 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) (* Continue *) cc cf ctx -and end_outer_borrow config : V.BorrowId.id -> cm_fun = +let end_outer_borrow config : V.BorrowId.id -> cm_fun = end_borrow config [] None -and end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = +let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = end_borrows config [] None (** Helper function: see [activate_inactivated_mut_borrow]. |