aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-11-26 17:35:31 +0100
committerCyril SIX <cyril.six@kalray.eu>2018-11-26 17:35:31 +0100
commit5631ccb7c416bb7ecbe7920cb432a78436c0a7ac (patch)
treec84dfc9edea4d1aaf48985a229dddb811cbc3ffa /extraction
parent3d38bf85c8ac3a83fe7aaeb5e01bb9a8403e6a60 (diff)
downloadcompcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.tar.gz
compcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.zip
BROKEN - works for x86, not for k1 anymore
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 6ab2ce3a..a47a7237 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -167,7 +167,6 @@ Set Extraction AccessOpaque.
Cd "extraction".
Separate Extraction
- Asm.dummy_function Asmgen.addptrofs Asmgen.storeind_ptr
Compiler.transf_c_program Compiler.transf_cminor_program
Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env