diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
| commit | d594c5da5e11fb10775c2b772961b8a2383887c7 (patch) | |
| tree | 750ed5d4a0829519a258f3c12f7d518e53504487 /extraction | |
| parent | 1e97bb4f6297b6fa7949684e522a592aab754d99 (diff) | |
| parent | 2dd864217cc864d44e828a4d14dd45668e4ab095 (diff) | |
| download | compcert-kvx-d594c5da5e11fb10775c2b772961b8a2383887c7.tar.gz compcert-kvx-d594c5da5e11fb10775c2b772961b8a2383887c7.zip | |
Merge branch 'named-structs'
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 8 |
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 |