Pragma Modifies (GNAT Reference Manual)

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

2.112 Pragma Modifies ¶

Syntax:

pragma Modifies (MODIFIES_SPECIFICATION);

MODIFIES_SPECIFICATION ::=
    MODIFIES_CLAUSE
  | (MODIFIES_CLAUSE {, MODIFIES_CLAUSE});

MODIFIES_CLAUSE ::= MODIFIED_OBJECTS { when GUARD }

GUARD ::= boolean_EXPRESSION

MODIFIED_OBJECTS ::= MODIFIED_OBJECT | (MODIFIED_OBJECT {, MODIFIED_OBJECT})

MODIFIED_OBJECT ::=
    name
  | MODIFIED_OBJECT . all
  | MODIFIED_OBJECT . component_selector_name
  | MODIFIED_OBJECT (expression {, expression})

The Modifies pragma is intended to be an exact replacement for the implementation-defined Modifies aspect, and shares its restrictions and semantics.

This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section TBD.