summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
authorSon Ho2021-11-22 10:25:09 +0100
committerSon Ho2021-11-22 10:25:09 +0100
commit61e54d5c7fa5e8662d8cc438f4f2bd4856bf3ca6 (patch)
treee279ea490bd1522822bdd7b4d65a4d08b86c50f8 /src/Values.ml
parentc1f628b7fde13df56bc7e71f1619f4427ed157dc (diff)
Implement typed_avalue_to_string_
Diffstat (limited to '')
-rw-r--r--src/Values.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 5ebc97b0..d63ace85 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -146,9 +146,9 @@ and aadt_value = {
and aloan_content =
| AMutLoan of BorrowId.id * typed_avalue
- | ASharedLoan of BorrowId.Set.t * value * typed_avalue
- | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *)
- | AEndedSharedLoan of value * typed_avalue
+ | ASharedLoan of BorrowId.Set.t * typed_value * typed_avalue
+ | AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
+ | AEndedSharedLoan of typed_value * typed_avalue
| AIgnoredMutLoan of BorrowId.id * typed_avalue
| AIgnoredSharedLoan of abstract_shared_borrows
@@ -159,7 +159,7 @@ and aborrow_content =
| AMutBorrow of BorrowId.id * typed_avalue
| ASharedBorrow of BorrowId.id
| AIgnoredMutBorrow of typed_avalue
- | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *)
+ | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
| AIgnoredSharedBorrow of abstract_shared_borrows
and aassumed_value = ABox of typed_avalue