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

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)