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 /backend/CMtypecheck.ml | |
parent | 145b32ec504541e98f73b2c87ff2d8181b5e7968 (diff) |
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 'backend/CMtypecheck.ml')
-rw-r--r-- | backend/CMtypecheck.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index e3a6f70..244a73f 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 |