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

	* sem_ch3.adb (Analyze_Object_Declaration): issue an error in formal
	mode on initialization expression which does not respect SPARK
	restrictions.
	* sem_util.adb, sem_util.ads (Is_SPARK_Initialization_Expr): determines
	if the tree referenced by its argument represents an initialization
	expression in SPARK, suitable for initializing an object in an object
	declaration.

2011-08-02  Javier Miranda  <miranda@adacore.com>

	* exp_ch9.adb (Expand_Access_Protected_Subprogram_Type): Link the
	internally generated access to subprogram with its associated protected
	subprogram type.
	* einfo.ads, einfo.adb (Original_Access_Type): New attribute.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177139 138bc75d-0d04-0410-961f-82ee72b054a4

7 files changed, 176 insertions, 0 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 500a0a278d5..f478f3c2007 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch3.adb (Analyze_Object_Declaration): issue an error in formal
+	mode on initialization expression which does not respect SPARK
+	restrictions.
+	* sem_util.adb, sem_util.ads (Is_SPARK_Initialization_Expr): determines
+	if the tree referenced by its argument represents an initialization
+	expression in SPARK, suitable for initializing an object in an object
+	declaration.
+
+2011-08-02  Javier Miranda  <miranda@adacore.com>
+
+	* exp_ch9.adb (Expand_Access_Protected_Subprogram_Type): Link the
+	internally generated access to subprogram with its associated protected
+	subprogram type.
+	* einfo.ads, einfo.adb (Original_Access_Type): New attribute.
+
 2011-08-02  Geert Bosch  <bosch@adacore.com>
 
 	* cstand.adb (Register_Float_Type): Print information about type to
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index eb217d49d59..42217f5420f 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -181,6 +181,7 @@ package body Einfo is
    --    Default_Expr_Function           Node21
    --    Discriminant_Constraint         Elist21
    --    Interface_Name                  Node21
+   --    Original_Access_Type            Node21
    --    Original_Array_Type             Node21
    --    Small_Value                     Ureal21
 
@@ -2353,6 +2354,12 @@ package body Einfo is
       return Flag242 (Id);
    end Optimize_Alignment_Time;
 
+   function Original_Access_Type (Id : E) return E is
+   begin
+      pragma Assert (Ekind (Id) = E_Access_Subprogram_Type);
+      return Node21 (Id);
+   end Original_Access_Type;
+
    function Original_Array_Type (Id : E) return E is
    begin
       pragma Assert (Is_Array_Type (Id) or else Is_Modular_Integer_Type (Id));
@@ -4852,6 +4859,12 @@ package body Einfo is
       Set_Flag242 (Id, V);
    end Set_Optimize_Alignment_Time;
 
+   procedure Set_Original_Access_Type (Id : E; V : E) is
+   begin
+      pragma Assert (Ekind (Id) = E_Access_Subprogram_Type);
+      Set_Node21 (Id, V);
+   end Set_Original_Access_Type;
+
    procedure Set_Original_Array_Type (Id : E; V : E) is
    begin
       pragma Assert (Is_Array_Type (Id) or else Is_Modular_Integer_Type (Id));
@@ -8332,6 +8345,9 @@ package body Einfo is
          when Fixed_Point_Kind                             =>
             Write_Str ("Small_Value");
 
+         when E_Access_Subprogram_Type                     =>
+            Write_Str ("Original_Access_Type");
+
          when E_In_Parameter                               =>
             Write_Str ("Default_Expr_Function");
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index e69704d86ab..0366dbeb604 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3206,6 +3206,12 @@ package Einfo is
 --       Optimize_Alignment (Off) mode applies to the type/object, then neither
 --       of the flags Optimize_Alignment_Space/Optimize_Alignment_Time is set.
 
