diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
| commit | b686f8df572ea77c8832637bed4e4cd81f0931e2 (patch) | |
| tree | 49d7921708c2dbb874dd7b53d0d74d9416735cb2 /extraction | |
| parent | 2a26429f28bea6356521135c632ddb9a8b11c018 (diff) | |
| download | compcert-kvx-b686f8df572ea77c8832637bed4e4cd81f0931e2.tar.gz compcert-kvx-b686f8df572ea77c8832637bed4e4cd81f0931e2.zip | |
Ctyping: better typing of conditional expressions.
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index f7e99545..ecd2853a 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -156,11 +156,11 @@ 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.build_composite_env - Csyntax.make_program Clight.make_program Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr - Ctyping.retype_function Ctyping.econdition' + Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Clight.make_program Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin |