diff options
| author | Son Ho | 2022-01-13 21:24:58 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-13 21:24:58 +0100 |
| commit | e9c3dfc34d7cac0d2449b4d11db5adf7218b25db (patch) | |
| tree | ac838adf50a7051918a9d2169f139b03bde14173 /src/InterpreterUtils.ml | |
| parent | 01cde7e6ddc047c2ea13365a67555ed1defbe1e4 (diff) | |
Introduce ended borrow/loan projectors over symbolic values
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterUtils.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index ce6bd0ce..9b272db8 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -133,6 +133,9 @@ exception FoundGLoanContent of g_loan_content exception FoundSymbolicValue of V.symbolic_value (** Utility exception *) +exception FoundAProjBorrows of V.symbolic_value * T.rty +(** Utility exception *) + let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : bool = let obj = @@ -146,6 +149,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : match aproj with | AProjLoans sv | AProjBorrows (sv, _) -> if sv.V.sv_id = sv_id then raise Found else () + | AEndedProjLoans | AEndedProjBorrows -> () method! visit_abstract_shared_borrows _ asb = let visit (asb : V.abstract_shared_borrow) : unit = |