From 2f643e4419e8237c63d6823720da8100da9c8b11 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Apr 2014 09:18:51 +0000 Subject: Clean-up pass on C types: - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index b9f684e..344a00f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -21,6 +21,7 @@ Require Inlining. Require ValueDomain. Require Tailcall. Require Allocation. +Require Ctypes. Require Compiler. (* Standard lib *) @@ -125,6 +126,7 @@ 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 Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr Conventions1.dummy_int_reg Conventions1.dummy_float_reg -- cgit v1.2.3