aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintClight.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-26 10:41:07 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-26 10:41:07 +0000
commit2570ddd61b1c98b62c8d97fce862654535696844 (patch)
treee9a652b115045a3b2c4ade69ec3cc3fdad429b54 /cfrontend/PrintClight.ml
parent65cc3738e7436e46f70c0508638a71fbb49c50a8 (diff)
downloadcompcert-kvx-2570ddd61b1c98b62c8d97fce862654535696844.tar.gz
compcert-kvx-2570ddd61b1c98b62c8d97fce862654535696844.zip
- Support for _Alignof(ty) operator from ISO C 2011
and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/PrintClight.ml')
-rw-r--r--cfrontend/PrintClight.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 77f22f74..1bd21daa 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -54,7 +54,6 @@ let rec precedence = function
| Efield _ -> (16, LtoR)
| Econst_int _ -> (16, NA)
| Econst_float _ -> (16, NA)
- | Esizeof _ -> (15, RtoL)
| Eunop _ -> (15, RtoL)
| Eaddrof _ -> (15, RtoL)
| Ecast _ -> (14, RtoL)
@@ -92,8 +91,6 @@ let rec expr p (prec, e) =
fprintf p "%ld" (camlint_of_coqint n)
| Econst_float(f, _) ->
fprintf p "%F" f
- | Esizeof(ty, _) ->
- fprintf p "sizeof(%s)" (name_type ty)
| Eunop(op, a1, _) ->
fprintf p "%s%a" (name_unop op) expr (prec', a1)
| Eaddrof(a1, _) ->
@@ -268,7 +265,6 @@ let rec collect_expr = function
| Ecast(r, _) -> collect_expr r
| Econdition(r1, r2, r3, _) ->
collect_expr r1; collect_expr r2; collect_expr r3
- | Esizeof _ -> ()
let rec collect_exprlist = function
| [] -> ()