diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 08:57:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 08:57:09 +0000 |
| commit | c4877832826fa26aea9c236f16bdc2de16c98150 (patch) | |
| tree | d25f713d4c6f4cf6126ad0451b80b32138eac84a /common/AST.v | |
| parent | a82c9c0e4a0b8e37c9c3ea5ae99714982563606f (diff) | |
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
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 10 |
1 files changed, 10 insertions, 0 deletions
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 |