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/PrintCminor.ml | |
| parent | 145b32ec504541e98f73b2c87ff2d8181b5e7968 (diff) | |
| download | compcert-kvx-25b9b003178002360d666919f2e49e7f5f4a36e2.tar.gz compcert-kvx-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 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 30884b18..110e735e 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -21,6 +21,7 @@ open Datatypes open BinPos open Integers open AST +open PrintAST open Cminor (* Precedences and associativity -- like those of C *) @@ -57,6 +58,7 @@ let name_of_unop = function | Ocast16unsigned -> "int16u" | Ocast16signed -> "int16s" | Onegint -> "-" + | Oboolval -> "(_Bool)" | Onotbool -> "!" | Onotint -> "~" | Onegf -> "-f" @@ -193,6 +195,15 @@ let rec print_stmt p s = print_expr e1 print_expr_list (true, el) print_sig sg + | Sbuiltin(None, ef, el) -> + fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@])@;@]" + (name_of_external ef) + print_expr_list (true, el) + | Sbuiltin(Some id, ef, el) -> + fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]@]" + (ident_name id) + (name_of_external ef) + print_expr_list (true, el) | Sseq(Sskip, s2) -> print_stmt p s2 | Sseq(s1, Sskip) -> |