diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-14 19:37:28 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-09-16 09:47:14 +0200 |
| commit | 3d25d06ec58f0527b6f0eee7e0df19c18f7133ed (patch) | |
| tree | bd52761506b8caf5c8908f51c546b7191dfd4edb /cfrontend/PrintCsyntax.ml | |
| parent | a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d (diff) | |
| download | compcert-kvx-3d25d06ec58f0527b6f0eee7e0df19c18f7133ed.tar.gz compcert-kvx-3d25d06ec58f0527b6f0eee7e0df19c18f7133ed.zip | |
clightgen -dclight: print function parameters correctly
The Clight output of clightgen is Clight version 2, after SimplLocals
conversion, where function parameters are temporary variables, not
variables.
This commit makes sure the function parameters are printed as
temporary variables and not as variables. In passing, it
generalizes the Clight pretty-printer so that it can print
both Clight version 1 and Clight version 2.
Closes: #314
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 3a44796c..1c9729c5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -391,7 +391,7 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let name_function_parameters fun_name params cconv = +let name_function_parameters name_param fun_name params cconv = let b = Buffer.create 20 in Buffer.add_string b fun_name; Buffer.add_char b '('; @@ -404,7 +404,7 @@ let name_function_parameters fun_name params cconv = if cconv.cc_vararg then Buffer.add_string b ",..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl (extern_atom id) ty); + Buffer.add_string b (name_cdecl (name_param id) ty); add_params false rem in add_params true params end; @@ -413,8 +413,8 @@ let name_function_parameters fun_name params cconv = let print_function p id f = fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params f.fn_callconv) + (name_cdecl (name_function_parameters extern_atom + (extern_atom id) f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[<v 2>{@ "; List.iter |