diff options
Diffstat (limited to 'src/InterpreterUtils.ml')
-rw-r--r-- | src/InterpreterUtils.ml | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index ca437593..be899c08 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -224,3 +224,25 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) : obj#visit_typed_value () v; false with Found -> true + +let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx) + (v : V.typed_value) : bool = + let obj = + object + inherit [_] V.iter_typed_value + + method! visit_symbolic_value _ s = + match s.sv_kind with + | V.FunCallRet -> + if ty_has_borrow_below_mut ctx.type_context.type_infos s.sv_ty then + raise Found + else () + | V.SynthInput -> () + | V.FunCallGivenBack | V.SynthGivenBack -> failwith "Unreachable" + end + in + (* We use exceptions *) + try + obj#visit_typed_value () v; + false + with Found -> true |