diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-16 14:54:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-22 16:06:39 +0200 |
| commit | dffc9885e54f9c68af23ec79023dfe8516a4cc32 (patch) | |
| tree | f7a3755303b6a14b039d90f335d4b860da93ac1e /export/ExportCtypes.ml | |
| parent | d32955030937937706b71a96dc6584800f0b8722 (diff) | |
| download | compcert-kvx-dffc9885e54f9c68af23ec79023dfe8516a4cc32.tar.gz compcert-kvx-dffc9885e54f9c68af23ec79023dfe8516a4cc32.zip | |
Add support to clightgen for generating Csyntax AST as .v files
As proposed in #404.
This is presented as a new option `-clight` to the existing `clightgen` tool.
Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
Diffstat (limited to 'export/ExportCtypes.ml')
| -rw-r--r-- | export/ExportCtypes.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/export/ExportCtypes.ml b/export/ExportCtypes.ml index 428a1459..d0a7f28a 100644 --- a/export/ExportCtypes.ml +++ b/export/ExportCtypes.ml @@ -98,6 +98,16 @@ and typlist p = function | Tcons(t, tl) -> fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl +(* Access modes for members of structs or unions *) + +let bitfield p = function + | Full -> + fprintf p "Full" + | Bits(sz, sg, pos, width) -> + fprintf p "@[<hov 2>(Bits@ %a@ %a@ %a@ %a)@]" + intsize sz signedness sg + coqZ pos coqZ width + (* Composite definitions *) let print_member p = function @@ -119,4 +129,3 @@ let print_composite_definition p (Composite(id, su, m, a)) = (match su with Struct -> "Struct" | Union -> "Union") (print_list print_member) m attribute a - |