diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-03 17:40:22 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-24 17:38:06 +0100 |
| commit | ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 (patch) | |
| tree | 34c130d8052a83b05f5db755997f7d60a94481e6 /common/AST.v | |
| parent | 1e29e518e62ad88e9c2e2b180beb07434a07cdd7 (diff) | |
| download | compcert-kvx-ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99.tar.gz compcert-kvx-ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99.zip | |
Add Genv.public_symbol operation.
Restrict pointer event values to public global names.
Update proofs accordingly. PowerPC and ARM need updating.
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/common/AST.v b/common/AST.v index 75286bd6..9c29a374 100644 --- a/common/AST.v +++ b/common/AST.v @@ -657,6 +657,15 @@ Proof. Defined. Global Opaque external_function_eq. +(** Global variables referenced by an external function *) + +Definition globals_external (ef: external_function) : list ident := + match ef with + | EF_vload_global _ id _ => id :: nil + | EF_vstore_global _ id _ => id :: nil + | _ => nil + end. + (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := |