diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f43848e6..f8f991c6 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -804,3 +804,29 @@ let rec update_env_along_read_place (config : config) (access : path_access) failwith "Unreachable" in update_env_along_read_place config access p env' + +(** Update the environment to be able to write to a place. + + See [update_env_alond_read_place]. +*) +let rec update_env_along_write_place (config : config) + (tyctx : type_def TypeDefId.vector) (nv : typed_value) (p : place) + (env : env) : env = + (* Attempt to write the place: if it fails, update the environment and retry *) + match write_place config nv p env with + | Ok v -> env + | Error err -> + let env' = + match err with + | FailSharedLoan bids -> end_borrows config bids env + | FailMutLoan bid -> end_borrow config bid env + | FailInactivatedMutBorrow bid -> + activate_inactivated_mut_borrow config bid env + | FailSymbolic (pe, sp) -> + (* Expand the symbolic value *) + raise Unimplemented + | FailBottom (remaining_pes, pe, ty) -> + (* Expand the [Bottom] value *) + expand_bottom_value config tyctx p env remaining_pes pe ty + in + update_env_along_write_place config tyctx nv p env' |