summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-24 11:57:18 +0100
committerSon Ho2021-11-24 11:57:18 +0100
commit782499394daad2152b173218f98f53a453f1fca8 (patch)
tree2f6a628dfa9cc33d3fb65f380d9263644543d8c1
parentaf8f42e1d54600b6a3e9c8a048f63883d79248df (diff)
Update eval_operand
-rw-r--r--src/Interpreter.ml12
1 files changed, 3 insertions, 9 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 08f45052..5db82445 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1192,7 +1192,6 @@ let rec update_env_along_write_place (config : config) (access : access_kind)
in
update_env_along_write_place config access tyctx p nv env'
-(*
exception UpdateEnv of env
(** Small utility used to break control-flow *)
@@ -1202,10 +1201,6 @@ exception UpdateEnv of env
This is used when reading, borrowing, writing to a value. We typically
first call [update_env_along_read_place] or [update_env_along_write_place]
to get access to the value, then call this function to "prepare" the value.
-
- The [access_kind] controls the type of operation we will perform:
- - [Read]: copy the value, perform an immutable borrow
- - [Write]: update the value, move, mutably borrow
*)
let rec collect_borrows_at_place (config : config) (access : access_kind)
(p : place) (env : env) : env =
@@ -1245,11 +1240,11 @@ let rec collect_borrows_at_place (config : config) (access : access_kind)
| Loan lc -> (
match lc with
| SharedLoan (bids, ty) -> (
- (* End the borrows if we need a [Write] access, otherwise dive into
+ (* End the loans if we need a modification access, otherwise dive into
the shared value *)
match access with
| Read -> inspect_update ty
- | Write ->
+ | Write | Move ->
let env' = end_outer_borrows config bids env in
raise (UpdateEnv env'))
| MutLoan bid ->
@@ -1488,7 +1483,7 @@ let eval_operand (config : config) (ctx : eval_ctx) (op : operand) :
(* Move the value *)
assert (not (bottom_in_value v));
let bottom = { value = Bottom; ty = v.ty } in
- match write_place config bottom p env2 with
+ match write_place config access p bottom env2 with
| Error _ -> failwith "Unreachable"
| Ok env3 ->
let ctx3 = { ctx with env = env3 } in
@@ -1519,4 +1514,3 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
(* TODO:
update write_value
*)
- *)