lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants (with variable input).

gcc/ada/

2017-11-08  Piotr Trojanek  <trojanek@adacore.com>

	* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case
	for constants (with variable input).
	(Is_Constant_Object_Without_Variable_Input): Remove.

2017-11-08  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting.

2017-11-08  Piotr Trojanek  <trojanek@adacore.com>

	* spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK
	cross-references.
	(dspark): Remove hardcoded table bound.

2017-11-08  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Aggregate): For Ada2020 delta aggregates, use
	the type of the base of the construct to determine the type (or
	candidate interpretations) of the delta aggregate. This allows the
	construct to appear in a context that expects a private extension.
	* sem_res.adb (Resolve): Handle properly a delta aggregate with an
	overloaded base.

gcc/testsuite/

2017-11-08  Ed Schonberg  <schonberg@adacore.com>

	* gnat.dg/delta_aggr.adb: New testcase.

From-SVN: r254544

9 files changed, 85 insertions, 91 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8fbb417..beff132 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,30 @@
 2017-11-08  Piotr Trojanek  <trojanek@adacore.com>
 
+	* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case
+	for constants (with variable input).
+	(Is_Constant_Object_Without_Variable_Input): Remove.
+
+2017-11-08  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting.
+
+2017-11-08  Piotr Trojanek  <trojanek@adacore.com>
+
+	* spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK
+	cross-references.
+	(dspark): Remove hardcoded table bound.
+
+2017-11-08  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Analyze_Aggregate): For Ada2020 delta aggregates, use
+	the type of the base of the construct to determine the type (or
+	candidate interpretations) of the delta aggregate. This allows the
+	construct to appear in a context that expects a private extension.
+	* sem_res.adb (Resolve): Handle properly a delta aggregate with an
+	overloaded base.
+
+2017-11-08  Piotr Trojanek  <trojanek@adacore.com>
+
 	* spark_xrefs.ads (SPARK_Xref_Record): Replace file and scope indices
 	with Entity_Id of the reference.
 	* spark_xrefs.adb (dspark): Adapt pretty-printing routine.
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 063b812..b8f6d99 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -12909,8 +12909,8 @@ package body Exp_Ch9 is
       end if;
 
       --  If the type of the dispatching object is an access type then return
-      --  an explicit dereference  of a copy of the object, and note that
-      --  this is the controlling actual of the call.
+      --  an explicit dereference  of a copy of the object, and note that this
+      --  is the controlling actual of the call.
 
       if Is_Access_Type (Etype (Object)) then
          Object :=
@@ -14590,9 +14590,9 @@ package body Exp_Ch9 is
 
             --    Jnn'unchecked_access
 
