diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Invariants.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 0478459b..e1ba0b22 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -334,6 +334,12 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let info = { outer_borrow = false; outer_shared = false } in visitor#visit_eval_ctx info ctx +let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit = + match (cv, ty) with + | V.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty) + | V.Bool _, T.Bool | V.Char _, T.Char | V.String _, T.Str -> () + | _ -> failwith "Erroneous typing" + let check_typing_invariant (ctx : C.eval_ctx) : unit = let visitor = object @@ -342,13 +348,13 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = method! visit_typed_value info tv = (* Check this pair (value, type) *) (match (tv.V.value, tv.V.ty) with - | V.Concrete cv, _ -> raise Unimplemented + | V.Concrete cv, ty -> check_constant_value_type cv ty | V.Adt av, _ -> raise Unimplemented | V.Bottom, _ -> (* Nothing to check *) () | V.Borrow bc, _ -> raise Unimplemented | V.Loan lc, _ -> raise Unimplemented | V.Symbolic spc, _ -> raise Unimplemented - | _ -> failwith "Inconsistent typing"); + | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv |