summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 22:13:20 +0100
committerSon Ho2022-01-04 22:13:20 +0100
commite70b541f6c3b6fb29f9807258cc88b4d88178f6a (patch)
treed4e78a88b0b50f2a9e6fe4872a040a56dfce49de /src
parent1ccba902961e20c098fd02224915f74e08c594a6 (diff)
Implement check_constant_value_type
Diffstat (limited to 'src')
-rw-r--r--src/Invariants.ml10
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