Pragma Initializes (GNAT Reference Manual) (original) (raw)

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

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