diff options
author | Son Ho | 2022-01-03 19:54:56 +0100 |
---|---|---|
committer | Son Ho | 2022-01-03 19:54:56 +0100 |
commit | bd5ddbf71c2f1df42f6e65123613c9011e016c52 (patch) | |
tree | c4ef901f7e6f35146408ad9a41197bab65b62325 /src | |
parent | 191c1eec8d3da6c2559280e085f1dc0c80296a57 (diff) |
Make minor progress on compute_expanded_symbolic_ref_value
Diffstat (limited to 'src')
-rw-r--r-- | src/Interpreter.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 02d9aff5..0b444862 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2695,6 +2695,11 @@ let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) let box_value = mk_box_value boxed_value in (ctx, box_value) +let compute_expanded_symbolic_ref_value (ended_regions : T.RegionId.set_t) + (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) : + C.eval_ctx * V.typed_value = + raise Unimplemented + (** Expand a symbolic value. Note that we return a list of contexts because when expanding enumerations @@ -2712,6 +2717,7 @@ let expand_symbolic_value (config : C.config) (expand_enumerations : bool) (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let rty = sp.V.svalue.V.sv_ty in + let ended_regions = sp.V.rset_ended in let ctx, nv = match (pe, rty) with (* "Regular" ADTs *) @@ -2724,12 +2730,13 @@ let expand_symbolic_value (config : C.config) (expand_enumerations : bool) | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> assert (arity = List.length tys); (* Generate the field values *) - compute_expanded_symbolic_tuple_value sp.V.rset_ended tys ctx + compute_expanded_symbolic_tuple_value ended_regions tys ctx (* Borrows *) - | Deref, T.Ref (_, _, _) -> raise Unimplemented + | Deref, T.Ref (region, ref_ty, rkind) -> + compute_expanded_symbolic_ref_value ended_regions region ref_ty rkind (* Boxes *) | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - compute_expanded_symbolic_box_value sp.V.rset_ended boxed_ty ctx + compute_expanded_symbolic_box_value ended_regions boxed_ty ctx | _ -> failwith ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) |