This patch delays the generation of index checks for the following cases of
Loop_Entry attribute references:
Prefix'Loop_Entry (Expr)
Prefix'Loop_Entry (Expr1, Expr2, ... ExprN)
Even though these constructs appear initially as attribute references, analysis
converts them into indexed compon
This patch provides the initial implementation of attribute Loop_Entry. This
attribute is indended for formal verification proofs.
The syntax of the attribute is as follows:
Prefix'Loop_Entry (Target_Loop_Name)
The brief semantic rules for this attribute are:
The prefix must denote a non-lim
