diff options
Diffstat (limited to 'src/InterpreterStatements.ml')
| -rw-r--r-- | src/InterpreterStatements.ml | 17 |
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 *) |