diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
| commit | 9c7c84cc40eaacc1e2c13091165785cddecba5ad (patch) | |
| tree | 65eafe51ad284d88fd5a949e1b2a54cd272f9f91 /common/Events.v | |
| parent | f4b416882955d9d91bca60f3eb35b95f4124a5be (diff) | |
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
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Events.v b/common/Events.v index 329f31c..a5c82d0 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. |