diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-08-22 13:29:36 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-08-22 13:29:36 +0200 |
commit | d2595e3afb8c38a3391a66c3fc3f7a92fff9eff4 (patch) | |
tree | f3c8fba9ffffee5924dadd803fcebdc3520c9361 /exportclight/ExportClight.ml | |
parent | d97caa16d15b0faca8386a060ec2bfaedad3cdab (diff) | |
parent | 47fae389c800034e002c9f8a398e9adc79a14b81 (diff) | |
download | compcert-d2595e3afb8c38a3391a66c3fc3f7a92fff9eff4.tar.gz compcert-d2595e3afb8c38a3391a66c3fc3f7a92fff9eff4.zip |
Merge branch 'bitfields' (#400)
Diffstat (limited to 'exportclight/ExportClight.ml')
-rw-r--r-- | exportclight/ExportClight.ml | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 474a1bd8..ced07427 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -161,6 +161,22 @@ let attribute p a = a.attr_volatile (print_option coqN) a.attr_alignas +(* Raw int size and signedness *) + +let intsize p sz = + fprintf p "%s" + (match sz with + | I8 -> "I8" + | I16 -> "I16" + | I32 -> "I32" + | IBool -> "IBool") + +let signedness p sg = + fprintf p "%s" + (match sg with + | Signed -> "Signed" + | Unsigned -> "Unsigned") + (* Types *) let rec typ p t = @@ -444,11 +460,24 @@ let print_ident_globdef p = function (* Composite definitions *) +let print_member p = function + | Member_plain (id, ty) -> + fprintf p "@[<hov 2>Member_plain@ %a@ %a@]" + ident id typ ty + | Member_bitfield (id, sz, sg, a, width, pad) -> + fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]" + ident id + intsize sz + signedness sg + attribute a + coqZ width + pad + let print_composite_definition p (Composite(id, su, m, a)) = fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]" ident id (match su with Struct -> "Struct" | Union -> "Union") - (print_list (print_pair ident typ)) m + (print_list print_member) m attribute a (* The prologue *) |