summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-12 14:23:10 +0100
committerSon Ho2022-01-12 14:23:10 +0100
commitce333b8591d7fd856aa16d54c0a0abbc8983fc63 (patch)
treebe53b580473030a8da8622005560cfcd7adc74b6
parentf2dd12e889cca6e75b03868a7d31952c8bdfa9c7 (diff)
Make minor modifications
-rw-r--r--src/InterpreterPaths.ml2
-rw-r--r--src/InterpreterStatements.ml4
-rw-r--r--src/Values.ml2
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