From: Pierre-Marie de Rodat Date: Wed, 8 Nov 2017 16:45:55 +0000 (+0000) Subject: lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants... X-Git-Tag: upstream/12.2.0~35731 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=9ac3cbb39d0988cb23dee4fd6a67bf7a3020bb69;p=platform%2Fupstream%2Fgcc.git lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants (with variable input). gcc/ada/ 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. gcc/testsuite/ 2017-11-08 Ed Schonberg * gnat.dg/delta_aggr.adb: New testcase. From-SVN: r254544 --- 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 + * 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 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; diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 4da3435..d4a0b0f 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 0000000..57e0a69 --- /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;