From a9995fe949d31e0f53b1e3e26908de8f98972ca5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 25 Nov 2021 16:41:21 +0100
Subject: Finish the implementation of set_discriminant

---
 src/Interpreter.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d1b264f1..74cbe70d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1870,17 +1870,24 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
           else
             (* Replace the value *)
             let bottom_v =
-              compute_expanded_bottom_adt_value ctx.type_context def_id
+              compute_expanded_bottom_adt_value ctx2.type_context def_id
                 (Some variant_id) regions types
             in
             let env3 = write_place_unwrap config access p bottom_v ctx2.env in
             let ctx3 = { ctx2 with env = env3 } in
             Ok (ctx3, Unit))
-  | _, V.Bottom -> raise Unimplemented
+  | T.Adt (def_id, regions, types), V.Bottom ->
+      let bottom_v =
+        compute_expanded_bottom_adt_value ctx2.type_context def_id
+          (Some variant_id) regions types
+      in
+      let env3 = write_place_unwrap config access p bottom_v ctx2.env in
+      let ctx3 = { ctx2 with env = env3 } in
+      Ok (ctx3, Unit)
   | _, V.Symbolic _ ->
       assert (config.mode = SymbolicMode);
       (* TODO *) raise Unimplemented
-  | _, V.Adt _ -> failwith "Inconsistent state"
+  | _, (V.Adt _ | V.Bottom) -> failwith "Inconsistent state"
   | _, (V.Concrete _ | V.Tuple _ | V.Borrow _ | V.Loan _ | V.Assumed _) ->
       failwith "Unexpected value"
 
-- 
cgit v1.2.3