diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 12 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
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 |