[Ada] Add declaration for Itypes in Alfa mode

[Arnaud Charlet]

The formal verification back-end expects declaration to be present for Itypes,
even if they are not attached to the tree. Add such declarations in the case
of Itypes introduced for index/component types of arrays and anonymous array
types in object declaration.

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

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes
	created in Alfa mode, instead of inserting artificial declarations of
	non-Itypes in the tree.
	* sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to
	know if an Itype has a corresponding declaration, as defined in
	itypes.ads.

-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 178239)
+++ sem_ch3.adb	(working copy)
@@ -4741,26 +4741,20 @@
 
          Make_Index (Index, P, Related_Id, Nb_Index);
 
-         --  In formal verification mode, create an explicit subtype for every
-         --  index if not already a subtype_mark, and replace the existing type
-         --  of index by this new type. Having a declaration for all type
+         --  In formal verification mode, create an explicit declaration for
+         --  Itypes created for index types. Having a declaration for all type
          --  entities facilitates the task of the formal verification back-end.
+         --  Notice that this declaration is not attached to the tree.
 
          if ALFA_Mode
-           and then not Nkind_In (Index, N_Identifier, N_Expanded_Name)
+           and then Is_Itype (Etype (Index))
          then
             declare
                Loc     : constant Source_Ptr := Sloc (Def);
-               New_E   : Entity_Id;
+               Sub_Ind : Node_Id;
                Decl    : Entity_Id;
-               Sub_Ind : Node_Id;
 
             begin
-               New_E :=
-                 New_External_Entity
-                   (E_Void, Current_Scope, Sloc (P), Related_Id, 'D',
-                    Nb_Index, 'T');
-
                if Nkind (Index) = N_Subtype_Indication then
                   Sub_Ind := Relocate_Node (Index);
                else
@@ -4775,11 +4769,10 @@
 
                Decl :=
                  Make_Subtype_Declaration (Loc,
-                   Defining_Identifier => New_E,
+                   Defining_Identifier => Etype (Index),
                    Subtype_Indication  => Sub_Ind);
 
-               Insert_Action (Parent (Def), Decl);
-               Set_Etype (Index, New_E);
+               Analyze (Decl);
             end;
          end if;
 
@@ -4799,34 +4792,29 @@
 
       if Present (Component_Typ) then
 
-         --  In formal verification mode, create an explicit subtype for the
-         --  component type if not already a subtype_mark. Having a declaration
-         --  for all type entities facilitates the task of the formal
-         --  verification back-end.
+         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
 
+         --  In formal verification mode, create an explicit declaration for
+         --  the Itype created for a component type. Having a declaration for
+         --  all type entities facilitates the task of the formal verification
+         --  back-end. Notice that this declaration is not attached to the
+         --  tree.
+
          if ALFA_Mode
-           and then Nkind (Component_Typ) = N_Subtype_Indication
+           and then Is_Itype (Element_Type)
          then
             declare
                Loc  : constant Source_Ptr := Sloc (Def);
                Decl : Entity_Id;
 
             begin
-               Element_Type :=
-                 New_External_Entity
-                   (E_Void, Current_Scope, Sloc (P), Related_Id, 'C', 0, 'T');
-
                Decl :=
                  Make_Subtype_Declaration (Loc,
                    Defining_Identifier => Element_Type,
                    Subtype_Indication  => Relocate_Node (Component_Typ));
 
-               Insert_Action (Parent (Def), Decl);
+               Analyze (Decl);
             end;
-
-         else
-            Element_Type :=
-              Process_Subtype (Component_Typ, P, Related_Id, 'C');
          end if;
 
          Set_Etype (Component_Typ, Element_Type);
@@ -4915,6 +4903,30 @@
                                (Implicit_Base, Finalize_Storage_Only
                                                         (Element_Type));
 
+         --  In ALFA mode, generate a declaration for Itype T, so that the
+         --  formal verification back-end can use it.
+
+         if ALFA_Mode
+           and then Is_Itype (T)
+         then
+            declare
+               Loc  : constant Source_Ptr := Sloc (Def);
+               Decl : Node_Id;
+
+            begin
+               Decl := Make_Full_Type_Declaration (Loc,
+                  Defining_Identifier => T,
+                  Type_Definition     =>
+                   Make_Constrained_Array_Definition (Loc,
+                     Discrete_Subtype_Definitions =>
+                       New_Copy_List (Discrete_Subtype_Definitions (Def)),
+                     Component_Definition         =>
+                       Relocate_Node (Component_Definition (Def))));
+
+               Analyze (Decl);
+            end;
+         end if;
+
       --  Unconstrained array case
 
       else
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 178239)
+++ sem_util.adb	(working copy)
@@ -8507,6 +8507,20 @@
       end if;
    end Is_Volatile_Object;
 
+   ---------------------------
+   -- Itype_Has_Declaration --
+   ---------------------------
+
+   function Itype_Has_Declaration (Id : Entity_Id) return Boolean is
+   begin
+      pragma Assert (Is_Itype (Id));
+      return Present (Parent (Id))
+        and then Nkind_In (Parent (Id),
+                           N_Full_Type_Declaration,
+                           N_Subtype_Declaration)
+        and then Defining_Entity (Parent (Id)) = Id;
+   end Itype_Has_Declaration;
+
    -------------------------
    -- Kill_Current_Values --
    -------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 178235)
+++ sem_util.ads	(working copy)
@@ -969,6 +969,11 @@
    --  for something actually declared as volatile, not for an object that gets
    --  treated as volatile (see Einfo.Treat_As_Volatile).
 
+   function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
+   --  Applies to Itypes. True if the Itype is attached to a declaration for
+   --  the type through its Parent field, which may or not be present in the
+   --  tree.
+
    procedure Kill_Current_Values (Last_Assignment_Only : Boolean := False);
    --  This procedure is called to clear all constant indications from all
    --  entities in the current scope and in any parent scopes if the current