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 /exportclight | |
| 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 'exportclight')
| -rw-r--r-- | exportclight/Clightgen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 4209975a..f7279a5e 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -45,7 +45,7 @@ let compile_c_ast sourcename csyntax ofile = | Errors.Error msg -> fatal_error loc "%a" print_error msg in (* Dump Clight in C syntax if requested *) - PrintClight.print_if clight; + PrintClight.print_if_2 clight; (* Print Clight in Coq syntax *) let oc = open_out ofile in ExportClight.print_program (Format.formatter_of_out_channel oc) |