summaryrefslogtreecommitdiff
path: root/compiler/InterpreterUtils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterUtils.ml')
-rw-r--r--compiler/InterpreterUtils.ml30
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 =