diff options
| author | Son Ho | 2022-01-20 19:08:29 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-20 19:08:29 +0100 |
| commit | 7fcd02817f4201e81ed35bf3356095997966c8d5 (patch) | |
| tree | 54dcdb48c7ae8865867213f5301b9de2f88d9830 /src/Invariants.ml | |
| parent | ef0ca516c08d43300089a5cd3e80e9dd0bb81889 (diff) | |
Make good progress on updating InterpreterStatements to use CPS
Diffstat (limited to '')
| -rw-r--r-- | src/Invariants.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 33e7d90b..52de4c5e 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -8,6 +8,7 @@ module C = Contexts module Subst = Substitute module A = CfimAst module L = Logging +open Cps open TypesUtils open InterpreterUtils open InterpreterBorrowsCore @@ -726,3 +727,9 @@ let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit = check_borrowed_values_invariant ctx; check_typing_invariant ctx; check_symbolic_values config ctx + +(** Same as [check_invariants], but written in CPS *) +let cf_check_invariants (config : C.config) : cm_fun = + fun cf ctx -> + check_invariants config ctx; + cf ctx |