summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-17 16:22:32 +0100
committerSon Ho2021-12-17 16:22:32 +0100
commit05b0bf5202aea7d55fee822e7607e70b3d6d98b6 (patch)
tree3eebb6721d5667227c8f540e3573274ff8257e4e
parentf6c1c4ab8898176a7866b4f277b0d991e1a8f9d3 (diff)
Fix some issues
-rw-r--r--src/Interpreter.ml13
1 files changed, 8 insertions, 5 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 133de215..c39387a7 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -66,7 +66,7 @@ let borrow_in_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrows) : bool
(** TODO: move *)
let remove_borrow_from_asb (bid : V.BorrowId.id)
- (asb : V.abstract_shared_borrows) : bool =
+ (asb : V.abstract_shared_borrows) : V.abstract_shared_borrows =
let removed = ref 0 in
let asb =
List.filter
@@ -680,7 +680,10 @@ let rec apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
let value : V.avalue =
match (v.V.value, ty) with
| V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
- | V.Adt v, T.Adt (id, regions, tys) -> raise Unimplemented
+ | V.Adt adt, T.Adt (id, regions, tys) ->
+ (* Retrieve the types of the fields *)
+ (* Explore the field values *)
+ raise Unimplemented
| V.Bottom, _ -> failwith "Unreachable"
| V.Borrow bc, T.Ref (r, ref_ty, kind) ->
if
@@ -848,7 +851,7 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child)
| V.AIgnoredSharedLoan asb ->
(* Nothing special to do *)
- ()
+ V.ALoan (super#visit_AIgnoredSharedLoan outer asb)
(** We reimplement [visit_ALoan] because we may have to update the
outer borrows *)
@@ -902,8 +905,8 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
set_replaced_bc (Abstract bc);
(* Update the value - note that we are necessarily in the second
* of the two cases described above *)
- let asb = removed_borrow_from_asb l asb in
- V.AIgnoredSharedBorrow asb)
+ let asb = remove_borrow_from_asb l asb in
+ V.ABorrow (V.AIgnoredSharedBorrow asb))
else
(* Nothing special to do *)
V.ABorrow (super#visit_AIgnoredSharedBorrow outer asb)