Next: , Previous: Pragma Ghost, Up: Implementation Defined Pragmas


2.70 Pragma Global

Syntax:

    pragma 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 Global in the SPARK 2014 Reference Manual, section 6.1.4.