diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-11 16:00:04 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-30 14:18:48 +0200 |
| commit | d97caa16d15b0faca8386a060ec2bfaedad3cdab (patch) | |
| tree | c99f939a1ec8429a9024b761ccb8c22cc6ae0b95 /cparser | |
| parent | a0ad5ff6f9c7603610a7448935b36c9ed22c6435 (diff) | |
| download | compcert-kvx-d97caa16d15b0faca8386a060ec2bfaedad3cdab.tar.gz compcert-kvx-d97caa16d15b0faca8386a060ec2bfaedad3cdab.zip | |
Revise the declaration of __compcert_* helper functions
Don't put them in the C environment used for elaboration.
Instead, add them directly to the generated CompCert C at the end of
the C2C translation.
Diffstat (limited to 'cparser')
0 files changed, 0 insertions, 0 deletions