-            --  and add it to aggegate for access to formals. Note that
-            --  the actual may be by-copy but still be a controlling actual
-            --  if it is an access to class-wide interface.
+            --  and add it to aggegate for access to formals. Note that the
+            --  actual may be by-copy but still be a controlling actual if it
+            --  is an access to class-wide interface.
 
             if not Is_Controlling_Actual (Actual) then
                Append_To (Params,
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 8cc2e72..37349fa 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -252,11 +252,6 @@ package body SPARK_Specific is
       function Get_Scope_Num (E : Entity_Id) return Nat;
       --  Return the scope number associated with the entity E
 
-      function Is_Constant_Object_Without_Variable_Input
-        (E : Entity_Id) return Boolean;
-      --  Return True if E is known to have no variable input, as defined in
-      --  SPARK RM.
-
       function Is_Future_Scope_Entity
         (E : Entity_Id;
          S : Scope_Index) return Boolean;
@@ -332,50 +327,6 @@ package body SPARK_Specific is
 
       function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
 
-      -----------------------------------------------
-      -- Is_Constant_Object_Without_Variable_Input --
-      -----------------------------------------------
-
-      function Is_Constant_Object_Without_Variable_Input
-        (E : Entity_Id) return Boolean
-      is
-      begin
-         case Ekind (E) is
-
-            --  A constant is known to have no variable input if its
-            --  initializing expression is static (a value which is
-            --  compile-time-known is not guaranteed to have no variable input
-            --  as defined in the SPARK RM). Otherwise, the constant may or not
-            --  have variable input.
-
-            when E_Constant =>
-               declare
-                  Decl : Node_Id;
-               begin
-                  if Present (Full_View (E)) then
-                     Decl := Parent (Full_View (E));
-                  else
-                     Decl := Parent (E);
-                  end if;
-
-                  if Is_Imported (E) then
-                     return False;
-                  else
-                     pragma Assert (Present (Expression (Decl)));
-                     return Is_Static_Expression (Expression (Decl));
-                  end if;
-               end;
-
-            when E_In_Parameter
-               | E_Loop_Parameter
-            =>
-               return True;
-
-            when others =>
-               return False;
-         end case;
-      end Is_Constant_Object_Without_Variable_Input;
-
       ----------------------------
       -- Is_Future_Scope_Entity --
       ----------------------------
@@ -729,7 +680,6 @@ package body SPARK_Specific is
          declare
             Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
             Ref       : Xref_Key   renames Ref_Entry.Key;
-            Typ       : Character;
 
          begin
             --  If this assertion fails, the scope which we are looking for is
@@ -757,24 +707,10 @@ package body SPARK_Specific is
                pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
             end loop;
 
-            --  References to constant objects without variable inputs (see
-            --  SPARK RM 3.3.1) are considered specially in SPARK section,
-            --  because these will be translated as constants in the
-            --  intermediate language for formal verification, and should
-            --  therefore never appear in frame conditions. Other constants may
-            --  later be treated the same, up to GNATprove to decide based on
-            --  its flow analysis.
-
-            if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
-               Typ := 'c';
-            else
-               Typ := Ref.Typ;
-            end if;
-
             SPARK_Xref_Table.Append (
               (Entity    => Unique_Entity (Ref.Ent),
                Ref_Scope => Ref.Ref_Scope,
-               Rtype     => Typ));
+               Rtype     => Ref.Typ));
          end;
       end loop;
 
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 5380235..cfc4db7 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -414,12 +414,44 @@ package body Sem_Ch4 is
    -----------------------
 
    --  Most of the analysis of Aggregates requires that the type be known,
-   --  and is therefore put off until resolution.
+   --  and is therefore put off until resolution of the context.
+   --  Delta aggregates have a base component that determines the type of the
+   --  enclosing aggregate so its type can be ascertained earlier. This also
+   --  allows delta aggregates to appear in the context of a record type with
+   --  a private extension, as per the latest update of AI2-0127.
 
    procedure Analyze_Aggregate (N : Node_Id) is
    begin
       if No (Etype (N)) then
-         Set_Etype (N, Any_Composite);
+         if Nkind (N) = N_Delta_Aggregate then
+            declare
+               Base : constant Node_Id := Expression (N);
+               I  : Interp_Index;
+               It : Interp;
+
+            begin
+               Analyze (Base);
+
+               --  If the base is overloaded, propagate interpretations
+               --  to the enclosing aggregate.
+
+               if Is_Overloaded (Base) then
+                  Get_First_Interp (Base, I, It);
+                  Set_Etype (N, Any_Type);
+
+                  while Present (It.Nam) loop
+                     Add_One_Interp (N, It.Typ, It.Typ);
+                     Get_Next_Interp (I, It);
+                  end loop;
+
+               else
+                  Set_Etype (N, Etype (Base));
+               end if;
+            end;
+
+         else
+            Set_Etype (N, Any_Composite);
+         end if;
       end if;
    end Analyze_Aggregate;
 
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 1e140ee..e84fda2 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -2371,9 +2371,9 @@ package body Sem_Disp is
    -----------------------------------
 
    function Is_Inherited_Public_Operation (Op : Entity_Id) return Boolean is
+      Pack_Decl : Node_Id;
       Prim      : Entity_Id := Op;
       Scop      : Entity_Id := Prim;
-      Pack_Decl : Node_Id;
 
    begin
       --  Locate the ultimate non-hidden alias entity
@@ -2386,9 +2386,11 @@ package body Sem_Disp is
 
       if Comes_From_Source (Prim) and then Ekind (Scop) = E_Package then
          Pack_Decl := Unit_Declaration_Node (Scop);
