aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2020-11-25 17:23:12 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2020-11-25 17:23:12 +0100
commit713d5663a6c7b75eee9a9ae57cfecf8332e72be4 (patch)
treef8edb58f1f9c92482b548dd320fab32324e7563e /extraction
parentfbe134640de11d69cef417e2e59e2e2669ccc7ad (diff)
downloadcompcert-kvx-713d5663a6c7b75eee9a9ae57cfecf8332e72be4.tar.gz
compcert-kvx-713d5663a6c7b75eee9a9ae57cfecf8332e72be4.zip
Removing OrigAsmgen by moving the necessary functions in Asmgen.v
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f5b8291b..ffcebaaa 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -247,4 +247,6 @@ Separate Extraction
Globalenvs.Senv.invert_symbol
Parser.translation_unit_file
Compopts.optim_postpass
- Archi.has_notrap_loads.
+ Archi.has_notrap_loads
+ Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64
+ Asmgen.Asmgen_expand.storeptr.