diff options
| author | Son Ho | 2022-01-25 23:11:05 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-25 23:11:05 +0100 |
| commit | 592a2113734078290d4406df7804bfc128865958 (patch) | |
| tree | 015864f2dbf6f09ec1ac243d95e1818292608cd4 /src/SymbolicAstUtils.ml | |
| parent | 0a93309c8dc40fcda0bfb7f72bb8af38fcc14afd (diff) | |
Use msymbolic_value instead of mvalue in some places in Values.aproj
Diffstat (limited to '')
| -rw-r--r-- | src/SymbolicAstUtils.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml index 264f9cad..5a329c8d 100644 --- a/src/SymbolicAstUtils.ml +++ b/src/SymbolicAstUtils.ml @@ -9,9 +9,9 @@ open InterpreterUtils type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's -type ended_loan = (V.mvalue, V.mvalue list) ended +type ended_loan = (V.typed_value, V.msymbolic_value list) ended -type ended_borrow = (V.mvalue, V.mvalue) ended +type ended_borrow = (V.typed_value, V.typed_value) ended type ended_loan_or_borrow = | EndedLoan of ended_loan @@ -45,7 +45,7 @@ let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list match aproj with | AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) - add_sloan [ mk_typed_value_from_symbolic_value msv ] + add_sloan [ msv ] | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl) | AEndedProjBorrows mv -> add_sborrow mv | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> |