-         return Nkind (Pack_Decl) = N_Package_Declaration
-           and then List_Containing (Unit_Declaration_Node (Prim)) =
-                            Visible_Declarations (Specification (Pack_Decl));
+
+         return
+           Nkind (Pack_Decl) = N_Package_Declaration
+             and then List_Containing (Unit_Declaration_Node (Prim)) =
+                        Visible_Declarations (Specification (Pack_Decl));
 
       else
          return False;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 07e4ba8..afa2e8e 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -2439,13 +2439,11 @@ package body Sem_Res is
                   Set_Entity (N, Seen);
                   Generate_Reference (Seen, N);
 
-               elsif Nkind (N) = N_Case_Expression then
-                  Set_Etype (N, Expr_Type);
-
-               elsif Nkind (N) = N_Character_Literal then
-                  Set_Etype (N, Expr_Type);
-
-               elsif Nkind (N) = N_If_Expression then
+               elsif Nkind_In (N, N_Case_Expression,
+                                  N_Character_Literal,
+                                  N_If_Expression,
+                                  N_Delta_Aggregate)
+               then
                   Set_Etype (N, Expr_Type);
 
                --  AI05-0139-2: Expression is overloaded because type has
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 429310c..175f5e7 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -597,6 +597,7 @@ package body Sem_Util is
 
       procedure Inner (E : Entity_Id) is
          Scop : Node_Id;
+
       begin
          --  If entity has an internal name, skip by it, and print its scope.
          --  Note that we strip a final R from the name before the test; this
@@ -13198,14 +13199,14 @@ package body Sem_Util is
       if Ekind (Proc_Nam) = E_Procedure
         and then Present (Parameter_Specifications (Parent (Proc_Nam)))
       then
-         Param := Parameter_Type (First (
-                    Parameter_Specifications (Parent (Proc_Nam))));
+         Param :=
+           Parameter_Type
+             (First (Parameter_Specifications (Parent (Proc_Nam))));
 
-         --  The formal may be an anonymous access type.
+         --  The formal may be an anonymous access type
 
          if Nkind (Param) = N_Access_Definition then
             Param_Typ := Entity (Subtype_Mark (Param));
-
          else
             Param_Typ := Etype (Param);
          end if;
@@ -23329,6 +23330,7 @@ package body Sem_Util is
          declare
             H  : Entity_Id := Homonym (N);
             Nr : Nat := 1;
+
          begin
             while Present (H) loop
                if Scope (H) = Scope (N) then
diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb
index 48b8b58..552ed59 100644
--- a/gcc/ada/spark_xrefs.adb
+++ b/gcc/ada/spark_xrefs.adb
@@ -39,7 +39,7 @@ package body SPARK_Xrefs is
       Write_Line ("SPARK Xrefs File Table");
       Write_Line ("----------------------");
 
-      for Index in 1 .. SPARK_File_Table.Last loop
+      for Index in SPARK_File_Table.First .. SPARK_File_Table.Last loop
          declare
             AFR : SPARK_File_Record renames SPARK_File_Table.Table (Index);
 
@@ -62,7 +62,7 @@ package body SPARK_Xrefs is
       Write_Line ("SPARK Xrefs Scope Table");
       Write_Line ("-----------------------");
 
-      for Index in 1 .. SPARK_Scope_Table.Last loop
+      for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
          declare
             ASR : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
 
@@ -92,7 +92,7 @@ package body SPARK_Xrefs is
       Write_Line ("SPARK Xref Table");
       Write_Line ("----------------");
 
-      for Index in 1 .. SPARK_Xref_Table.Last loop
+      for Index in SPARK_Xref_Table.First .. SPARK_Xref_Table.Last loop
          declare
             AXR : SPARK_Xref_Record renames SPARK_Xref_Table.Table (Index);
 
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index 79a21b9..4223003 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -75,7 +75,6 @@ package SPARK_Xrefs is
       Rtype : Character;
       --  Indicates type of the reference, using code used in ALI file:
       --    r = reference
-      --    c = reference to constant object
       --    m = modification
       --    s = call
    end record;