Pragma Initializes (GNAT Reference Manual)

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

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