diff options
| -rw-r--r-- | src/InterpreterPaths.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
3 files changed, 7 insertions, 1 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 491e4c21..bf039b52 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -730,6 +730,8 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) trait (i.e., by calling a dedicated function). This is why we added a parameter to control this copy. Note that here by ADT we mean the user-defined ADTs (not tuples or assumed types). + + TODO: move *) let rec copy_value (allow_adt_copy : bool) (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 917f1265..38813894 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -36,6 +36,7 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) (p : E.place) : C.eval_ctx = (* Prepare the destination *) + (* TODO: there might be a problem because the value to assign is hanging in the air ! *) let ctx, _ = prepare_lplace config p ctx in (* Update the destination *) let ctx = write_place_unwrap config Write p v ctx in @@ -817,6 +818,9 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) (* Pop the stack frame and retrieve the return value *) let ctx, ret_value = ctx_pop_frame config ctx in + (* TODO: there might be a problem because the return value + * if hanging in the air while we assign to place! *) + (* Move the return value to its destination *) let ctx = assign_to_place config ctx ret_value dest in diff --git a/src/Values.ml b/src/Values.ml index bcb08dc8..e8d4560e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -422,7 +422,7 @@ and aborrow_content = > x -> shared_loan {l0} (U32 0) > px -> ⊥ - > abs0 { a_shared_bororw l0 } + > abs0 { a_shared_borrow l0 } ``` *) | AIgnoredMutBorrow of BorrowId.id option * typed_avalue |