diff options
| author | Son HO | 2023-12-23 01:46:58 +0100 |
|---|---|---|
| committer | GitHub | 2023-12-23 01:46:58 +0100 |
| commit | 15a7d7b7322a1cd0ebeb328fde214060e23fa8b4 (patch) | |
| tree | 6cce7d76969870f5bc18c5a7cd585e8873a1c0dc /compiler/InterpreterBorrows.ml | |
| parent | c3e0b90e422cbd902ee6d2b47073940c0017b7fb (diff) | |
| parent | 63ccbd914d5d44aa30dee38a6fcc019310ab640b (diff) | |
Merge pull request #64 from AeneasVerif/son/merge_back
Merge the forward/backward functions
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index e56919fa..a2eb2545 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1628,7 +1628,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); assert (opt_bid = None); (* Simply explore the child *) list_avalues false push_fail child_av @@ -1639,7 +1639,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) { child = child_av; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); (* Simply explore the child *) list_avalues false push_fail child_av) | ABorrow bc -> ( @@ -1659,14 +1659,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push av | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); assert (opt_bid = None); (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); (* Just explore the child *) list_avalues false push_fail child_av | AProjSharedBorrow asb -> @@ -1683,7 +1683,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_context.type_infos ty)) + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1732,7 +1732,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_context.type_infos ty)); + assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)); ([], v) in |