Add an optional borrow identifier to AIgnoredMutBorrow, introduce the

AEndedIgnoredMutBorrow variant and fix a couple of bugs

1 files changed, 15 insertions, 2 deletions

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 36d11a9e..82f95556 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -815,6 +815,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
   (* Create the abstractions from the region groups and add them to the context *)
+  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+    ref V.AbstractionId.Map.empty
+  in
   let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
     let abs_id = rg.A.id in
     let parents =
@@ -827,17 +830,27 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
         (fun s rid -> T.RegionId.Set.add rid s)
         T.RegionId.Set.empty rg.A.regions
     in
+    let ancestors_regions =
+      List.fold_left
+        (fun acc parent_id ->
+          T.RegionId.Set.union acc
+            (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+        regions rg.A.parents
+    in
+    abs_to_ancestors_regions :=
+      V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions;
     (* Project over the input values *)
     let ctx, args_projs =
       List.fold_left_map
         (fun ctx (arg, arg_rty) ->
-          apply_proj_borrows_on_input_value config ctx regions arg arg_rty)
+          apply_proj_borrows_on_input_value config ctx regions ancestors_regions
+            arg arg_rty)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
     let avalues = List.append args_projs [ ret_av ] in
     (* Create the abstraction *)
-    let abs = { V.abs_id; parents; regions; avalues } in
+    let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
     (* Insert the abstraction in the context *)
     let ctx = { ctx with env = Abs abs :: ctx.env } in
     (* Return *)