From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Feb 2012 19:14:14 +0000
Subject: 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
---
 backend/CMtypecheck.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'backend/CMtypecheck.ml')

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
-- 
cgit