diff options
| author | Son Ho | 2022-01-21 11:09:11 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-21 11:09:11 +0100 |
| commit | 54e493eaede8907496487e41070347fa0d0b22c9 (patch) | |
| tree | 7b3a6beef09660d7c25255caff3e7006071f9680 /src | |
| parent | 21fec40e3bee3d0544a76fc553067a0928c73b95 (diff) | |
Make minor modifications for the invariants checks
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterStatements.ml | 12 | ||||
| -rw-r--r-- | src/Invariants.ml | 11 |
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 = |