summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/SymbolicToPure.ml16
1 files changed, 15 insertions, 1 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 469021a0..bae2925b 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -406,7 +406,21 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
let scrutinee = Place (mk_place_from_var scrutinee_var) in
(* Translate the branches *)
match exp with
- | ExpandNoBranch (_, _) -> raise Unimplemented
+ | ExpandNoBranch (sexp, e) -> (
+ match sexp with
+ | V.SeConcrete _ ->
+ (* Actually, we don't *register* symbolic expansions to constant
+ * values in the symbolic ADT *)
+ failwith "Unreachable"
+ | SeMutRef (_, sv) | SeSharedRef (_, sv) ->
+ (* The (mut/shared) borrow type is extracted to identity: we thus simply
+ * introduce an reassignment *)
+ let ctx, var = fresh_var_for_symbolic_value sv ctx in
+ let e = translate_expression e ctx in
+ Let (Assignment (var, scrutinee), e)
+ | SeAdt _ ->
+ (* Should be in the [ExpandAdt] case *)
+ failwith "Unreachable")
| ExpandAdt branches -> (
(* We don't do the same thing if there is a branching or not *)
match branches with