diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-04 19:14:14 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-04 19:14:14 +0000 |
commit | 25b9b003178002360d666919f2e49e7f5f4a36e2 (patch) | |
tree | d5f7fb317f34f3a7ac9383c21b0eb143317c30f8 /common/Values.v | |
parent | 145b32ec504541e98f73b2c87ff2d8181b5e7968 (diff) | |
download | compcert-25b9b003178002360d666919f2e49e7f5f4a36e2.tar.gz compcert-25b9b003178002360d666919f2e49e7f5f4a36e2.zip |
Merge of the "volatile" branch:
- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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) |