summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-25 12:23:26 +0100
committerSon Ho2022-01-25 12:23:26 +0100
commit73ef593adbefaddbb32ceac16c3ae05b277920af (patch)
tree786c404aeda2a13d0b6d6b113d86dea4b4995f40 /src
parent5095a482e9a208db239b909fae1e9c7fea4f5117 (diff)
Finish implementing SymbolicToPure.translate_expansion
Diffstat (limited to 'src')
-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