[multiple changes]

2013-04-25  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_N_In): Remove procedure.
	(Expand_SPARK): Remove special expansion for membership tests.

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Object_Declaration): Update all places
	that should use constant Base_Typ. When building an invariant
	check, account for invariants coming from the base type. Prevent
	the creation of a junk invariant check when the related object
	is of an array type and it is initialized with an aggregate.
	* exp_util.adb (Make_Invariant_Call): Typ is now a variable. Use
	the base type to create an invariant call when the type of the
	expression is a composite subtype.

2013-04-25  Vasiliy Fofanov  <fofanov@adacore.com>

	* a-cborse.adb: Fix minor typo.

2013-04-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Different_Generic_Profile): A spec and body
	match in an instance if a subtype declaration that renames a
	generic actual with the same name appears between spec and body.

From-SVN: r198294

6 files changed, 105 insertions, 61 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3ce1469..35e3d73 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,29 @@
+2013-04-25  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_N_In): Remove procedure.
+	(Expand_SPARK): Remove special expansion for membership tests.
+
+2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch3.adb (Expand_N_Object_Declaration): Update all places
+	that should use constant Base_Typ. When building an invariant
+	check, account for invariants coming from the base type. Prevent
+	the creation of a junk invariant check when the related object
+	is of an array type and it is initialized with an aggregate.
+	* exp_util.adb (Make_Invariant_Call): Typ is now a variable. Use
+	the base type to create an invariant call when the type of the
+	expression is a composite subtype.
+
+2013-04-25  Vasiliy Fofanov  <fofanov@adacore.com>
+
+	* a-cborse.adb: Fix minor typo.
+
+2013-04-25  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Different_Generic_Profile): A spec and body
+	match in an instance if a subtype declaration that renames a
+	generic actual with the same name appears between spec and body.
+
 2013-04-25  Robert Dewar  <dewar@adacore.com>
 
 	* sem_util.adb: Minor reformatting.
diff --git a/gcc/ada/a-cborse.adb b/gcc/ada/a-cborse.adb
index eacd3eb..baeedba 100644
--- a/gcc/ada/a-cborse.adb
+++ b/gcc/ada/a-cborse.adb
@@ -1815,7 +1815,7 @@ package body Ada.Containers.Bounded_Ordered_Sets is
          end if;
 
          --  Item is not equivalent to any other element in the tree
-         --  (specifically, it is less then Nodes (Hint).Element), so it is
+         --  (specifically, it is less than Nodes (Hint).Element), so it is
          --  safe to assign the value of Item to Node.Element. This means that
          --  the node will have to move to a different position in the tree
          --  (because its element will have a different value).
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 7606762..1e50036 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -5035,10 +5035,14 @@ package body Exp_Ch3 is
          --  with invariants, and invariant checks are enabled, then insert an
          --  invariant check after the object declaration. Note that it is OK
          --  to clobber the object with an invalid value since if the exception
-         --  is raised, then the object will go out of scope.
+         --  is raised, then the object will go out of scope. In the case where
+         --  an array object is initialized with an aggregate, the expression
+         --  is removed. Check flag Has_Init_Expression to avoid generating a
+         --  junk invariant check.
 
-         if Has_Invariants (Typ)
-           and then Present (Invariant_Procedure (Typ))
+         if Has_Invariants (Base_Typ)
+           and then Present (Invariant_Procedure (Base_Typ))
+           and then not Has_Init_Expression (N)
          then
             Insert_After (N,
               Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));
@@ -5052,18 +5056,14 @@ package body Exp_Ch3 is
          --  Initialize call as it is required but one for each ancestor of
          --  its type. This processing is suppressed if No_Initialization set.
 
-         if not Needs_Finalization (Typ)
-           or else No_Initialization (N)
-         then
+         if not Needs_Finalization (Typ) or else No_Initialization (N) then
             null;
 
-         elsif not Abort_Allowed
-           or else not Comes_From_Source (N)
-         then
+         elsif not Abort_Allowed or else not Comes_From_Source (N) then
             Insert_Action_After (Init_After,
               Make_Init_Call
                 (Obj_Ref => New_Occurrence_Of (Def_Id, Loc),
-                 Typ     => Base_Type (Typ)));
+                 Typ     => Base_Typ));
 
          --  Abort allowed
 
