From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: Merge of the newmem and newextcalls branches: - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index b40b94c7..548c8df8 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -34,11 +34,6 @@ Open Local Scope error_monad_scope. (** * Operations on C types *) -Definition signature_of_function (f: Csyntax.function) : signature := - mksignature - (typlist_of_typelist (type_of_params (Csyntax.fn_params f))) - (opttyp_of_type (Csyntax.fn_return f)). - Definition chunk_of_type (ty: type): res memory_chunk := match access_mode ty with | By_value chunk => OK chunk @@ -615,7 +610,7 @@ Definition transl_function (f: Csyntax.function) : res function := do tparams <- transl_params (Csyntax.fn_params f); do tvars <- transl_vars (Csyntax.fn_vars f); do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f); - OK (mkfunction (signature_of_function f) tparams tvars tbody). + OK (mkfunction (opttyp_of_type (Csyntax.fn_return f)) tparams tvars tbody). Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with -- cgit