From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 17:40:22 +0100 Subject: Add Genv.public_symbol operation. Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. --- common/AST.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'common/AST.v') 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 := -- cgit