@@ -5086,7 +5086,7 @@ package body Exp_Ch3 is
                L   : constant List_Id := New_List (
                        Make_Init_Call
                          (Obj_Ref => New_Occurrence_Of (Def_Id, Loc),
-                          Typ     => Base_Type (Typ)));
+                          Typ     => Base_Typ));
 
                Blk : constant Node_Id :=
                        Make_Block_Statement (Loc,
@@ -5558,7 +5558,7 @@ package body Exp_Ch3 is
                Insert_Action_After (Init_After,
                  Make_Adjust_Call (
                    Obj_Ref => New_Reference_To (Def_Id, Loc),
-                   Typ     => Base_Type (Typ)));
+                   Typ     => Base_Typ));
             end if;
 
             --  For tagged types, when an init value is given, the tag has to
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index cd32353..0050799 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -30,7 +30,6 @@ 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 Nlists;   use Nlists;
 with Rtsfind;  use Rtsfind;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Res;  use Sem_Res;
@@ -55,9 +54,6 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
    --  Expand attributes 'Old and 'Result only
 
-   procedure Expand_SPARK_N_In (N : Node_Id);
-   --  Expand set membership into individual ones
-
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
@@ -102,9 +98,6 @@ package body Exp_SPARK is
               N_Identifier    =>
             Expand_Potential_Renaming (N);
 
-         when N_In =>
-            Expand_SPARK_N_In (N);
-
          --  A NOT IN B gets transformed to NOT (A IN B). This is the same
          --  expansion used in the normal case, so shared the code.
 
@@ -204,17 +197,6 @@ package body Exp_SPARK is
       end case;
    end Expand_SPARK_N_Attribute_Reference;
 
-   -----------------------
-   -- Expand_SPARK_N_In --
-   -----------------------
-
-   procedure Expand_SPARK_N_In (N : Node_Id) is
-   begin
-      if Present (Alternatives (N)) then
-         Expand_Set_Membership (N);
-      end if;
-   end Expand_SPARK_N_In;
-
    ------------------------------------------------
    -- Expand_SPARK_N_Object_Renaming_Declaration --
    ------------------------------------------------
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index df4d170..0473bfa 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -5466,11 +5466,24 @@ package body Exp_Util is
 
    function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
       Loc : constant Source_Ptr := Sloc (Expr);
-      Typ : constant Entity_Id  := Etype (Expr);
+      Typ : Entity_Id;
 
    begin
