diff options
author | Son Ho | 2022-02-08 20:49:46 +0100 |
---|---|---|
committer | Son Ho | 2022-02-08 20:49:46 +0100 |
commit | bbb1ea77402545d52af0bb0076923d99ecc4c9e2 (patch) | |
tree | e530d8a5882cb82b68497f24b1a6ede09874ec99 /src/Invariants.ml | |
parent | fb013997dda4c01fdc395ab52ba9dc3669f3d71a (diff) |
Add an option to allow the presence of bottom values below borrows
Diffstat (limited to '')
-rw-r--r-- | src/Invariants.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index fff5b897..0e4b1e23 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -298,14 +298,15 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = - borrows/loans can't contain ⊥ or inactivated mut borrows - shared loans can't contain mutable loans *) -let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = +let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) : + unit = let visitor = object inherit [_] C.iter_eval_ctx as super method! visit_Bottom info = (* No ⊥ inside borrowed values *) - assert (not info.outer_borrow) + assert (config.C.allow_bottom_below_borrow || not info.outer_borrow) method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -784,7 +785,7 @@ let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit = if config.C.check_invariants then ( log#ldebug (lazy "Checking invariants"); check_loans_borrows_relation_invariant ctx; - check_borrowed_values_invariant ctx; + check_borrowed_values_invariant config ctx; check_typing_invariant ctx; check_symbolic_values config ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") |