Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2

Complete the constants extraction by making all functions fail

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