diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-12 18:51:54 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-12 18:51:54 +0100 |
| commit | 45b0cf75d14fdc2a053e3f966441d2103a40c41b (patch) | |
| tree | e87702b0458a23843ca87868b4a3a72919864629 /extraction/extraction.v | |
| parent | 8f337598016aa49ff6554085b406b7e6026bfc3d (diff) | |
| parent | 50f25f57749d3eb46d859350719c9324fb75afa2 (diff) | |
| download | compcert-kvx-45b0cf75d14fdc2a053e3f966441d2103a40c41b.tar.gz compcert-kvx-45b0cf75d14fdc2a053e3f966441d2103a40c41b.zip | |
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index f58991aa..a7fe8f9f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -113,6 +113,8 @@ Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => "fun _ -> !Clflags.option_fpostpass". +Extract Constant Compopts.optim_pp_optimizer => + "fun _ -> !Clflags.option_pp_optimizer". Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". Extract Constant Compopts.debug => @@ -191,4 +193,4 @@ Separate Extraction Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol Parser.translation_unit_file - Compopts.optim_postpass. + Compopts.optim_postpass Compopts.optim_pp_optimizer. |