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

2.90 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.