+--    Original_Access_Type (Node21)
+--       Present in E_Access_Subprogram_Type entities. Set only if the access
+--       type was generated by the expander as part of processing an access
+--       to protected subprogram type. Points to the access to protected
+--       subprogram type.
+
 --    Original_Array_Type (Node21)
 --       Present in modular types and array types and subtypes. Set only
 --       if the Is_Packed_Array_Type flag is set, indicating that the type
@@ -4876,6 +4882,7 @@ package Einfo is
    --  E_Access_Subprogram_Type
    --    Equivalent_Type                     (Node18)   (remote types only)
    --    Directly_Designated_Type            (Node20)
+   --    Original_Access_Type                (Node21)
    --    Needs_No_Actuals                    (Flag22)
    --    Can_Use_Internal_Rep                (Flag229)
    --    (plus type attributes)
@@ -6223,6 +6230,7 @@ package Einfo is
    function OK_To_Reorder_Components            (Id : E) return B;
    function Optimize_Alignment_Space            (Id : E) return B;
    function Optimize_Alignment_Time             (Id : E) return B;
+   function Original_Access_Type                (Id : E) return E;
    function Original_Array_Type                 (Id : E) return E;
    function Original_Record_Component           (Id : E) return E;
    function Overlays_Constant                   (Id : E) return B;
@@ -6812,6 +6820,7 @@ package Einfo is
    procedure Set_OK_To_Reorder_Components        (Id : E; V : B := True);
    procedure Set_Optimize_Alignment_Space        (Id : E; V : B := True);
    procedure Set_Optimize_Alignment_Time         (Id : E; V : B := True);
+   procedure Set_Original_Access_Type            (Id : E; V : E);
    procedure Set_Original_Array_Type             (Id : E; V : E);
    procedure Set_Original_Record_Component       (Id : E; V : E);
    procedure Set_Overlays_Constant               (Id : E; V : B := True);
@@ -7546,6 +7555,7 @@ package Einfo is
    pragma Inline (OK_To_Reorder_Components);
    pragma Inline (Optimize_Alignment_Space);
    pragma Inline (Optimize_Alignment_Time);
+   pragma Inline (Original_Access_Type);
    pragma Inline (Original_Array_Type);
    pragma Inline (Original_Record_Component);
    pragma Inline (Overlays_Constant);
@@ -7943,6 +7953,7 @@ package Einfo is
    pragma Inline (Set_OK_To_Rename);
    pragma Inline (Set_Optimize_Alignment_Space);
    pragma Inline (Set_Optimize_Alignment_Time);
+   pragma Inline (Set_Original_Access_Type);
    pragma Inline (Set_Original_Array_Type);
    pragma Inline (Set_Original_Record_Component);
    pragma Inline (Set_Overlays_Constant);
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 0312187f1a8..6a15dd532e5 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -5067,6 +5067,12 @@ package body Exp_Ch9 is
       Insert_After (N, Decl1);
       Analyze (Decl1);
 
+      --  Associate the access to subprogram with its original access to
+      --  protected subprogram type. Needed by the backend to know that this
+      --  type corresponds with an access to protected subprogram type.
+
+      Set_Original_Access_Type (D_T2, T);
+
       --  Create Equivalent_Type, a record with two components for an access to
       --  object and an access to subprogram.
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 337ff456c00..5e937249b58 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3168,6 +3168,15 @@ package body Sem_Ch3 is
 
          Apply_Scalar_Range_Check (E, T);
          Apply_Static_Length_Check (E, T);
+
+         if Nkind (Original_Node (N)) = N_Object_Declaration
+           and then Comes_From_Source (Original_Node (N))
+           and then Formal_Verification_Mode  --  only call test if needed
+           and then not Is_SPARK_Initialization_Expr (E)
+         then
+            Check_Formal_Restriction
+              ("initialization expression is not appropriate", E);
+         end if;
       end if;
 
       --  If the No_Streams restriction is set, check that the type of the
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 91cc8121d60..feddff824e5 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7368,6 +7368,118 @@ package body Sem_Util is
       end if;
    end Is_Selector_Name;
 
