diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterUtils.ml | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index a1a06ee5..0817b111 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -236,28 +236,38 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t) let regions = ty_regions s.sv_ty in not (RegionId.Set.disjoint regions ended_regions) +let bottom_in_value_visitor (ended_regions : RegionId.Set.t) = + object + inherit [_] iter_typed_value + method! visit_VBottom _ = raise Found + + method! visit_symbolic_value _ s = + if symbolic_value_has_ended_regions ended_regions s then raise Found + else () + end + (** Check if a {!type:Values.value} contains [⊥]. Note that this function is very general: it also checks wether symbolic values contain already ended regions. *) let bottom_in_value (ended_regions : RegionId.Set.t) (v : typed_value) : bool = - let obj = - object - inherit [_] iter_typed_value - method! visit_VBottom _ = raise Found - - method! visit_symbolic_value _ s = - if symbolic_value_has_ended_regions ended_regions s then raise Found - else () - end - in + let obj = bottom_in_value_visitor ended_regions in (* We use exceptions *) try obj#visit_typed_value () v; false with Found -> true +let bottom_in_adt_value (ended_regions : RegionId.Set.t) (v : adt_value) : bool + = + let obj = bottom_in_value_visitor ended_regions in + (* We use exceptions *) + try + obj#visit_adt_value () v; + false + with Found -> true + let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx) (v : typed_value) : bool = let obj = |