diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 10 |
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) |