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 /test/compression | |
parent | a0ad5ff6f9c7603610a7448935b36c9ed22c6435 (diff) | |
download | compcert-d97caa16d15b0faca8386a060ec2bfaedad3cdab.tar.gz compcert-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 'test/compression')
0 files changed, 0 insertions, 0 deletions