[Ada] Attribute Update

[Arnaud Charlet <charlet at adacore dot com>]

This patch provides the initial implementation of attribute Update. This
construct is intended for formal verification proofs.

The syntax of the attribute is as follows:

   X'Update ( RECORD_COMPONENT_ASSOCIATION_LIST )
   X'Update ( ARRAY_COMPONENT_ASSOCIATION {, ARRAY_COMPONENT_ASSOCIATION} )
   X'Update ( MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION
                {, MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION} )
   MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION ::=
     INDEX_EXPRESSION_LIST_LIST => EXPRESSION
   INDEX_EXPRESSION_LIST_LIST ::=
     INDEX_EXPRESSION_LIST { | INDEX_EXPRESSION_LIST}
   INDEX_EXPRESSION_LIST ::= (EXPRESSION {, EXPRESSION} )

The brief semantics of this attribute are as follows:

The prefix of attribute Update must be a non-limited object of a record or
array type. The type of the attribute is that of its prefix. The evaluation of
attribute Update begins with the creation of an anonymous object of type T
which is initialized to the value of the prefix. Next, components of the object
are updated to new values as specified by the corresponding association_list.
The attribute reference then denotes the constant view of this updated object.

A record update may not modify discriminants and it is not allowed to mention
components more than once. An array update modifies specified elements in the
same order of their appearance in the corresponding association_list. The use
of "others" in the association_lists is not allowed.

------------
-- Source --
------------

--  main.adb

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   type Rec is record
      Comp_1 : Natural;
      Comp_2 : Natural;
   end record;

   procedure Output_Rec (Obj : Rec) is
   begin
     Put_Line ("Comp_1:" & Obj.Comp_1'Img);
     Put_Line ("Comp_2:" & Obj.Comp_2'Img);
   end Output_Rec;

   Base_Obj : constant Rec := (1, 2);
   Obj      : constant Rec := Base_Obj'Update (Comp_2 => 3);

begin
   Output_Rec (Base_Obj);
   Output_Rec (Obj);
end Main;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnatd.V main.adb
$ ./main
Comp_1: 1
Comp_2: 2
Comp_1: 1
Comp_2: 3

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

2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference): Add processing
	for attribute Update.
	(Expand_Update_Attribute): New routine.
	* par-ch4.adb (P_Name): The sole expression of attribute Update
	is an aggregate, parse it accordingly.
	* sem_attr.adb (Analyze_Attribute): Verify the legality of
	attribute Update.
	(Eval_Attribute): Attribute Update does not
	need evaluation because it is never static.
	* snames.ads-tmpl: Add Name_Update to the list of special names
	recognized by the compiler. Add an Attribute_Id for Update.

Attachment: difs
Description: Text document