Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

1 files changed, 10 insertions, 6 deletions

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 8a924a0a..992146de 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -250,12 +250,16 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                     Ok (ctx, { res with updated = nv })
               else Error (FailSharedLoan bids))
       | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r ->
-          let pe, v, ty = r in
-          let pe = "- pe: " ^ show_projection_elem pe in
-          let v = "- v:\n" ^ show_value v in
-          let ty = "- ty:\n" ^ show_ety ty in
-          craise __FILE__ __LINE__ span
-            ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
+          if v.value = VBottom then
+            craise __FILE__ __LINE__ span
+              "Can not apply a projection to the ⊥ value"
+          else
+            let pe, v, ty = r in
+            let pe = "- pe: " ^ show_projection_elem pe in
+            let v = "- v:\n" ^ show_value v in
+            let ty = "- ty:\n" ^ show_ety ty in
+            craise __FILE__ __LINE__ span
+              ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
 
 (** Generic function to access (read/write) the value at a given place.