diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8fbb4176f69..beff132b57e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,28 @@ +2017-11-08 Piotr Trojanek + + * 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 + + * exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting. + +2017-11-08 Piotr Trojanek + + * spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK + cross-references. + (dspark): Remove hardcoded table bound. + +2017-11-08 Ed Schonberg + + * 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 * spark_xrefs.ads (SPARK_Xref_Record): Replace file and scope indices diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 063b812f9bc..b8f6d99390f 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 8cc2e7299fd..37349faf2f0 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 538023524e3..cfc4db7c2b6 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 1e140ee8210..e84fda29331 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 07e4ba83f66..afa2e8e966c 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 429310cd80d..175f5e7c969 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 48b8b584747..552ed595ead 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 79a21b9faf6..422300381a8 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; diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 4da3435f37c..d4a0b0f3c26 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2017-11-08 Ed Schonberg + + * gnat.dg/delta_aggr.adb: New testcase. + 2017-11-08 Jakub Jelinek * g++.dg/pr57878.C (__sso_string_base::_M_get_allocator): Return diff --git a/gcc/testsuite/gnat.dg/delta_aggr.adb b/gcc/testsuite/gnat.dg/delta_aggr.adb new file mode 100644 index 00000000000..57e0a69693a --- /dev/null +++ b/gcc/testsuite/gnat.dg/delta_aggr.adb @@ -0,0 +1,51 @@ +-- { dg-do compile } +-- { dg-options "-gnat2020" } + +procedure Delta_Aggr is + type T1 is tagged record + F1, F2, F3 : Integer := 0; + end record; + + function Make (X : Integer) return T1 is + begin + return (10, 20, 30); + end Make; + + package Pkg is + type T2 is new T1 with private; + X, Y : constant T2; + function Make (X : Integer) return T2; + private + type T2 is new T1 with + record + F4 : Integer := 0; + end record; + X : constant T2 := (0, 0, 0, 0); + Y : constant T2 := (1, 2, 0, 0); + end Pkg; + + package body Pkg is + function Make (X : Integer) return T2 is + begin + return (X, X ** 2, X ** 3, X ** 4); + end Make; + end Pkg; + + use Pkg; + + Z : T2 := (Y with delta F1 => 111); + + -- a legal delta aggregate whose type is a private extension + pragma Assert (Y = (X with delta F1 => 1, F2 => 2)); + pragma assert (Y.F2 = X.F1); + +begin + Z := (X with delta F1 => 1); + + -- The base of the delta aggregate can be overloaded, in which case + -- the candidate interpretations for the aggregate are those of the + -- base, to be resolved from context. + + Z := (Make (2) with delta F1 => 1); + null; +end Delta_Aggr;