[multiple changes]

2013-10-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb: in Ada 2012 access_to_function types can have
	in-out parameters.
	(Derived_Type_Declaration): SPARK restriction
	must be flagged on the original node, since it may have been
	written as a subtype declaration.
	(Analyze_Subtype_Declaration): Do not enter name of
	entity in declaration if it is the current entity, because it may
	have been inserted in a previous analysis and it appears in the
	else_part of an if-statement that is rewritten during expansion.

2013-10-13  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove procedure.
	(Expand_SPARK): Remove call to Expand_SPARK_N_Attribute_Reference and
	Expand_SPARK_N_Simple_Return_Statement.
	(Expand_SPARK_N_Simple_Return_Statement,
 	Expand_SPARK_Simple_Function_Return): Remove procedures.

From-SVN: r203502

3 files changed, 34 insertions, 111 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 347f311..b8483d4 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,23 @@
+2013-10-13  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb: in Ada 2012 access_to_function types can have
+	in-out parameters.
+	(Derived_Type_Declaration): SPARK restriction
+	must be flagged on the original node, since it may have been
+	written as a subtype declaration.
+	(Analyze_Subtype_Declaration): Do not enter name of
+	entity in declaration if it is the current entity, because it may
+	have been inserted in a previous analysis and it appears in the
+	else_part of an if-statement that is rewritten during expansion.
+
+2013-10-13  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove procedure.
+	(Expand_SPARK): Remove call to Expand_SPARK_N_Attribute_Reference and
+	Expand_SPARK_N_Simple_Return_Statement.
+	(Expand_SPARK_N_Simple_Return_Statement,
+ 	Expand_SPARK_Simple_Function_Return): Remove procedures.
+
 2013-10-13  Vincent Celier  <celier@adacore.com>
 
 	* gnat_ugn.texi: Minor editing.
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 0050799..bd8932e 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -25,19 +25,15 @@
 
 with Atree;    use Atree;
 with Einfo;    use Einfo;
-with Exp_Attr; use Exp_Attr;
 with Exp_Ch4;  use Exp_Ch4;
 with Exp_Ch6;  use Exp_Ch6;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
-with Rtsfind;  use Rtsfind;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
-with Snames;   use Snames;
 with Stand;    use Stand;
-with Tbuild;   use Tbuild;
 
 package body Exp_SPARK is
 
@@ -51,18 +47,9 @@ package body Exp_SPARK is
    --    * expansion of actuals to introduce necessary temporaries
    --    * replacement of renaming by subprogram renamed
 
-   procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-   --  Expand attributes 'Old and 'Result only
-
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
-   procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id);
-   --  Insert conversion on function return if necessary
-
-   procedure Expand_SPARK_Simple_Function_Return (N : Node_Id);
-   --  Expand simple return from function
-
    procedure Expand_Potential_Renaming (N : Node_Id);
    --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
    --  replace N with the renamed object.
@@ -74,8 +61,6 @@ package body Exp_SPARK is
    procedure Expand_SPARK (N : Node_Id) is
    begin
       case Nkind (N) is
