Implement the symbolic case of set_discriminant

1 files changed, 8 insertions, 1 deletions

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"