diff options
Diffstat (limited to 'src/InterpreterPaths.ml')
| -rw-r--r-- | src/InterpreterPaths.ml | 2 |
1 files changed, 2 insertions, 0 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 = |