summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-25 15:52:57 +0100
committerSon Ho2021-11-25 15:52:57 +0100
commita0fe240ca48038e6252bd5db1c33507b8f0e49a8 (patch)
tree9aab92de9cf0bf56f16844b8d8789ccf7a58362d
parent3ab2771f3c15283d02c51edd113bf8f9b3949b01 (diff)
Implement the Drop case of eval_statement
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 75e97e03..79ec5988 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1835,7 +1835,12 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
let ctx1, _ = prepare_rplace config Read p ctx in
Ok (ctx1, Unit)
| A.SetDiscriminant (p, variant_id) -> raise Unimplemented
- | A.Drop p -> raise Unimplemented
+ | A.Drop p ->
+ let ctx1, v = prepare_lplace config p ctx in
+ let nv = { v with value = V.Bottom } in
+ let env2 = write_place_unwrap config Write p nv ctx1.env in
+ let ctx2 = { ctx with env = env2 } in
+ Ok (ctx2, Unit)
| A.Assert assertion -> raise Unimplemented
| A.Call call -> raise Unimplemented
| A.Panic -> Error Panic