-         when N_Attribute_Reference =>
-            Expand_SPARK_N_Attribute_Reference (N);
 
          --  Qualification of entity names in formal verification mode
          --  is limited to the addition of a suffix for homonyms (see
@@ -107,9 +92,6 @@ package body Exp_SPARK is
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
 
-         when N_Simple_Return_Statement =>
-            Expand_SPARK_N_Simple_Return_Statement (N);
-
          --  In SPARK mode, no other constructs require expansion
 
          when others =>
@@ -179,24 +161,6 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Call;
 
-   ----------------------------------------
-   -- Expand_SPARK_N_Attribute_Reference --
-   ----------------------------------------
-
-   procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
-      Id : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
-
-   begin
-      case Id is
-         when Attribute_Old    |
-              Attribute_Result =>
-            Expand_N_Attribute_Reference (N);
-
-         when others =>
-            null;
-      end case;
-   end Expand_SPARK_N_Attribute_Reference;
-
    ------------------------------------------------
    -- Expand_SPARK_N_Object_Renaming_Declaration --
    ------------------------------------------------
@@ -208,80 +172,6 @@ package body Exp_SPARK is
       Evaluate_Name (Name (N));
    end Expand_SPARK_N_Object_Renaming_Declaration;
 
-   --------------------------------------------
-   -- Expand_SPARK_N_Simple_Return_Statement --
-   --------------------------------------------
-
-   procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id) is
-   begin
-      --  Defend against previous errors (i.e. the return statement calls a
-      --  function that is not available in configurable runtime).
-
-      if Present (Expression (N))
-        and then Nkind (Expression (N)) = N_Empty
-      then
-         return;
-      end if;
-
-      --  Distinguish the function and non-function cases:
-
-      case Ekind (Return_Applies_To (Return_Statement_Entity (N))) is
-
-         when E_Function          |
-              E_Generic_Function  =>
-            Expand_SPARK_Simple_Function_Return (N);
-
-         when E_Procedure         |
-              E_Generic_Procedure |
-              E_Entry             |
-              E_Entry_Family      |
-              E_Return_Statement =>
-            null;
-
-         when others =>
-            raise Program_Error;
-      end case;
-
-   exception
-      when RE_Not_Available =>
-         return;
-   end Expand_SPARK_N_Simple_Return_Statement;
-
-   -----------------------------------------
-   -- Expand_SPARK_Simple_Function_Return --
-   -----------------------------------------
-
-   procedure Expand_SPARK_Simple_Function_Return (N : Node_Id) is
-      Scope_Id : constant Entity_Id :=
-                   Return_Applies_To (Return_Statement_Entity (N));
-      --  The function we are returning from
-
-      R_Type : constant Entity_Id := Etype (Scope_Id);
-      --  The result type of the function
-
-      Exp : constant Node_Id := Expression (N);
-      pragma Assert (Present (Exp));
-
-      Exptyp : constant Entity_Id := Etype (Exp);
-      --  The type of the expression (not necessarily the same as R_Type)
-
-   begin
-      --  Check the result expression of a scalar function against the subtype
-      --  of the function by inserting a conversion. This conversion must
-      --  eventually be performed for other classes of types, but for now it's
-      --  only done for scalars.
-      --  ???
-
-      if Is_Scalar_Type (Exptyp) then
-         Rewrite (Exp, Convert_To (R_Type, Exp));
-
-         --  The expression is resolved to ensure that the conversion gets
-         --  expanded to generate a possible constraint check.
-
-         Analyze_And_Resolve (Exp, R_Type);
-      end if;
-   end Expand_SPARK_Simple_Function_Return;
-
    -------------------------------
    -- Expand_Potential_Renaming --
    -------------------------------
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 8410409..6b2e0a6 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1236,12 +1236,14 @@ package body Sem_Ch3 is
       --  be updated when the full type declaration is seen. This only applies
       --  to incomplete types declared in some enclosing scope, not to limited
       --  views from other packages.
+      --  Prior to Ada 2012, access to functions can only have in_parameters.
 
       if Present (Formals) then
          Formal := First_Formal (Desig_Type);
          while Present (Formal) loop
             if Ekind (Formal) /= E_In_Parameter
               and then Nkind (T_Def) = N_Access_Function_Definition
+              and then Ada_Version < Ada_2012
             then
                Error_Msg_N ("functions can only have IN parameters", Formal);
             end if;
@@ -4050,6 +4052,13 @@ package body Sem_Ch3 is
       --  type with constraints. In this case the entity has been introduced
       --  in the private declaration.
 
+      --  Finally this happens in some complex cases  when validity checks are
+      --  enabled, where the same subtype declaration may be analyzed twice.
+      --  This can happen if the subtype is created by the pre-analysis of
+      --  an attribute tht gives the range of a loop statement, and the loop
+      --  itself appears within an if_statement that will be rewritten during
+      --  expansion.
+
       if Skip
         or else (Present (Etype (Id))
                   and then (Is_Private_Type (Etype (Id))
@@ -4058,6 +4067,9 @@ package body Sem_Ch3 is
       then
          null;
 
+      elsif Current_Entity (Id) = Id then
+         null;
+
       else
          Enter_Name (Id);
       end if;
@@ -14804,7 +14816,8 @@ package body Sem_Ch3 is
       --  extensions of tagged record types.
 
       if No (Extension) then
-         Check_SPARK_Restriction ("derived type is not allowed", N);
+         Check_SPARK_Restriction
+           ("derived type is not allowed", Original_Node (N));
       end if;
    end Derived_Type_Declaration;