summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 638e8b45..c5a1dad1 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -556,18 +556,15 @@ let rec read_projection (config : config) (access : path_access) (env : env)
match FieldId.nth_opt adt.field_values field_id with
| None -> unreachable __LOC__
| Some fv -> read_projection config access env p fv)
- | _, Adt _ -> unreachable __LOC__
(* Tuples *)
| Field (ProjTuple _, field_id), Tuple values -> (
match FieldId.nth_opt values field_id with
| None -> unreachable __LOC__
| Some fv -> read_projection config access env p fv)
- | _, Tuple _ -> unreachable __LOC__
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *)
| Field (ProjAdt (_, Some _variant_id), _), Bottom ->
Error (FailBottom (1 + List.length p', pe, v.ty))
- | _, Bottom -> unreachable __LOC__
(* Symbolic value: needs to be expanded *)
| _, Symbolic sp ->
assert (config.mode = SymbolicMode);
@@ -586,7 +583,12 @@ let rec read_projection (config : config) (access : path_access) (env : env)
| _, MutBorrow (_, bv) -> read_projection config access env p' bv
| _, InactivatedMutBorrow bid ->
Error (FailInactivatedMutBorrow bid))
- | _, (Concrete _ | Assumed _ | Borrow _ | Loan _) ->
+ (* Remaining cases: error. We enumerate all the value variants
+ * on purpose, to make sure we statically catch errors if we
+ * modify the [value] definition. *)
+ | ( _,
+ ( Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _
+ | Loan _ ) ) ->
unreachable __LOC__)
(* Entering loans failed *)
| res -> res)