From b686f8df572ea77c8832637bed4e4cd81f0931e2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 May 2015 15:20:54 +0200 Subject: 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. --- extraction/extraction.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'extraction') 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 -- cgit