diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-01 15:49:23 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-01 15:49:23 +0100 |
| commit | 47c82de6010935d11c3d64f6d06c2061c34dc091 (patch) | |
| tree | 1922a9a57d4ff4cd7c135dded6cb9ddf33c1ce2a /cparser/Cprint.ml | |
| parent | be2192f295290c72d56e01263bc354f6844229ec (diff) | |
| download | compcert-kvx-47c82de6010935d11c3d64f6d06c2061c34dc091.tar.gz compcert-kvx-47c82de6010935d11c3d64f6d06c2061c34dc091.zip | |
Use C99 syntax to print attributes over array types
Before, we were doing C90, there was no official syntax for such attributes, and we used ours. With C99 we can use "ty [ attributes N ]" to print "array with attributes of N elements of type ty".
Diffstat (limited to 'cparser/Cprint.ml')
| -rw-r--r-- | cparser/Cprint.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 470c22e5..0a927873 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -142,13 +142,14 @@ let rec dcl ?(pp_indication=true) pp ty n = dcl pp t n' | TArray(t, sz, a) -> let n' pp = + n pp; begin match a with - | [] -> n pp - | _ -> fprintf pp " (%a%t)" attributes a n + | [] -> fprintf pp "[" + | _ -> fprintf pp "[%a " attributes a end; begin match sz with - | None -> fprintf pp "[]" - | Some i -> fprintf pp "[%Ld]" i + | None -> fprintf pp "]" + | Some i -> fprintf pp "%Ld]" i end in dcl pp t n' | TFun(tres, args, vararg, a) -> |