From dffc9885e54f9c68af23ec79023dfe8516a4cc32 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 16 Sep 2021 14:54:22 +0200 Subject: 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. --- export/ExportCtypes.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'export/ExportCtypes.ml') 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 "@[(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 "@[(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 - -- cgit