summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-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 =