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 :=