+   ----------------------------------
+   -- Is_SPARK_Initialization_Expr --
+   ----------------------------------
+
+   function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean is
+      Is_Ok : Boolean;
+
+      Expr, Comp_Assn, Choice : Node_Id;
+   begin
+      Is_Ok := True;
+
+      pragma Assert (Nkind (N) in N_Subexpr);
+
+      case Nkind (N) is
+         when N_Character_Literal |
+              N_Integer_Literal   |
+              N_Real_Literal      |
+              N_String_Literal    |
+              N_Expanded_Name     |
+              N_Membership_Test   =>
+            null;
+
+         when N_Identifier =>
+            if Is_Entity_Name (N)
+              and then Present (Entity (N))  --  needed in some cases
+            then
+               case Ekind (Entity (N)) is
+                  when E_Constant            |
+                       E_Enumeration_Literal |
+                       E_Named_Integer       |
+                       E_Named_Real          =>
+                     null;
+                  when others =>
+                     Is_Ok := False;
+               end case;
+            end if;
+
+         when N_Qualified_Expression |
+              N_Type_Conversion      =>
+            Is_Ok := Is_SPARK_Initialization_Expr (Expression (N));
+
+         when N_Unary_Op =>
+            Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (N));
+
+         when N_Binary_Op | N_Short_Circuit =>
+            Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (N))
+              and then Is_SPARK_Initialization_Expr (Right_Opnd (N));
+
+         when N_Aggregate           |
+              N_Extension_Aggregate =>
+            if Nkind (N) = N_Extension_Aggregate then
+               Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (N));
+            end if;
+
+            Expr := First (Expressions (N));
+            while Present (Expr) loop
+               if not Is_SPARK_Initialization_Expr (Expr) then
+                  Is_Ok := False;
+                  goto Done;
+               end if;
+
+               Next (Expr);
+            end loop;
+
+            Comp_Assn := First (Component_Associations (N));
+            while Present (Comp_Assn) loop
+               Choice := First (Choices (Comp_Assn));
+               while Present (Choice) loop
+                  if Nkind (Choice) in N_Subexpr
+                    and then not Is_SPARK_Initialization_Expr (Choice)
+                  then
+                     Is_Ok := False;
+                     goto Done;
+                  end if;
+
+                  Next (Choice);
+               end loop;
+
+               Expr := Expression (Comp_Assn);
+               if Present (Expr)  --  needed for box association
+                 and then not Is_SPARK_Initialization_Expr (Expr)
+               then
+                  Is_Ok := False;
+                  goto Done;
+               end if;
+
+               Next (Comp_Assn);
+            end loop;
+
+         when N_Attribute_Reference =>
+            if Nkind (Prefix (N)) in N_Subexpr then
+               Is_Ok := Is_SPARK_Initialization_Expr (Prefix (N));
+            end if;
+
+            Expr := First (Expressions (N));
+            while Present (Expr) loop
+               if not Is_SPARK_Initialization_Expr (Expr) then
+                  Is_Ok := False;
+                  goto Done;
+               end if;
+
+               Next (Expr);
+            end loop;
+
+         when others =>
+            Is_Ok := False;
+      end case;
+
+      <<Done>>
+      return Is_Ok;
+   end Is_SPARK_Initialization_Expr;
+
    -------------------------------
    -- Is_SPARK_Object_Reference --
    -------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 715fc1b0499..6803dfb9b66 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -828,6 +828,11 @@ package Sem_Util is
    --  represent use of the N_Identifier node for a true identifier, when
    --  normally such nodes represent a direct name.
 
+   function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean;
+   --  Determines if the tree referenced by N represents an initialization
+   --  expression in SPARK, suitable for initializing an object in an object
+   --  declaration.
+
    function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
    --  Determines if the tree referenced by N represents an object in SPARK