summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-17 10:24:00 +0100
committerSon Ho2021-12-17 10:24:00 +0100
commited1562db8a72631e36b89171b377e395cb0f8632 (patch)
tree904d95b499bca3eb9bd685c76bb93a4a51962f97 /src
parent2e784a2cd8162bdc08b7533ab73ffec9bcd52147 (diff)
Make minor modifications
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml12
-rw-r--r--src/Values.ml2
2 files changed, 14 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 4ea95028..8948701f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -846,6 +846,18 @@ let give_back_shared_to_abs _config _bid _abs : V.abs =
*)
let give_back_value (config : C.config) (bid : V.BorrowId.id)
(v : V.typed_value) (env : C.env) : C.env =
+ (* TODO:
+ (* We use a reference to check that we updated exactly one borrow *)
+ let replaced : bool ref = ref false in
+ let set_replaced () =
+ assert (not !replaced);
+ replaced := true
+ in
+ let obj =
+ object
+ inherit [_] C.map_env
+ end
+ in*)
let give_back_value_to_env_elem ev : C.env_elem =
match ev with
| C.Var (vid, destv) ->
diff --git a/src/Values.ml b/src/Values.ml
index 8c4c689c..3905d96e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -241,6 +241,8 @@ and aloan_content =
note independent of the parent avalues. For instance, a value
`AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is
to be seen like a `mut_borrow ... (mut_borrow ...)`.
+
+ TODO: be more precise about the ignored vlaues
*)
and aborrow_content =
| AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue