diff options
Diffstat (limited to 'common/Values.v')
-rw-r--r-- | common/Values.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 7fae3b72..54eac863 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) |