Ada Programming/Attributes/'Loop Entry
Description
[edit | edit source]X'Loop_Entry [(loop_name)]
The 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.
A Loop_Entry
attribute can only occur within an Assert
, Assert_And_Cut
, Assume
, Loop_Variant
or Loop_Invariant
pragma. 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 Loop_Invariant
pragma.
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.