From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 Jun 2010 08:27:14 +0000
Subject: Support for inlined built-ins. AST: add ef_inline flag to external
 functions. Selection: recognize calls to inlined built-ins and inline them as
 Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm:
 adapted expansion of builtins. C2Clight: adapted detection of builtins.
 Conventions: refactored in a machine-independent part (backend/Conventions)  
 and a machine-dependent part (ARCH/SYS/Conventions1).

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/AST.v | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'common/AST.v')

diff --git a/common/AST.v b/common/AST.v
index 861795cc..bca0535b 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -82,6 +82,19 @@ Inductive memory_chunk : Type :=
   | Mfloat32 : memory_chunk        (**r 32-bit single-precision float *)
   | Mfloat64 : memory_chunk.       (**r 64-bit double-precision float *)
 
+(** The type (integer/pointer or float) of a chunk. *)
+
+Definition type_of_chunk (c: memory_chunk) : typ :=
+  match c with
+  | Mint8signed => Tint
+  | Mint8unsigned => Tint
+  | Mint16signed => Tint
+  | Mint16unsigned => Tint
+  | Mint32 => Tint
+  | Mfloat32 => Tfloat
+  | Mfloat64 => Tfloat
+  end.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
@@ -390,9 +403,12 @@ Qed.
 
 Record external_function : Type := mkextfun {
   ef_id: ident;
-  ef_sig: signature
+  ef_sig: signature;
+  ef_inline: bool
 }.
 
+(** Function definitions are the union of internal and external functions. *)
+
 Inductive fundef (F: Type): Type :=
   | Internal: F -> fundef F
   | External: external_function -> fundef F.
-- 
cgit