diff options
Diffstat (limited to 'src/InterpreterPaths.ml')
| -rw-r--r-- | src/InterpreterPaths.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 52742703..edd27138 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -304,7 +304,11 @@ let access_kind_to_projection_access (access : access_kind) : projection_access lookup_shared_borrows = false; } -(** Read the value at a given place *) +(** Read the value at a given place. + + Note that we only access the value at the place, and do not check that + the value is "well-formed" (for instance that it doesn't contain bottoms). + *) let read_place (config : C.config) (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : V.typed_value path_access_result = let access = access_kind_to_projection_access access in |