From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- extraction/extraction.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..0ba4abdd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,6 +23,8 @@ Require ValueDomain. Require Tailcall. Require Allocation. Require Ctypes. +Require Csyntax. +Require Clight. Require Compiler. Require Parser. Require Initializers. @@ -157,7 +159,8 @@ 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 Conventions1.dummy_int_reg Conventions1.dummy_float_reg -- cgit From 67b13ecb9cfd2511c1db62a6cc38cf796cfb2a14 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 31 Dec 2014 17:14:28 +0100 Subject: Add a type system for CompCert C and type-checking constructor functions. Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator. --- extraction/extraction.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 0ba4abdd..45239aa5 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -24,6 +24,7 @@ Require Tailcall. Require Allocation. Require Ctypes. Require Csyntax. +Require Ctyping. Require Clight. Require Compiler. Require Parser. @@ -163,6 +164,8 @@ Separate Extraction 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 -- cgit From 9f2ca1049957004161834090a697cd4118e2fb08 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 20 Jan 2015 14:54:48 +0100 Subject: Protect against redefinition of the __i64_xxx helper library functions. This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions. --- extraction/extraction.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) -- cgit