diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 16:15:54 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 16:15:54 +0200 |
| commit | aebbc43842ec0c49058b718c685e08edf11ce614 (patch) | |
| tree | 4a9418d0e86a88986dbca4f51ecd9a5cfd0c7355 /extraction | |
| parent | 87d2c34910a017c13a908cfe2cf2c627e56e6cfe (diff) | |
| download | compcert-kvx-aebbc43842ec0c49058b718c685e08edf11ce614.tar.gz compcert-kvx-aebbc43842ec0c49058b718c685e08edf11ce614.zip | |
route through LICMaux
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 1bb5a709..b102503b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -87,6 +87,9 @@ Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info". Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis". Extraction Inline Inlining.ret Inlining.bind. +(* Loop invariant code motion *) +Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections". + (* Allocation *) Extract Constant Allocation.regalloc => "Regalloc.regalloc". |