Merge pull request #65 from AeneasVerif/son/fix_loops

Fix an issue with loops

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 =