summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml38
1 files changed, 18 insertions, 20 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5db49935..3d3d7129 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2651,30 +2651,28 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
let ended_regions = sp.V.rset_ended in
match rty with
(* The value should be a "regular" ADTs *)
- | T.Adt (T.AdtId def_id, regions, types) -> (
+ | T.Adt (T.AdtId def_id, regions, types) ->
(* Compute the expanded value - there should be exactly one because we
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = true in
- match
+ let res =
compute_expanded_symbolic_adt_value expand_enumerations ended_regions
def_id regions types ctx
- with
- | res ->
- (* Update the synthesized program *)
- let seel = List.map (fun (_, x) -> x) res in
- S.synthesize_symbolic_expansion_branching original_sv seel;
- (* Apply in the context *)
- let apply (ctx, see) : C.eval_ctx =
- let ctx =
- apply_symbolic_expansion_non_borrow config original_sv see ctx
- in
- (* Sanity check: the symbolic value has disappeared *)
- assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
- (* Return *)
- ctx
- in
- List.map apply res
- | _ -> failwith "Unexpected")
+ in
+ (* Update the synthesized program *)
+ let seel = List.map (fun (_, x) -> x) res in
+ S.synthesize_symbolic_expansion_branching original_sv seel;
+ (* Apply in the context *)
+ let apply (ctx, see) : C.eval_ctx =
+ let ctx =
+ apply_symbolic_expansion_non_borrow config original_sv see ctx
+ in
+ (* Sanity check: the symbolic value has disappeared *)
+ assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
+ (* Return *)
+ ctx
+ in
+ List.map apply res
| _ -> failwith "Unexpected"
(** Update the environment to be able to read a place.
@@ -3318,7 +3316,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
let access = Read in
let ctx, v = prepare_rplace config access p ctx in
match v.V.value with
- | Adt av -> [ eval_rvalue_discriminant_concrete config p ctx ]
+ | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ]
| Symbolic sv ->
(* Expand the symbolic value - may lead to branching *)
let ctxl = expand_symbolic_enum_value config sv ctx in