diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterExpansion.ml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 544cc64a..85259b89 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -247,6 +247,17 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types +(** Compute the expansion of an Option value. + *) +let compute_expanded_symbolic_option_value (expand_enumerations : bool) + (kind : V.sv_kind) (ty : T.rty) : V.symbolic_expansion list = + assert expand_enumerations; + let some_se = + V.SeAdt (Some T.option_some_id, [ mk_fresh_symbolic_value kind ty ]) + in + let none_se = V.SeAdt (Some T.option_none_id, []) in + [ none_se; some_se ] + let compute_expanded_symbolic_tuple_value (kind : V.sv_kind) (field_types : T.rty list) : V.symbolic_expansion = (* Generate the field values *) @@ -481,6 +492,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let cc : cm_fun = fun cf ctx -> match rty with + (* TODO: I think it is possible to factorize a lot the below match *) (* "Regular" ADTs *) | T.Adt (T.AdtId def_id, regions, types) -> (* Compute the expanded value *) @@ -494,6 +506,22 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let seel = List.map (fun see -> (Some see, cf)) seel in apply_branching_symbolic_expansions_non_borrow config original_sv original_sv_place seel ctx + (* Options *) + | T.Adt (T.Assumed Option, regions, types) -> + (* Sanity check *) + assert (regions = []); + let ty = Collections.List.to_cons_nil types in + (* Compute the expanded value *) + let seel = + compute_expanded_symbolic_option_value allow_branching sp.sv_kind ty + in + + (* Check for branching *) + assert (List.length seel <= 1 || allow_branching); + (* Apply *) + let seel = List.map (fun see -> (Some see, cf)) seel in + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx (* Tuples *) | T.Adt (T.Tuple, [], tys) -> (* Generate the field values *) |