Pragma Refined_Global (GNAT Reference Manual)

Next: Pragma Refined_Post, Previous: Pragma Refined_Depends, Up: Implementation Defined Pragmas [Contents][Index]

2.149 Pragma Refined_Global ¶

Syntax:

pragma Refined_Global (GLOBAL_SPECIFICATION);

GLOBAL_SPECIFICATION ::=
     null
  | (GLOBAL_LIST)
  | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST})

MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST

MODE_SELECTOR ::= In_Out | Input | Output | Proof_In
GLOBAL_LIST   ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
GLOBAL_ITEM   ::= NAME

For the semantics of this pragma, see the entry for aspect Refined_Global in the SPARK 2014 Reference Manual, section 6.1.4.