From c4877832826fa26aea9c236f16bdc2de16c98150 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 15 Jan 2012 08:57:09 +0000 Subject: Added volatile_read_global and volatile_store_global builtins. Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 4f113c7..becf4e4 100644 --- a/common/AST.v +++ b/common/AST.v @@ -418,6 +418,12 @@ Inductive external_function : Type := (** A volatile store operation. If the adress given as first argument points within a volatile global variable, generate an event. Otherwise, produce no event and behave like a regular memory store. *) + | EF_vload_global (chunk: memory_chunk) (id: ident) (ofs: int) + (** A volatile load operation from a global variable. + Specialized version of [EF_vload]. *) + | EF_vstore_global (chunk: memory_chunk) (id: ident) (ofs: int) + (** A volatile store operation in a global variable. + Specialized version of [EF_vstore]. *) | EF_malloc (** Dynamic memory allocation. Takes the requested size in bytes as argument; returns a pointer to a fresh block of the given size. @@ -446,6 +452,8 @@ Definition ef_sig (ef: external_function): signature := | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None + | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None | EF_malloc => mksignature (Tint :: nil) (Some Tint) | EF_free => mksignature (Tint :: nil) None | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None @@ -461,6 +469,8 @@ Definition ef_inline (ef: external_function) : bool := | EF_builtin name sg => true | EF_vload chunk => true | EF_vstore chunk => true + | EF_vload_global chunk id ofs => true + | EF_vstore_global chunk id ofs => true | EF_malloc => false | EF_free => false | EF_memcpy sz al => true -- cgit v1.2.3