1 files changed, 7 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v
index 7fae3b7..54eac86 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -160,6 +160,13 @@ Definition notint (v: val) : val :=
 
 Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
 
+Definition boolval (v: val) : val :=
+  match v with
+  | Vint n => of_bool (negb (Int.eq n Int.zero))
+  | Vptr b ofs => Vtrue
+  | _ => Vundef
+  end.
+
 Definition notbool (v: val) : val :=
   match v with
   | Vint n => of_bool (Int.eq n Int.zero)