+      Typ := Etype (Expr);
+
+      --  Subtypes may be subject to invariants coming from their respective
+      --  base types.
+
+      if Ekind_In (Typ, E_Array_Subtype,
+                        E_Private_Subtype,
+                        E_Record_Subtype)
+      then
+         Typ := Base_Type (Typ);
+      end if;
+
       pragma Assert
         (Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
+
       return
         Make_Procedure_Call_Statement (Loc,
           Name                   =>
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 0e56e16..68edadf 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -7547,8 +7547,8 @@ package body Sem_Ch6 is
               or else Scope (T1) /= Scope (T2);
 
          --  If T2 is a generic actual type it is declared as the subtype of
-         --  the actual.  If that actual is itself a subtype we need to use
-         --  its own base type to check for compatibility.
+         --  the actual. If that actual is itself a subtype we need to use its
+         --  own base type to check for compatibility.
 
          elsif Ekind (BT2) = Ekind (T2) and then BT1 = Base_Type (BT2) then
             return True;
@@ -8304,10 +8304,35 @@ package body Sem_Ch6 is
       function Different_Generic_Profile (E : Entity_Id) return Boolean is
          F1, F2 : Entity_Id;
 
+         function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean;
+         --  Check that the types of corresponding formals have the same
+         --  generic actual if any. We have to account for subtypes of a
+         --  generic formal, declared between a spec and a body, which may
+         --  appear distinct in an instance but matched in the generic.
+
+         -------------------------
+         -- Same_Generic_Actual --
+         -------------------------
+
+         function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean is
+         begin
+            return Is_Generic_Actual_Type (T1) = Is_Generic_Actual_Type (T2)
+              or else
+                (Present (Parent (T1))
+                  and then Comes_From_Source (Parent (T1))
+                  and then Nkind (Parent (T1)) = N_Subtype_Declaration
+                  and then Is_Entity_Name (Subtype_Indication (Parent (T1)))
+                  and then Entity (Subtype_Indication (Parent (T1))) = T2);
+         end Same_Generic_Actual;
+
+      --  Start of processing for Different_Generic_Profile
+
       begin
-         if Ekind (E) = E_Function
-           and then Is_Generic_Actual_Type (Etype (E)) /=
-                    Is_Generic_Actual_Type (Etype (Designator))
+         if not In_Instance then
+            return False;
+
+         elsif Ekind (E) = E_Function
+           and then not Same_Generic_Actual (Etype (E), Etype (Designator))
          then
             return True;
          end if;
@@ -8315,9 +8340,7 @@ package body Sem_Ch6 is
          F1 := First_Formal (Designator);
          F2 := First_Formal (E);
          while Present (F1) loop
-            if Is_Generic_Actual_Type (Etype (F1)) /=
-               Is_Generic_Actual_Type (Etype (F2))
-            then
+            if not Same_Generic_Actual (Etype (F1), Etype (F2)) then
                return True;
             end if;
 
@@ -8414,7 +8437,7 @@ package body Sem_Ch6 is
                --  If E is an internal function with a controlling result that
                --  was created for an operation inherited by a null extension,
                --  it may be overridden by a body without a previous spec (one
-               --  more reason why these should be shunned). In that case
+               --  more reason why these should be shunned). In that case we
                --  remove the generated body if present, because the current
                --  one is the explicit overriding.
 
@@ -8954,9 +8977,9 @@ package body Sem_Ch6 is
             --  All other node types cannot appear in this context. Strictly
             --  we should raise a fatal internal error. Instead we just ignore
             --  the nodes. This means that if anyone makes a mistake in the
-            --  expander and mucks an expression tree irretrievably, the
-            --  result will be a failure to detect a (probably very obscure)
-            --  case of non-conformance, which is better than bombing on some
+            --  expander and mucks an expression tree irretrievably, the result
+            --  will be a failure to detect a (probably very obscure) case
+            --  of non-conformance, which is better than bombing on some
             --  case where two expressions do in fact conform.
 
             when others =>
@@ -9146,8 +9169,8 @@ package body Sem_Ch6 is
          return Type_Conformant
                   (Iface_Prim, Prim, Skip_Controlling_Formals => True);
 
-      --  Case of a function returning an interface, or an access to one.
-      --  Check that the return types correspond.
+      --  Case of a function returning an interface, or an access to one. Check
+      --  that the return types correspond.
 
       elsif Implements_Interface (Typ, Iface) then
          if (Ekind (Etype (Prim)) = E_Anonymous_Access_Type)
@@ -9368,8 +9391,8 @@ package body Sem_Ch6 is
                   Next_Elmt (Prim_Elt);
                end loop;
 
-               --  If no match found, then the new subprogram does not
-               --  override in the generic (nor in the instance).
+               --  If no match found, then the new subprogram does not override
+               --  in the generic (nor in the instance).
 
                --  If the type in question is not abstract, and the subprogram
                --  is, this will be an error if the new operation is in the
@@ -9494,9 +9517,9 @@ package body Sem_Ch6 is
 
          --  Insert inequality right after equality if it is explicit or after
          --  the derived type when implicit. These entities are created only
-         --  for visibility purposes, and eventually replaced in the course of
-         --  expansion, so they do not need to be attached to the tree and seen
-         --  by the back-end. Keeping them internal also avoids spurious
+         --  for visibility purposes, and eventually replaced in the course
+         --  of expansion, so they do not need to be attached to the tree and
+         --  seen by the back-end. Keeping them internal also avoids spurious
          --  freezing problems. The declaration is inserted in the tree for
          --  analysis, and removed afterwards. If the equality operator comes
          --  from an explicit declaration, attach the inequality immediately
@@ -9605,9 +9628,9 @@ package body Sem_Ch6 is
          New_E : Entity_Id) return Boolean;
       --  Check whether new subprogram and old subprogram are both inherited
       --  from subprograms that have distinct dispatch table entries. This can
-      --  occur with derivations from instances with accidental homonyms.
-      --  The function is conservative given that the converse is only true
-      --  within instances that contain accidental overloadings.
+      --  occur with derivations from instances with accidental homonyms. The
+      --  function is conservative given that the converse is only true within
+      --  instances that contain accidental overloadings.
 
       ------------------------------------
       -- Check_For_Primitive_Subprogram --
@@ -10274,8 +10297,8 @@ package body Sem_Ch6 is
          Check_Dispatching_Operation (S, Empty);
          Check_For_Primitive_Subprogram (Is_Primitive_Subp);
 
-         --  If subprogram has an explicit declaration, check whether it
-         --  has an overriding indicator.
+         --  If subprogram has an explicit declaration, check whether it has an
+         --  overriding indicator.
 
          if Comes_From_Source (S) then
             Check_Synchronized_Overriding (S, Overridden_Subp);
@@ -10366,11 +10389,11 @@ package body Sem_Ch6 is
             if Scope (E) /= Current_Scope then
                null;
 
-            --  Ada 2012 (AI05-0165): For internally generated bodies of
-            --  null procedures locate the internally generated spec. We
-            --  enforce mode conformance since a tagged type may inherit
-            --  from interfaces several null primitives which differ only
-            --  in the mode of the formals.
+            --  Ada 2012 (AI05-0165): For internally generated bodies of null
+            --  procedures locate the internally generated spec. We enforce
+            --  mode conformance since a tagged type may inherit from
+            --  interfaces several null primitives which differ only in
+            --  the mode of the formals.
 
             elsif not Comes_From_Source (S)
               and then Is_Null_Procedure (S)