From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy 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/Events.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index 329f31c2..a5c82d09 100644 --- a/common/Events.v +++ b/common/Events.v @@ -400,7 +400,7 @@ End EVENTVAL_INV. (** Each external function is of one of the following kinds: *) Inductive extfun_kind: signature -> Type := - | EF_syscall (sg: signature) (name: ident): extfun_kind sg + | EF_syscall (name: ident) (sg: signature): extfun_kind sg (** A system call. Takes integer-or-float arguments, produces a result that is an integer or a float, does not modify the memory, and produces an [Event_syscall] event in the trace. *) @@ -985,7 +985,7 @@ This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := match classify_external_function ef with - | EF_syscall sg name => extcall_io_sem name sg + | EF_syscall name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem @@ -994,7 +994,7 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef.(ef_sig)). + extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call. destruct (classify_external_function ef). apply extcall_io_ok. -- cgit