diff options
author | Son Ho | 2024-06-05 16:12:15 +0200 |
---|---|---|
committer | Son Ho | 2024-06-05 16:12:15 +0200 |
commit | a6c9ab139977982f610f3d46e2e2f4c141880c3c (patch) | |
tree | fa009e747aa09d9ab610cbcc13112f844b890a7c /compiler/InterpreterLoopsMatchCtxs.ml | |
parent | bb1caf9a8efdadd599560b3ff7a12d275a12f696 (diff) |
Relax some constraints in the symbolic execution when borrow-checking
Diffstat (limited to '')
-rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 3f7c023e..a1c0841a 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span) | Loop (loop_id', rg_id, kind) -> sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span; sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span; - let can_end = false in + (* If we borrow-check: we can set the abstractions as endable. + If we synthesize we have to constrain the region abstractions + a bit. *) + let can_end = !Config.borrow_check in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in super#visit_abs env abs |