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


2.84 Pragma Initializes

Syntax:

    pragma Initializes (INITIALIZATION_LIST);
    
    INITIALIZATION_LIST ::=
         null
      | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})
    
    INITIALIZATION_ITEM ::= name [=> INPUT_LIST]
    
    INPUT_LIST ::=
         null
      |  INPUT
      | (INPUT {, INPUT})
    
    INPUT ::= name

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