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/Cshmgen.v | |
| parent | a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d (diff) | |
| download | compcert-3d25d06ec58f0527b6f0eee7e0df19c18f7133ed.tar.gz compcert-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/Cshmgen.v')
0 files changed, 0 insertions, 0 deletions