summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-21 11:09:11 +0100
committerSon Ho2022-01-21 11:09:11 +0100
commit54e493eaede8907496487e41070347fa0d0b22c9 (patch)
tree7b3a6beef09660d7c25255caff3e7006071f9680 /src
parent21fec40e3bee3d0544a76fc553067a0928c73b95 (diff)
Make minor modifications for the invariants checks
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterStatements.ml12
-rw-r--r--src/Invariants.ml11
2 files changed, 9 insertions, 14 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index edc3bef1..d76def43 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -714,10 +714,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
* checking the invariants *)
let cc = greedy_expand_symbolic_values config in
(* Sanity check *)
- let cc =
- if config.C.check_invariants then comp cc (Inv.cf_check_invariants config)
- else cc
- in
+ let cc = comp cc (Inv.cf_check_invariants config) in
(* Evaluate *)
let cf_eval_st cf : m_fun =
@@ -1160,12 +1157,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
* checking the invariants *)
let cc = greedy_expand_symbolic_values config in
(* Sanity check *)
- let cc =
- if config.C.check_invariants then
- comp_check_ctx cc (Inv.check_invariants config)
- else cc
- in
-
+ let cc = comp_check_ctx cc (Inv.check_invariants config) in
(* Continue *)
cc (cf res)
in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5e114c19..b16e71d0 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -766,10 +766,13 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
M.iter check_info !infos
let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
- check_loans_borrows_relation_invariant ctx;
- check_borrowed_values_invariant ctx;
- check_typing_invariant ctx;
- check_symbolic_values config ctx
+ if config.C.check_invariants then (
+ log#ldebug (lazy "Checking invariants");
+ check_loans_borrows_relation_invariant ctx;
+ check_borrowed_values_invariant ctx;
+ check_typing_invariant ctx;
+ check_symbolic_values config ctx)
+ else log#ldebug (lazy "Not checking invariants (check is not activated)")
(** Same as [check_invariants], but written in CPS *)
let cf_check_invariants (config : C.config) : cm_fun =