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, 18 insertions, 0 deletions

diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index e3a6f704..244a73f0 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -90,6 +90,7 @@ let type_unary_operation = function
   | Ocast8unsigned -> tint, tint
   | Ocast16unsigned -> tint, tint
   | Onegint -> tint, tint
+  | Oboolval -> tint, tint
   | Onotbool -> tint, tint
   | Onotint -> tint, tint
   | Onegf -> tfloat, tfloat
@@ -134,6 +135,7 @@ let name_of_unary_operation = function
   | Ocast8unsigned -> "cast8unsigned"
   | Ocast16unsigned -> "cast16unsigned"
   | Onegint -> "negint"
+  | Oboolval -> "notbool"
   | Onotbool -> "notbool"
   | Onotint -> "notint"
   | Onegf -> "negf"
@@ -293,6 +295,22 @@ let rec type_stmt env blk ret s =
       with Error s ->
         raise (Error (sprintf "In call:\n%s" s))
       end
+  | Sbuiltin(optid, ef, el) ->
+      let sg = ef_sig ef in
+      let tel = type_exprlist env [] el in
+      begin try
+        unify_list (ty_of_sig_args sg.sig_args) tel;
+        let ty_res =
+          match sg.sig_res with
+          | None -> tint (*???*)
+          | Some t -> ty_of_typ t in
+        begin match optid with
+        | None -> ()
+        | Some id -> unify (type_var env id) ty_res
+        end
+      with Error s ->
+        raise (Error (sprintf "In builtin call:\n%s" s))
+      end
   | Sseq(s1, s2) ->
       type_stmt env blk ret s1;
       type_stmt env blk ret s2