From 95a967ad7a49b788604c2ba1c029264921498fe6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 25 Nov 2021 15:55:30 +0100
Subject: Implement the assertion case of eval_statement

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

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 79ec5988..2acabd4f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1841,7 +1841,13 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
       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.Assert assertion -> (
+      let ctx1, v = eval_operand config ctx assertion.cond in
+      assert (v.ty = T.Bool);
+      match v.value with
+      | Concrete (Bool b) ->
+          if b = assertion.expected then Ok (ctx1, Unit) else Error Panic
+      | _ -> failwith "Expected a boolean")
   | A.Call call -> raise Unimplemented
   | A.Panic -> Error Panic
   | A.Return -> Ok (ctx, Return)
-- 
cgit v1.2.3