summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 22:10:08 +0100
committerSon Ho2022-01-04 22:10:08 +0100
commit1ccba902961e20c098fd02224915f74e08c594a6 (patch)
tree2f4edabc64ac6c9a85d044d5d9e558952f113b01 /src
parent6ca4bee9d52a2d9c9e246ef8116121d9018ca101 (diff)
Start working on check_typing_invariant
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml24
1 files changed, 23 insertions, 1 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index b67fa3a2..0478459b 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -9,6 +9,7 @@ module Subst = Substitute
module A = CfimAst
module L = Logging
open InterpreterUtils
+open Errors
let debug_invariants : bool ref = ref false
@@ -333,7 +334,28 @@ 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_typing_invariant (_ctx : C.eval_ctx) : unit = ()
+let check_typing_invariant (ctx : C.eval_ctx) : unit =
+ let visitor =
+ object
+ inherit [_] C.iter_eval_ctx as super
+
+ 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.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");
+ (* Continue exploring to inspect the subterms *)
+ super#visit_typed_value info tv
+
+ method! visit_typed_avalue info atv = raise Unimplemented
+ end
+ in
+ visitor#visit_eval_ctx () ctx
let check_invariants (ctx : C.eval_ctx) : unit =
check_loans_borrows_relation_invariant ctx;