From 07619853cdee8079dcba2e01912cd0b905f21dce Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 13:29:38 +0100
Subject: Implement the symbolic case of set_discriminant

---
 src/Interpreter.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2fa1bea2..5db49935 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3540,7 +3540,14 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
       (ctx, Unit)
   | _, V.Symbolic _ ->
       assert (config.mode = SymbolicMode);
-      (* TODO *) raise Unimplemented
+      (* This is a bit annoying: in theory we should expand the symbolic value
+       * then set the discriminant, because in the case the discriminant is
+       * exactly the one we set, the fields are left untouched, and in the
+       * other cases they are set to Bottom.
+       * For now, we forbid setting the discriminant of a symbolic value:
+       * setting a discriminant should only be used to initialize a value,
+       * really. *)
+      failwith "Unexpected value"
   | _, (V.Adt _ | V.Bottom) -> failwith "Inconsistent state"
   | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> failwith "Unexpected value"
 
-- 
cgit v1.2.3