[Ada] Attribute Loop_Entry

[Arnaud Charlet <charlet at adacore dot com>]

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-limited object and the only attribute association
allowed must be a loop name. Attribute Loop_Entry can only appear inside pragma
Loop_Assertion.

For each prefix of a Loop_Entry attribute, a constant is implicitly declared at
the beginning of the associated loop statement. The constant's type is that of
the prefix. It is initialized to the result of evaluating the prefix as an
expression at the point of the constant declaration. The constant declaration
is not elaborated if the loop statement had a null iteration scheme.

The value of Prefix'Loop_Entry (Target_Loop_Name) is the value of the constant
and the type of Prefix'Loop_Entry (Target_Loop_Name) is that of the constant.

Example of usage:

procedure Main is
   Counter : Natural := 1;

begin
   Target : for Index in 1 .. 3 loop
      pragma Loop_Assertion
        (Invariant => Counter'Loop_Entry (Target) = Counter);

      Counter := Counter + 1;
   end loop Target;
end Main;

In the above example, the value of Counter at the point of entry into the loop
is 1. As a result, the Loop_Assertion should fail on the second iteration.

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-11-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb: Include Loop_Entry_Attributes to the list of
	Node/List/Elist10 usage.
	(Loop_Entry_Attributes): New routine.
	(Set_Loop_Entry_Attributes): New routine.
	(Write_Field10_Name): Add an output string for Loop_Entry_Attributes.
	* einfo.ads: Define new attribute Loop_Entry_Attributes along
	with its usage in nodes.
	(Loop_Entry_Attributes): New routine and dedicated pragma Inline.
	(Set_Loop_Entry_Attributes): New routine and dedicated pragma Inline.
	* exp_attr.adb (Expand_N_Attribute_Reference): Do not expand
	Attribute_Loop_Entry here.
	* exp_ch5.adb: Add with and use clause for Elists;
	(Expand_Loop_Entry_Attributes): New routine.
	(Expand_N_Loop_Statement): Add a call to Expand_Loop_Entry_Attributes.
	* exp_prag.adb (Expand_Pragma_Loop_Assertion): Specialize the
	search to include multiple nested loops produced by the expansion
	of Ada 2012 array iterator.
	* sem_attr.adb: Add with and use clause for Elists.
	(Analyze_Attribute): Check the legality of attribute Loop_Entry.
	(Resolve_Attribute): Nothing to do for Loop_Entry.
	(S14_Attribute): New routine.
	* snames.ads-tmpl: Add a comment on entries marked with
	HiLite. Add new name Name_Loop_Entry. Add new attribute
	Attribute_Loop_Entry.

Attachment: difs
Description: Text document