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