aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/extraction.v
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/extraction.v')
-rw-r--r--extraction/extraction.v8
1 files changed, 7 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 94ac6f52..1db52ef3 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -23,6 +23,9 @@ Require ValueDomain.
Require Tailcall.
Require Allocation.
Require Ctypes.
+Require Csyntax.
+Require Ctyping.
+Require Clight.
Require Compiler.
Require Parser.
Require Initializers.
@@ -151,9 +154,12 @@ Cd "extraction".
Separate Extraction
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.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
+ Csyntax.make_program Clight.make_program
Initializers.transl_init Initializers.constval
Csyntax.Eindex Csyntax.Epreincr
+ Ctyping.retype_function Ctyping.econdition'
+ Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr
Conventions1.dummy_int_reg Conventions1.dummy_float_reg
RTL.instr_defs RTL.instr_uses
Machregs.mregs_for_operation Machregs.mregs_for_builtin