diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-08 15:33:47 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-08 15:33:47 +0200 |
| commit | f0a5038b4e4220300637d3e9e918d9ec31623108 (patch) | |
| tree | 2d1e5f006d7a9bcd4c2a1ddcf5803be97b105db9 /extraction | |
| parent | ed1f32134283d3cd4f939a26dfd99992ec48da86 (diff) | |
| download | compcert-kvx-f0a5038b4e4220300637d3e9e918d9ec31623108.tar.gz compcert-kvx-f0a5038b4e4220300637d3e9e918d9ec31623108.zip | |
Added versions of the tranform_* functions in AST to work with functions
taking the ident as argument.
This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 6327f871..dc7522b8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -168,4 +168,5 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg AST.signature_main + AST.transform_partial_ident_program Parser.translation_unit_file. |