diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 1 | ||||
| -rw-r--r-- | src/Invariants.ml | 13 | ||||
| -rw-r--r-- | src/Print.ml | 1 | ||||
| -rw-r--r-- | src/Values.ml | 1 |
5 files changed, 11 insertions, 8 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 067b867e..ebfd87c7 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -978,7 +978,7 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) method! visit_ASymbolic _ sproj = match sproj with - | V.AProjBorrows (_, _) -> () + | V.AProjBorrows (_, _) | V.AEndedProjLoans | V.AEndedProjBorrows -> () | V.AProjLoans sv -> raise (FoundSymbolicValue sv) end in @@ -1064,6 +1064,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) | V.AProjLoans _ -> failwith "Unexpected" | V.AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty)) + | V.AEndedProjLoans | V.AEndedProjBorrows -> () end in (* Lookup the abstraction *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 9b272db8..65502126 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -226,6 +226,7 @@ let bottom_in_avalue (ended_regions : T.RegionId.set_t) (v : V.typed_avalue) : match ap with | V.AProjLoans _sv -> () | V.AProjBorrows (_sv, _rty) -> () + | V.AEndedProjLoans | V.AEndedProjBorrows -> () end in (* We use exceptions *) diff --git a/src/Invariants.ml b/src/Invariants.ml index 3fc390b5..23f7d456 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -593,14 +593,13 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = assert (child.V.ty = borrowed_aty) | V.AIgnoredSharedLoan child_av -> assert (child_av.V.ty = aloan_get_expected_child_type aty)) - | V.ASymbolic aproj, ty -> + | V.ASymbolic aproj, ty -> ( let ty1 = Subst.erase_regions ty in - let ty2 = - match aproj with - | V.AProjLoans sv | V.AProjBorrows (sv, _) -> - Subst.erase_regions sv.V.sv_ty - in - assert (ty1 = ty2) + match aproj with + | V.AProjLoans sv | V.AProjBorrows (sv, _) -> + let ty2 = Subst.erase_regions sv.V.sv_ty in + assert (ty1 = ty2) + | V.AEndedProjLoans | V.AEndedProjBorrows -> ()) | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv diff --git a/src/Print.ml b/src/Print.ml index 3869012a..d7830549 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -363,6 +363,7 @@ module Values = struct | ABorrow bc -> aborrow_content_to_string fmt bc | ALoan lc -> aloan_content_to_string fmt lc | ASymbolic s -> aproj_to_string fmt s + | AIgnored -> "_" and aloan_content_to_string (fmt : value_formatter) (lc : V.aloan_content) : string = diff --git a/src/Values.ml b/src/Values.ml index 41d8bd85..707986f8 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -250,6 +250,7 @@ type avalue = | ALoan of aloan_content | ABorrow of aborrow_content | ASymbolic of aproj + | AIgnored (** A value we don't own and thus ignore *) and adt_avalue = { variant_id : (VariantId.id option[@opaque]); |