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