diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-21 09:49:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-21 09:49:42 +0000 |
| commit | 1f16929dbe62bb60ea391705c48d893fa6c997d9 (patch) | |
| tree | b960942b883bb639e8a2a47561b3798ad1e0edfb /cfrontend | |
| parent | 58cf861123b8070d33d6b99d0907d99820646a16 (diff) | |
Beautify the output.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index a233c1f..9441d71 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -85,6 +85,10 @@ let attributes a = | Some l -> sprintf " _Alignas(%Ld)%s" (Int64.shift_left 1L (N.to_int l)) s1 +let attributes_space a = + let s = attributes a in + if String.length s = 0 then s else s ^ " " + let name_optid id = if id = "" then "" else " " ^ id @@ -101,8 +105,8 @@ let rec name_cdecl id ty = | Tpointer(t, a) -> let id' = match t with - | Tfunction _ | Tarray _ -> sprintf "(*%s%s)" (attributes a) id - | _ -> sprintf "*%s%s" (attributes a) id in + | Tfunction _ | Tarray _ -> sprintf "(*%s%s)" (attributes_space a) id + | _ -> sprintf "*%s%s" (attributes_space a) id in name_cdecl id' t | Tarray(t, n, a) -> name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t @@ -425,7 +429,7 @@ let print_init p = function | Init_int8 n -> fprintf p "%ld" (camlint_of_coqint n) | Init_int16 n -> fprintf p "%ld" (camlint_of_coqint n) | Init_int32 n -> fprintf p "%ld" (camlint_of_coqint n) - | Init_int64 n -> fprintf p "%Ld" (camlint64_of_coqint n) + | Init_int64 n -> fprintf p "%LdLL" (camlint64_of_coqint n) | Init_float32 n -> fprintf p "%F" (camlfloat_of_coqfloat n) | Init_float64 n -> fprintf p "%F" (camlfloat_of_coqfloat n) | Init_space n -> fprintf p "/* skip %ld */@ " (camlint_of_coqint n) |