Loop_Entry attribute is used to refer to the value that an
expression had upon entry to a given loop in much the same way that the
Old attribute in a subprogram postcondition can be used to refer
to the value an expression had upon entry to the subprogram. The
relevant loop is either identified by the given loop name, or it is the
innermost enclosing loop when no loop name is given.
Loop_Entry attribute can only occur within an
In addition, such a pragma must be one of the items in the sequence
of statements of a loop body, or nested inside block statements that
appear in the sequence of statements of a loop body.
A common use of
Loop_Entry is to compare the current value of objects with
their initial value at loop entry, in a
The effect of using
X'Loop_Entry is the same as declaring
a constant initialized with the initial value of
X at loop
entry. This copy is not performed if the loop is not entered, or if the
corresponding pragmas are ignored or disabled.