diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-19 20:03:49 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-19 20:03:49 +0200 |
| commit | 22d8683c16e863dc44ef45d66a4530d8c63d2c30 (patch) | |
| tree | 3a215856d1a93fc2b60ee56afce84927e149a1bd /extraction | |
| parent | d0163625ad55f8b01a3c002dd52be83b8a26e35e (diff) | |
| download | compcert-kvx-22d8683c16e863dc44ef45d66a4530d8c63d2c30.tar.gz compcert-kvx-22d8683c16e863dc44ef45d66a4530d8c63d2c30.zip | |
forgotten extraction
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index b102503b..18637336 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -224,4 +224,5 @@ Separate Extraction Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol Parser.translation_unit_file - Compopts.optim_postpass. + Compopts.optim_postpass + Archi.has_notrap_loads. |