From 21d7ef70aae92c62a6c39233e899b9ed70ace566 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 12:17:42 +0100 Subject: [PATCH] [multiple changes] 2015-10-26 Ed Schonberg * exp_ch4.adb (Expand_N_Case_Expression): In the scope of a predicate function, delay the expansion of the expression only if the target type has a specified Static_ Predicate aspect, because the expression is processed later. A dynamic predicate must be expanded in standard fashion. 2015-10-26 Claire Dross * a-nudira.ads: Remove SPARK_Mode as it currently causes an error. 2015-10-26 Arnaud Charlet * sem_aggr.adb, sem_type.adb, sem_ch12.adb, sem_res.adb, sem_ch4.adb, sem_ch8.adb, exp_aggr.adb, sem_eval.adb, s-fatgen.adb, a-tienio.adb: Fix typos. 2015-10-26 Hristian Kirtchev * sem_ch13.adb (Analyze_Aspect_Specifications): The processing for aspects Abstract_State, Ghost, Initial_Condition, Initializes and Refined_State no longer have to take SPARK_Mode into account. (Insert_After_SPARK_Mode): Removed. (Insert_Pragma): Update profile and comment on usage. The routine can now insert a pragma after the "header" of an instance. * sem_prag.adb (Analyze_If_Available): New routine. (Analyze_Pragma): Do not reset the Analyzed flag of various SPARK pragmas as they use the Is_Analyzed_Pragma attribute to avoid reanalysis. Various pragmas now trigger the analysis of related pragmas that depend on or are dependent on the current pragma. Remove the declaration order checks related to pragmas Abstract_State, Initial_Condition and Initializes. (Analyze_Pre_Post_Condition): Analyze pragmas SPARK_Mode and Volatile_Function prior to analyzing the pre/postcondition. (Check_Declaration_Order): Removed. (Check_Distinct_Name): Ensure that a potentially duplicated pragma Test_Case is not the pragma being analyzed. (Is_Followed_By_Pragma): Removed. From-SVN: r229331 --- gcc/ada/ChangeLog | 40 +++ gcc/ada/a-nudira.adb | 2 +- gcc/ada/a-nudira.ads | 3 +- gcc/ada/a-tienio.adb | 4 +- gcc/ada/exp_aggr.adb | 8 +- gcc/ada/exp_ch4.adb | 8 +- gcc/ada/s-fatgen.adb | 2 +- gcc/ada/sem_aggr.adb | 6 +- gcc/ada/sem_ch12.adb | 34 +-- gcc/ada/sem_ch13.adb | 262 +++++------------- gcc/ada/sem_ch4.adb | 6 +- gcc/ada/sem_ch8.adb | 6 +- gcc/ada/sem_eval.adb | 4 +- gcc/ada/sem_prag.adb | 644 +++++++++++++++++-------------------------- gcc/ada/sem_res.adb | 6 +- gcc/ada/sem_type.adb | 2 +- 16 files changed, 402 insertions(+), 635 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 38232d6f171..fff8b879093 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,43 @@ +2015-10-26 Ed Schonberg + + * exp_ch4.adb (Expand_N_Case_Expression): In the scope of a + predicate function, delay the expansion of the expression only + if the target type has a specified Static_ Predicate aspect, + because the expression is processed later. A dynamic predicate + must be expanded in standard fashion. + +2015-10-26 Claire Dross + + * a-nudira.ads: Remove SPARK_Mode as it currently causes an error. + +2015-10-26 Arnaud Charlet + + * sem_aggr.adb, sem_type.adb, sem_ch12.adb, sem_res.adb, sem_ch4.adb, + sem_ch8.adb, exp_aggr.adb, sem_eval.adb, s-fatgen.adb, a-tienio.adb: + Fix typos. + +2015-10-26 Hristian Kirtchev + + * sem_ch13.adb (Analyze_Aspect_Specifications): The processing + for aspects Abstract_State, Ghost, Initial_Condition, Initializes + and Refined_State no longer have to take SPARK_Mode into account. + (Insert_After_SPARK_Mode): Removed. + (Insert_Pragma): Update profile and comment on usage. The routine can + now insert a pragma after the "header" of an instance. + * sem_prag.adb (Analyze_If_Available): New routine. + (Analyze_Pragma): Do not reset the Analyzed flag of various + SPARK pragmas as they use the Is_Analyzed_Pragma attribute to + avoid reanalysis. Various pragmas now trigger the analysis + of related pragmas that depend on or are dependent on the + current pragma. Remove the declaration order checks related + to pragmas Abstract_State, Initial_Condition and Initializes. + (Analyze_Pre_Post_Condition): Analyze pragmas SPARK_Mode and + Volatile_Function prior to analyzing the pre/postcondition. + (Check_Declaration_Order): Removed. + (Check_Distinct_Name): Ensure that a potentially duplicated pragma + Test_Case is not the pragma being analyzed. + (Is_Followed_By_Pragma): Removed. + 2015-10-26 Ed Schonberg * sem_ch6.adb: Handle subprogram bodies without previous specs. diff --git a/gcc/ada/a-nudira.adb b/gcc/ada/a-nudira.adb index 156d018a1f3..251f852579c 100644 --- a/gcc/ada/a-nudira.adb +++ b/gcc/ada/a-nudira.adb @@ -29,7 +29,7 @@ -- -- ------------------------------------------------------------------------------ -package body Ada.Numerics.Discrete_Random with SPARK_Mode => Off is +package body Ada.Numerics.Discrete_Random is package SRN renames System.Random_Numbers; use SRN; diff --git a/gcc/ada/a-nudira.ads b/gcc/ada/a-nudira.ads index 7234a39729e..77501ec63ae 100644 --- a/gcc/ada/a-nudira.ads +++ b/gcc/ada/a-nudira.ads @@ -41,7 +41,7 @@ with System.Random_Numbers; generic type Result_Subtype is (<>); -package Ada.Numerics.Discrete_Random with SPARK_Mode is +package Ada.Numerics.Discrete_Random is -- Basic facilities @@ -65,7 +65,6 @@ package Ada.Numerics.Discrete_Random with SPARK_Mode is function Value (Coded_State : String) return State; private - pragma SPARK_Mode (Off); type Generator is new System.Random_Numbers.Generator; diff --git a/gcc/ada/a-tienio.adb b/gcc/ada/a-tienio.adb index b4e1e893283..e98f410eee9 100644 --- a/gcc/ada/a-tienio.adb +++ b/gcc/ada/a-tienio.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -97,7 +97,7 @@ package body Ada.Text_IO.Enumeration_IO is begin -- Ensure that Item is valid before attempting to retrieve the Image, to -- prevent the possibility of out-of-bounds addressing of index or image - -- tables. Units in the run-time library are normally compiled with + -- tables. Units in the run-time library are normally compiled with -- checks suppressed, which includes instantiated generics. if not Item'Valid then diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index f09759702aa..5266bca6cd5 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -2477,7 +2477,7 @@ package body Exp_Aggr is then Ancestor_Is_Expression := True; - -- Set up finalization data for enclosing record, because + -- Set up finalization data for enclosing record, because -- controlled subcomponents of the ancestor part will be -- attached to it. @@ -3559,7 +3559,7 @@ package body Exp_Aggr is end if; if Nkind (N) = N_Aggregate - and then Present (Component_Associations (N)) + and then Present (Component_Associations (N)) then Expr := First (Component_Associations (N)); while Present (Expr) loop @@ -3936,7 +3936,7 @@ package body Exp_Aggr is -- If the size is known, or all the components are static, try to -- build a fully positional aggregate. - -- The size of the type may not be known for an aggregate with + -- The size of the type may not be known for an aggregate with -- discriminated array components, but if the components are static -- it is still possible to verify statically that the length is -- compatible with the upper bound of the type, and therefore it is @@ -3980,7 +3980,7 @@ package body Exp_Aggr is else Error_Msg_N - ("non-static object requires elaboration code??", N); + ("non-static object requires elaboration code??", N); exit; end if; diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index aa3d19f27fa..6714894f637 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -4864,12 +4864,14 @@ package body Exp_Ch4 is return; end if; - -- If the case expression is a predicate specification, do not - -- expand, because it will be converted to the proper predicate - -- form when building the predicate function. + -- If the case expression is a predicate specification, and the type + -- to which it applies has a static predicate aspect, do not expand, + -- because it will be converted to the proper predicate form later. if Ekind_In (Current_Scope, E_Function, E_Procedure) and then Is_Predicate_Function (Current_Scope) + and then + Has_Static_Predicate_Aspect (Etype (First_Entity (Current_Scope))) then return; end if; diff --git a/gcc/ada/s-fatgen.adb b/gcc/ada/s-fatgen.adb index 57703f4ff6e..35d037ac388 100644 --- a/gcc/ada/s-fatgen.adb +++ b/gcc/ada/s-fatgen.adb @@ -744,7 +744,7 @@ package body System.Fat_Gen is else Result := Machine (Radix_To_M_Minus_1 + Result) - Radix_To_M_Minus_1; - if Result > abs X then + if Result > abs X then Result := Result - 1.0; end if; diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 9e436405e63..44d89f5edf8 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -401,7 +401,7 @@ package body Sem_Aggr is -- is set in Resolve_Array_Aggregate but the aggregate is not -- immediately replaced with a raise CE. In fact, Array_Aggr_Subtype must -- first construct the proper itype for the aggregate (Gigi needs - -- this). After constructing the proper itype we will eventually replace + -- this). After constructing the proper itype we will eventually replace -- the top-level aggregate with a raise CE (done in Resolve_Aggregate). -- Of course in cases such as: -- @@ -412,7 +412,7 @@ package body Sem_Aggr is -- (in this particular case the bounds will be 1 .. 2). procedure Make_String_Into_Aggregate (N : Node_Id); - -- A string literal can appear in a context in which a one dimensional + -- A string literal can appear in a context in which a one dimensional -- array of characters is expected. This procedure simply rewrites the -- string as an aggregate, prior to resolution. @@ -2718,7 +2718,7 @@ package body Sem_Aggr is if Etype (Imm_Type) = Base_Type (A_Type) then return True; - -- The base type of the parent type may appear as a private + -- The base type of the parent type may appear as a private -- extension if it is declared as such in a parent unit of the -- current one. For consistency of the subsequent analysis use -- the partial view for the ancestor part. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 7d52d2e44ae..bb4095b0df4 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -149,7 +149,7 @@ package body Sem_Ch12 is -- However, for private types, this by itself does not insure that the -- proper VIEW of the entity is used (the full type may be visible at the -- point of generic definition, but not at instantiation, or vice-versa). - -- In order to reference the proper view, we special-case any reference + -- In order to reference the proper view, we special-case any reference -- to private types in the generic object, by saving both views, one in -- the generic and one in the semantic copy. At time of instantiation, we -- check whether the two views are consistent, and exchange declarations if @@ -708,7 +708,7 @@ package body Sem_Ch12 is -- If the instantiation happens textually before the body of the generic, -- the instantiation of the body must be analyzed after the generic body, -- and not at the point of instantiation. Such early instantiations can - -- happen if the generic and the instance appear in a package declaration + -- happen if the generic and the instance appear in a package declaration -- because the generic body can only appear in the corresponding package -- body. Early instantiations can also appear if generic, instance and -- body are all in the declarative part of a subprogram or entry. Entities @@ -807,7 +807,7 @@ package body Sem_Ch12 is -- Within the generic part, entities in the formal package are -- visible. To validate subsequent type declarations, indicate -- the correspondence between the entities in the analyzed formal, - -- and the entities in the actual package. There are three packages + -- and the entities in the actual package. There are three packages -- involved in the instantiation of a formal package: the parent -- generic P1 which appears in the generic declaration, the fake -- instantiation P2 which appears in the analyzed generic, and whose @@ -1101,8 +1101,8 @@ package body Sem_Ch12 is -- include an Others clause. procedure Process_Default (F : Entity_Id); - -- Add a copy of the declaration of generic formal F to the list of - -- associations, and add an explicit box association for F if there + -- Add a copy of the declaration of generic formal F to the list of + -- associations, and add an explicit box association for F if there -- is none yet, and the default comes from an Others_Choice. function Renames_Standard_Subprogram (Subp : Entity_Id) return Boolean; @@ -1268,7 +1268,7 @@ package body Sem_Ch12 is -- insert actuals for those defaults, and cannot rely on their -- names to disambiguate them. - if Actual = First_Named then + if Actual = First_Named then Next (First_Named); elsif Present (Actual) then @@ -2883,7 +2883,7 @@ package body Sem_Ch12 is end if; -- Default name may be overloaded, in which case the interpretation - -- with the correct profile must be selected, as for a renaming. + -- with the correct profile must be selected, as for a renaming. -- If the definition is an indexed component, it must denote a -- member of an entry family. If it is a selected component, it -- can be a protected operation. @@ -4600,14 +4600,14 @@ package body Sem_Ch12 is Scope_Stack.Table (Scope_Stack.Last - J + 1).First_Use_Clause := Use_Clauses (J); Install_Use_Clauses (Use_Clauses (J)); - end loop; + end loop; else for J in reverse 1 .. Num_Scopes loop Scope_Stack.Table (Scope_Stack.Last - J + 1).First_Use_Clause := Use_Clauses (J); Install_Use_Clauses (Use_Clauses (J)); - end loop; + end loop; end if; -- Restore status of instances. If one of them is a body, make its @@ -5897,7 +5897,7 @@ package body Sem_Ch12 is and then not Comes_From_Source (E1) and then Chars (E1) /= Chars (E2) then - while Present (E1) and then Chars (E1) /= Chars (E2) loop + while Present (E1) and then Chars (E1) /= Chars (E2) loop Next_Entity (E1); end loop; end if; @@ -7695,14 +7695,14 @@ package body Sem_Ch12 is begin E1 := First_Entity (P); - while Present (E1) and then E1 /= Instance loop + while Present (E1) and then E1 /= Instance loop if Ekind (E1) = E_Package and then Nkind (Parent (E1)) = N_Package_Renaming_Declaration then if Renamed_Object (E1) = Pack then return True; - elsif E1 = P or else Renamed_Object (E1) = P then + elsif E1 = P or else Renamed_Object (E1) = P then return False; elsif Is_Actual_Of_Previous_Formal (E1) then @@ -8724,7 +8724,7 @@ package body Sem_Ch12 is if Scop = Par_I then null; - -- If the next node is a source body we must freeze in + -- If the next node is a source body we must freeze in -- the current scope as well. elsif Present (Next (N)) @@ -9472,7 +9472,7 @@ package body Sem_Ch12 is -- same order. function Get_Formal_Entity (N : Node_Id) return Entity_Id; - -- Retrieve entity of defining entity of generic formal parameter. + -- Retrieve entity of defining entity of generic formal parameter. -- Only the declarations of formals need to be considered when -- linking them to actuals, but the declarative list may include -- internal entities generated during analysis, and those are ignored. @@ -9571,7 +9571,7 @@ package body Sem_Ch12 is Actual := Entity (Name (Original_Node (Formal_Node))); - -- The actual in the formal package declaration may be a + -- The actual in the formal package declaration may be a -- renamed generic package, in which case we want to retrieve -- the original generic in order to traverse its formal part. @@ -9710,7 +9710,7 @@ package body Sem_Ch12 is Analyze (Actual); if not Is_Entity_Name (Actual) - or else Ekind (Entity (Actual)) /= E_Package + or else Ekind (Entity (Actual)) /= E_Package then Error_Msg_N ("expect package instance to instantiate formal", Actual); @@ -12259,7 +12259,7 @@ package body Sem_Ch12 is end if; -- Verify that limitedness matches. If parent is a limited - -- interface then the generic formal is not unless declared + -- interface then the generic formal is not unless declared -- explicitly so. If not declared limited, the actual cannot be -- limited (see AI05-0087). diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index ae02bdd00ea..2797c6309e5 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1208,39 +1208,28 @@ package body Sem_Ch13 is procedure Decorate (Asp : Node_Id; Prag : Node_Id); -- Establish linkages between an aspect and its corresponding pragma - procedure Insert_After_SPARK_Mode - (Prag : Node_Id; - Ins_Nod : Node_Id; - Decls : List_Id); + procedure Insert_Pragma + (Prag : Node_Id; + Is_Instance : Boolean := False); -- Subsidiary to the analysis of aspects -- Abstract_State - -- Ghost - -- Initializes - -- Initial_Condition - -- Refined_State - -- Insert node Prag before node Ins_Nod. If Ins_Nod is for pragma - -- SPARK_Mode, then skip SPARK_Mode. Decls is the associated declarative - -- list where Prag is to reside. - - procedure Insert_Pragma (Prag : Node_Id); - -- Subsidiary to the analysis of aspects -- Attach_Handler -- Contract_Cases -- Depends + -- Ghost -- Global + -- Initial_Condition + -- Initializes -- Post -- Pre -- Refined_Depends -- Refined_Global + -- Refined_State -- SPARK_Mode -- Warnings -- Insert pragma Prag such that it mimics the placement of a source - -- pragma of the same kind. - -- - -- procedure Proc (Formal : ...) with Global => ...; - -- - -- procedure Proc (Formal : ...); - -- pragma Global (...); + -- pragma of the same kind. Flag Is_Generic should be set when the + -- context denotes a generic instance. -------------- -- Decorate -- @@ -1254,42 +1243,14 @@ package body Sem_Ch13 is Set_Parent (Prag, Asp); end Decorate; - ----------------------------- - -- Insert_After_SPARK_Mode -- - ----------------------------- - - procedure Insert_After_SPARK_Mode - (Prag : Node_Id; - Ins_Nod : Node_Id; - Decls : List_Id) - is - Decl : Node_Id := Ins_Nod; - - begin - -- Skip SPARK_Mode - - if Present (Decl) - and then Nkind (Decl) = N_Pragma - and then Pragma_Name (Decl) = Name_SPARK_Mode - then - Decl := Next (Decl); - end if; - - if Present (Decl) then - Insert_Before (Decl, Prag); - - -- Aitem acts as the last declaration - - else - Append_To (Decls, Prag); - end if; - end Insert_After_SPARK_Mode; - ------------------- -- Insert_Pragma -- ------------------- - procedure Insert_Pragma (Prag : Node_Id) is + procedure Insert_Pragma + (Prag : Node_Id; + Is_Instance : Boolean := False) + is Aux : Node_Id; Decl : Node_Id; Decls : List_Id; @@ -1365,7 +1326,39 @@ package body Sem_Ch13 is Set_Visible_Declarations (Specification (N), Decls); end if; - Prepend_To (Decls, Prag); + -- The visible declarations of a generic instance have the + -- following structure: + + -- + -- + -- + + -- Insert the pragma before the first source declaration by + -- skipping the instance "header". + + if Is_Instance then + Decl := First (Decls); + while Present (Decl) and then not Comes_From_Source (Decl) loop + Decl := Next (Decl); + end loop; + + -- The instance "header" is followed by at least one source + -- declaration. + + if Present (Decl) then + Insert_Before (Decl, Prag); + + -- Otherwise the pragma is placed after the instance "header" + + else + Append_To (Decls, Prag); + end if; + + -- Otherwise this is not a generic instance + + else + Prepend_To (Decls, Prag); + end if; -- When the aspect is associated with a protected unit declaration, -- insert the generated pragma at the top of the visible declarations @@ -2298,8 +2291,6 @@ package body Sem_Ch13 is when Aspect_Abstract_State => Abstract_State : declare Context : Node_Id := N; - Decl : Node_Id; - Decls : List_Id; begin -- When aspect Abstract_State appears on a generic package, @@ -2318,54 +2309,12 @@ package body Sem_Ch13 is Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Abstract_State); - Decorate (Aspect, Aitem); - - Decls := Visible_Declarations (Specification (Context)); - -- In general pragma Abstract_State must be at the top - -- of the existing visible declarations to emulate its - -- source counterpart. The only exception to this is a - -- generic instance in which case the pragma must be - -- inserted after the association renamings. - - if Present (Decls) then - Decl := First (Decls); - - -- The visible declarations of a generic instance have - -- the following structure: - - -- - -- - -- - - -- The pragma must be inserted before the first source - -- declaration, skip the instance "header". - - if Is_Generic_Instance (Defining_Entity (Context)) then - while Present (Decl) - and then not Comes_From_Source (Decl) - loop - Decl := Next (Decl); - end loop; - end if; - - -- When aspects Abstract_State, Ghost, - -- Initial_Condition and Initializes are out of order, - -- ensure that pragma SPARK_Mode is always at the top - -- of the declarations to properly enabled/suppress - -- errors. - - Insert_After_SPARK_Mode - (Prag => Aitem, - Ins_Nod => Decl, - Decls => Decls); - - -- Otherwise the pragma forms a new declarative list - - else - Set_Visible_Declarations - (Specification (Context), New_List (Aitem)); - end if; + Decorate (Aspect, Aitem); + Insert_Pragma + (Prag => Aitem, + Is_Instance => + Is_Generic_Instance (Defining_Entity (Context))); else Error_Msg_NE @@ -2526,10 +2475,7 @@ package body Sem_Ch13 is -- declarations or after an object, a [generic] subprogram, or -- a type declaration. - when Aspect_Ghost => Ghost : declare - Decls : List_Id; - - begin + when Aspect_Ghost => Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, @@ -2537,40 +2483,8 @@ package body Sem_Ch13 is Pragma_Name => Name_Ghost); Decorate (Aspect, Aitem); - - -- When the aspect applies to a [generic] package, insert - -- the pragma at the top of the visible declarations. This - -- emulates the placement of a source pragma. - - if Nkind_In (N, N_Generic_Package_Declaration, - N_Package_Declaration) - then - Decls := Visible_Declarations (Specification (N)); - - if No (Decls) then - Decls := New_List; - Set_Visible_Declarations (N, Decls); - end if; - - -- When aspects Abstract_State, Ghost, Initial_Condition - -- and Initializes are out of order, ensure that pragma - -- SPARK_Mode is always at the top of the declarations to - -- properly enabled/suppress errors. - - Insert_After_SPARK_Mode - (Prag => Aitem, - Ins_Nod => First (Decls), - Decls => Decls); - - -- Otherwise the context is an object, [generic] subprogram - -- or type declaration. - - else - Insert_Pragma (Aitem); - end if; - + Insert_Pragma (Aitem); goto Continue; - end Ghost; -- Global @@ -2604,7 +2518,6 @@ package body Sem_Ch13 is when Aspect_Initial_Condition => Initial_Condition : declare Context : Node_Id := N; - Decls : List_Id; begin -- When aspect Initial_Condition appears on a generic @@ -2618,30 +2531,20 @@ package body Sem_Ch13 is if Nkind_In (Context, N_Generic_Package_Declaration, N_Package_Declaration) then - Decls := Visible_Declarations (Specification (Context)); - Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Initial_Condition); - Decorate (Aspect, Aitem); - - if No (Decls) then - Decls := New_List; - Set_Visible_Declarations (Context, Decls); - end if; - -- When aspects Abstract_State, Ghost, Initial_Condition - -- and Initializes are out of order, ensure that pragma - -- SPARK_Mode is always at the top of the declarations to - -- properly enabled/suppress errors. + Decorate (Aspect, Aitem); + Insert_Pragma + (Prag => Aitem, + Is_Instance => + Is_Generic_Instance (Defining_Entity (Context))); - Insert_After_SPARK_Mode - (Prag => Aitem, - Ins_Nod => First (Decls), - Decls => Decls); + -- Otherwise the context is illegal else Error_Msg_NE @@ -2663,7 +2566,6 @@ package body Sem_Ch13 is when Aspect_Initializes => Initializes : declare Context : Node_Id := N; - Decls : List_Id; begin -- When aspect Initializes appears on a generic package, @@ -2677,29 +2579,19 @@ package body Sem_Ch13 is if Nkind_In (Context, N_Generic_Package_Declaration, N_Package_Declaration) then - Decls := Visible_Declarations (Specification (Context)); - Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Initializes); - Decorate (Aspect, Aitem); - - if No (Decls) then - Decls := New_List; - Set_Visible_Declarations (Context, Decls); - end if; - -- When aspects Abstract_State, Ghost, Initial_Condition - -- and Initializes are out of order, ensure that pragma - -- SPARK_Mode is always at the top of the declarations to - -- properly enabled/suppress errors. + Decorate (Aspect, Aitem); + Insert_Pragma + (Prag => Aitem, + Is_Instance => + Is_Generic_Instance (Defining_Entity (Context))); - Insert_After_SPARK_Mode - (Prag => Aitem, - Ins_Nod => First (Decls), - Decls => Decls); + -- Otherwise the context is illegal else Error_Msg_NE @@ -2813,39 +2705,24 @@ package body Sem_Ch13 is -- Refined_State - when Aspect_Refined_State => Refined_State : declare - Decls : List_Id; + when Aspect_Refined_State => - begin -- The corresponding pragma for Refined_State is inserted in -- the declarations of the related package body. This action -- synchronizes both the source and from-aspect versions of -- the pragma. if Nkind (N) = N_Package_Body then - Decls := Declarations (N); - Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Refined_State); - Decorate (Aspect, Aitem); - - if No (Decls) then - Decls := New_List; - Set_Declarations (N, Decls); - end if; - -- Pragma Refined_State must be inserted after pragma - -- SPARK_Mode in the tree. This ensures that any error - -- messages dependent on SPARK_Mode will be properly - -- enabled/suppressed. + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); - Insert_After_SPARK_Mode - (Prag => Aitem, - Ins_Nod => First (Decls), - Decls => Decls); + -- Otherwise the context is illegal else Error_Msg_NE @@ -2853,7 +2730,6 @@ package body Sem_Ch13 is end if; goto Continue; - end Refined_State; -- Relative_Deadline diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index b01640d3dcf..9928c3b0cfb 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -1802,7 +1802,7 @@ package body Sem_Ch4 is -- call to a user-defined equality operator. -- For the predefined case, the result is Boolean, regardless of the - -- type of the operands. The operands may even be limited, if they are + -- type of the operands. The operands may even be limited, if they are -- generic actuals. If they are overloaded, label the left argument with -- the common type that must be present, or with the type of the formal -- of the user-defined function. @@ -3196,7 +3196,7 @@ package body Sem_Ch4 is -- Try_Indexed_Call and there is nothing else to do. if Is_Indexed - and then Nkind (N) = N_Slice + and then Nkind (N) = N_Slice then return; end if; @@ -5422,7 +5422,7 @@ package body Sem_Ch4 is -- and no further processing is required (this is the case of an -- operator constructed by Exp_Fixd for a fixed point operation) -- Otherwise add one interpretation with universal fixed result - -- If the operator is given in functional notation, it comes + -- If the operator is given in functional notation, it comes -- from source and Fixed_As_Integer cannot apply. if (Nkind (N) not in N_Op diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index e488ee77808..bf39088d6e1 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -107,7 +107,7 @@ package body Sem_Ch8 is -- Open scopes, that is to say scopes currently being compiled, have their -- corresponding rows of entities in order, innermost scope first. - -- The scopes of packages that are mentioned in context clauses appear in + -- The scopes of packages that are mentioned in context clauses appear in -- no particular order, interspersed among open scopes. This is because -- in the course of analyzing the context of a compilation, a package -- declaration is first an open scope, and subsequently an element of the @@ -191,7 +191,7 @@ package body Sem_Ch8 is -- removed from visibility chains on exit from the corresponding scope. -- From the outside, these entities are always accessed by selected -- notation, and the entity chain for the record type, protected type, - -- etc. is traversed sequentially in order to find the designated entity. + -- etc. is traversed sequentially in order to find the designated entity. -- The discriminants of a type and the operations of a protected type or -- task are unchained on exit from the first view of the type, (such as @@ -224,7 +224,7 @@ package body Sem_Ch8 is -- The Rtsfind mechanism can force a call to Semantics while another -- compilation is in progress. The unit retrieved by Rtsfind must be - -- compiled in its own context, and has no access to the visibility of + -- compiled in its own context, and has no access to the visibility of -- the unit currently being compiled. The procedures Save_Scope_Stack and -- Restore_Scope_Stack make entities in current open scopes invisible -- before compiling the retrieved unit, and restore the compilation diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index 28acbf06b4c..c4fe7687626 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -814,7 +814,7 @@ package body Sem_Eval is V := UI_Negate (Intval (Right_Opnd (N))); return; - elsif Nkind (N) = N_Attribute_Reference then + elsif Nkind (N) = N_Attribute_Reference then if Attribute_Name (N) = Name_Succ then R := First (Expressions (N)); V := Uint_1; @@ -2909,7 +2909,7 @@ package body Sem_Eval is -- Eval_Op_Not -- ----------------- - -- The not operation is a static functions, so the result is potentially + -- The not operation is a static functions, so the result is potentially -- static if the operand is potentially static (RM 4.9(7), 4.9(20)). procedure Eval_Op_Not (N : Node_Id) is diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index ca66fe2d906..b3e90b592e7 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2760,6 +2760,10 @@ package body Sem_Prag is -- is the entity of the related subprogram. Subp_Decl is the declaration -- of the related subprogram. Sets flag Legal when the pragma is legal. + procedure Analyze_If_Present (Id : Pragma_Id); + -- Inspect the remainder of the list containing pragma N and look for + -- a pragma that matches Id. If found, analyze the pragma. + procedure Analyze_Part_Of (Item_Id : Entity_Id; State : Node_Id; @@ -2888,11 +2892,6 @@ package body Sem_Prag is -- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part -- should be set when Comp comes from a record variant. - procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id); - -- Subsidiary routine to the analysis of pragmas Abstract_State, - -- Initial_Condition and Initializes. Determine whether pragma First - -- appears before pragma Second. If this is not the case, emit an error. - procedure Check_Duplicate_Pragma (E : Entity_Id); -- Check if a rep item of the same name as the current pragma is already -- chained as a rep pragma to the given entity. If so give a message @@ -3125,10 +3124,6 @@ package body Sem_Prag is -- Determines if the placement of the current pragma is appropriate -- for a configuration pragma. - function Is_Followed_By_Pragma (Prag_Nam : Name_Id) return Boolean; - -- Determine whether pragma N is followed by another pragma denoted by - -- its name Prag_Nam. It is assumed that N is a list member. - function Is_In_Context_Clause return Boolean; -- Returns True if pragma appears within the context clause of a unit, -- and False for any other placement (does not generate any messages). @@ -3349,11 +3344,6 @@ package body Sem_Prag is Subp_Decl := Empty; Legal := False; - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_Arg_Count (1); @@ -3404,6 +3394,37 @@ package body Sem_Prag is Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); end Analyze_Depends_Global; + ------------------------ + -- Analyze_If_Present -- + ------------------------ + + procedure Analyze_If_Present (Id : Pragma_Id) is + Stmt : Node_Id; + + begin + pragma Assert (Is_List_Member (N)); + + -- Inspect the declarations or statements following pragma N looking + -- for another pragma whose Id matches the caller's request. If it is + -- available, analyze it. + + Stmt := Next (N); + while Present (Stmt) loop + if Nkind (Stmt) = N_Pragma and then Get_Pragma_Id (Stmt) = Id then + Analyze_Pragma (Stmt); + exit; + + -- The first source declaration or statement immediately following + -- N ends the region where a pragma may appear. + + elsif Comes_From_Source (Stmt) then + exit; + end if; + + Next (Stmt); + end loop; + end Analyze_If_Present; + --------------------- -- Analyze_Part_Of -- --------------------- @@ -3603,11 +3624,6 @@ package body Sem_Prag is -- Post_Class. begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - -- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to -- offer uniformity among the various kinds of pre/postconditions by -- rewriting the pragma identifier. This allows the retrieval of the @@ -3733,6 +3749,11 @@ package body Sem_Prag is Subp_Id := Defining_Entity (Subp_Decl); + -- Chain the pragma on the contract for further processing by + -- Analyze_Pre_Post_Condition_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -3744,13 +3765,14 @@ package body Sem_Prag is if Nkind_In (Subp_Decl, N_Subprogram_Body, N_Subprogram_Body_Stub) then + -- The legality checks of pragmas Precondition and Postcondition + -- are affected by the SPARK mode in effect and the volatility of + -- the context. Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); Analyze_Pre_Post_Condition_In_Decl_Part (N); end if; - - -- Chain the pragma on the contract for further processing by - -- Analyze_Pre_Post_Condition_In_Decl_Part. - - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Analyze_Pre_Post_Condition; ----------------------------------------- @@ -3772,11 +3794,6 @@ package body Sem_Prag is Body_Id := Empty; Legal := False; - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_Arg_Count (1); Check_No_Identifiers; @@ -4331,107 +4348,6 @@ package body Sem_Prag is end if; end Check_Component; - ----------------------------- - -- Check_Declaration_Order -- - ----------------------------- - - procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is - procedure Check_Aspect_Specification_Order; - -- Inspect the aspect specifications of the context to determine the - -- proper order. - - -------------------------------------- - -- Check_Aspect_Specification_Order -- - -------------------------------------- - - procedure Check_Aspect_Specification_Order is - Asp_First : constant Node_Id := Corresponding_Aspect (First); - Asp_Second : constant Node_Id := Corresponding_Aspect (Second); - Asp : Node_Id; - - begin - -- Both aspects must be part of the same aspect specification list - - pragma Assert - (List_Containing (Asp_First) = List_Containing (Asp_Second)); - - -- Try to reach Second starting from First in a left to right - -- traversal of the aspect specifications. - - Asp := Next (Asp_First); - while Present (Asp) loop - - -- The order is ok, First is followed by Second - - if Asp = Asp_Second then - return; - end if; - - Next (Asp); - end loop; - - -- If we get here, then the aspects are out of order - - SPARK_Msg_N ("aspect % cannot come after aspect %", First); - end Check_Aspect_Specification_Order; - - -- Local variables - - Stmt : Node_Id; - - -- Start of processing for Check_Declaration_Order - - begin - -- Cannot check the order if one of the pragmas is missing - - if No (First) or else No (Second) then - return; - end if; - - -- Set up the error names in case the order is incorrect - - Error_Msg_Name_1 := Pragma_Name (First); - Error_Msg_Name_2 := Pragma_Name (Second); - - if From_Aspect_Specification (First) then - - -- Both pragmas are actually aspects, check their declaration - -- order in the associated aspect specification list. Otherwise - -- First is an aspect and Second a source pragma. - - if From_Aspect_Specification (Second) then - Check_Aspect_Specification_Order; - end if; - - -- Abstract_States is a source pragma - - else - if From_Aspect_Specification (Second) then - SPARK_Msg_N ("pragma % cannot come after aspect %", First); - - -- Both pragmas are source constructs. Try to reach First from - -- Second by traversing the declarations backwards. - - else - Stmt := Prev (Second); - while Present (Stmt) loop - - -- The order is ok, First is followed by Second - - if Stmt = First then - return; - end if; - - Prev (Stmt); - end loop; - - -- If we get here, then the pragmas are out of order - - SPARK_Msg_N ("pragma % cannot come after pragma %", First); - end if; - end if; - end Check_Declaration_Order; - ---------------------------- -- Check_Duplicate_Pragma -- ---------------------------- @@ -5890,39 +5806,6 @@ package body Sem_Prag is end if; end Is_Configuration_Pragma; - --------------------------- - -- Is_Followed_By_Pragma -- - --------------------------- - - function Is_Followed_By_Pragma (Prag_Nam : Name_Id) return Boolean is - Stmt : Node_Id; - - begin - pragma Assert (Is_List_Member (N)); - - -- Inspect the declarations or statements following pragma N looking - -- for another pragma whose name matches the caller's request. - - Stmt := Next (N); - while Present (Stmt) loop - if Nkind (Stmt) = N_Pragma - and then Pragma_Name (Stmt) = Prag_Nam - then - return True; - - -- The first source declaration or statement immediately following - -- N ends the region where a pragma may appear. - - elsif Comes_From_Source (Stmt) then - exit; - end if; - - Next (Stmt); - end loop; - - return False; - end Is_Followed_By_Pragma; - -------------------------- -- Is_In_Context_Clause -- -------------------------- @@ -10416,6 +10299,22 @@ package body Sem_Prag is Pack_Id := Defining_Entity (Pack_Decl); + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Pack_Id); + + -- The legality checks of pragmas Abstract_State, Initializes, and + -- Initial_Condition are affected by the SPARK mode in effect. In + -- addition, these three pragmas are subject to an inherent order: + + -- 1) Abstract_State + -- 2) Initializes + -- 3) Initial_Condition + + -- Analyze all these pragmas in the order outlined above + + Analyze_If_Present (Pragma_SPARK_Mode); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -10452,16 +10351,8 @@ package body Sem_Prag is Analyze_Abstract_State (States, Pack_Id); end if; - -- Verify the declaration order of pragmas Abstract_State and - -- Initializes. - - Check_Declaration_Order - (First => N, - Second => Get_Pragma (Pack_Id, Pragma_Initializes)); - - -- Chain the pragma on the contract for completeness - - Add_Contract_Item (N, Pack_Id); + Analyze_If_Present (Pragma_Initializes); + Analyze_If_Present (Pragma_Initial_Condition); end Abstract_State; ------------ @@ -11001,7 +10892,7 @@ package body Sem_Prag is -- POLICY_IDENTIFIER ::= Check | Disable | Ignore -- Note: Check and Ignore are language-defined. Disable is a GNAT - -- implementation defined addition that results in totally ignoring + -- implementation-defined addition that results in totally ignoring -- the corresponding assertion. If Disable is specified, then the -- argument of the assertion is not even analyzed. This is useful -- when the aspect/pragma argument references entities in a with'ed @@ -11213,11 +11104,6 @@ package body Sem_Prag is Obj_Id : Entity_Id; begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_No_Identifiers; Check_At_Most_N_Arguments (1); @@ -11244,6 +11130,11 @@ package body Sem_Prag is if Ekind (Obj_Id) = E_Variable then + -- Chain the pragma on the contract for further processing by + -- Analyze_External_Property_In_Decl_Part. + + Add_Contract_Item (N, Obj_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for -- the purposes of legality checks and removal of ignored Ghost -- code. @@ -11256,11 +11147,6 @@ package body Sem_Prag is Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); end if; - -- Chain the pragma on the contract for further processing by - -- Analyze_External_Property_In_Decl_Part. - - Add_Contract_Item (N, Obj_Id); - -- Otherwise the external property applies to a constant else @@ -12290,11 +12176,6 @@ package body Sem_Prag is Obj_Id := Defining_Entity (Obj_Decl); - -- A pragma that applies to a Ghost entity becomes Ghost for the - -- purposes of legality checks and removal of ignored Ghost code. - - Mark_Pragma_As_Ghost (N, Obj_Id); - -- The object declaration must be a library-level variable with -- an initialization expression. The expression must depend on -- a variable, parameter, or another constant_after_elaboration, @@ -12320,15 +12201,20 @@ package body Sem_Prag is return; end if; + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Obj_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Obj_Id); + -- Analyze the Boolean expression (if any) if Present (Arg1) then Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); end if; - - -- Chain the pragma on the contract for completeness - - Add_Contract_Item (N, Obj_Id); end Constant_After_Elaboration; -------------------- @@ -12384,11 +12270,6 @@ package body Sem_Prag is Check_No_Identifiers; Check_Arg_Count (1); - -- The pragma is analyzed at the end of the declarative part which - -- contains the related subprogram. Reset the analyzed flag. - - Set_Analyzed (N, False); - -- Ensure the proper placement of the pragma. Contract_Cases must -- be associated with a subprogram declaration or a body that acts -- as a spec. @@ -12427,6 +12308,11 @@ package body Sem_Prag is Spec_Id := Unique_Defining_Entity (Subp_Decl); + -- Chain the pragma on the contract for further processing by + -- Analyze_Contract_Cases_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -12439,13 +12325,14 @@ package body Sem_Prag is if Nkind_In (Subp_Decl, N_Subprogram_Body, N_Subprogram_Body_Stub) then + -- The legality checks of pragma Contract_Cases are affected by + -- the SPARK mode in effect and the volatility of the context. + -- Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); Analyze_Contract_Cases_In_Decl_Part (N); end if; - - -- Chain the pragma on the contract for further processing by - -- Analyze_Contract_Cases_In_Decl_Part. - - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Contract_Cases; ---------------- @@ -13145,7 +13032,6 @@ package body Sem_Prag is -- the annotation must instantiate itself. when Pragma_Depends => Depends : declare - Global : Node_Id; Legal : Boolean; Spec_Id : Entity_Id; Subp_Decl : Node_Id; @@ -13166,34 +13052,20 @@ package body Sem_Prag is if Nkind_In (Subp_Decl, N_Subprogram_Body, N_Subprogram_Body_Stub) then - -- Pragmas Global and Depends must be analyzed in a specific - -- order, as the latter depends on the former. When the two - -- pragmas appear out of order, their analyis is triggered - -- by pragma Global. - - -- pragma Depends ...; - -- pragma Global ...; - - -- Wait until pragma Global is encountered - - if Is_Followed_By_Pragma (Name_Global) then - null; + -- The legality checks of pragmas Depends and Global are + -- affected by the SPARK mode in effect and the volatility + -- of the context. In addition these two pragmas are subject + -- to an inherent order: - -- Otherwise pragma Depends is the last of the pair. Analyze - -- both pragmas when they appear in order. + -- 1) Global + -- 2) Depends - -- pragma Global ...; - -- pragma Depends ...; + -- Analyze all these pragmas in the order outlined above - else - Global := Get_Pragma (Spec_Id, Pragma_Global); - - if Present (Global) then - Analyze_Global_In_Decl_Part (Global); - end if; - - Analyze_Depends_In_Decl_Part (N); - end if; + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_If_Present (Pragma_Global); + Analyze_Depends_In_Decl_Part (N); end if; end if; end Depends; @@ -14154,12 +14026,21 @@ package body Sem_Prag is return; end if; - Spec_Id := Unique_Defining_Entity (Subp_Decl); + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + + -- The legality checks of pragma Extension_Visible are affected + -- by the SPARK mode in effect. Analyze all pragmas in specific + -- order. + + Analyze_If_Present (Pragma_SPARK_Mode); -- Mark the pragma as Ghost if the related subprogram is also -- Ghost. This also ensures that any expansion performed further -- below will produce Ghost nodes. + Spec_Id := Unique_Defining_Entity (Subp_Decl); Mark_Pragma_As_Ghost (N, Spec_Id); -- Examine the formals of the related subprogram @@ -14205,10 +14086,6 @@ package body Sem_Prag is Check_Static_Boolean_Expression (Expression (Get_Argument (N, Spec_Id))); end if; - - -- Chain the pragma on the contract for completeness - - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Extensions_Visible; -------------- @@ -14673,7 +14550,6 @@ package body Sem_Prag is -- the annotation must instantiate itself. when Pragma_Global => Global : declare - Depends : Node_Id; Legal : Boolean; Spec_Id : Entity_Id; Subp_Decl : Node_Id; @@ -14694,34 +14570,20 @@ package body Sem_Prag is if Nkind_In (Subp_Decl, N_Subprogram_Body, N_Subprogram_Body_Stub) then - -- Pragmas Global and Depends must be analyzed in a specific - -- order, as the latter depends on the former. When the two - -- pragmas appear in order, their analysis is triggered by - -- pragma Depends. + -- The legality checks of pragmas Depends and Global are + -- affected by the SPARK mode in effect and the volatility + -- of the context. In addition these two pragmas are subject + -- to an inherent order: - -- pragma Global ...; - -- pragma Depends ...; + -- 1) Global + -- 2) Depends - -- Wait until pragma Global is encountered + -- Analyze all these pragmas in the order outlined above - if Is_Followed_By_Pragma (Name_Depends) then - null; - - -- Otherwise pragma Global is the last of the pair. Analyze - -- both pragmas when they are out of order. - - -- pragma Depends ...; - -- pragma Global ...; - - else - Analyze_Global_In_Decl_Part (N); - - Depends := Get_Pragma (Spec_Id, Pragma_Depends); - - if Present (Depends) then - Analyze_Depends_In_Decl_Part (Depends); - end if; - end if; + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_Global_In_Decl_Part (N); + Analyze_If_Present (Pragma_Depends); end if; end if; end Global; @@ -15315,11 +15177,6 @@ package body Sem_Prag is Pack_Id : Entity_Id; begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); @@ -15341,36 +15198,31 @@ package body Sem_Prag is return; end if; - -- The pragma must be analyzed at the end of the visible - -- declarations of the related package. Save the pragma for later - -- (see Analyze_Initial_Condition_In_Decl_Part) by adding it to - -- the contract of the package. - Pack_Id := Defining_Entity (Pack_Decl); - -- A pragma that applies to a Ghost entity becomes Ghost for the - -- purposes of legality checks and removal of ignored Ghost code. + -- Chain the pragma on the contract for further processing by + -- Analyze_Initial_Condition_In_Decl_Part. - Mark_Pragma_As_Ghost (N, Pack_Id); + Add_Contract_Item (N, Pack_Id); - -- Verify the declaration order of pragma Initial_Condition with - -- respect to pragmas Abstract_State and Initializes when SPARK - -- checks are enabled. + -- The legality checks of pragmas Abstract_State, Initializes, and + -- Initial_Condition are affected by the SPARK mode in effect. In + -- addition, these three pragmas are subject to an inherent order: - if SPARK_Mode /= Off then - Check_Declaration_Order - (First => Get_Pragma (Pack_Id, Pragma_Abstract_State), - Second => N); + -- 1) Abstract_State + -- 2) Initializes + -- 3) Initial_Condition - Check_Declaration_Order - (First => Get_Pragma (Pack_Id, Pragma_Initializes), - Second => N); - end if; + -- Analyze all these pragmas in the order outlined above - -- Chain the pragma on the contract for further processing by - -- Analyze_Initial_Condition_In_Decl_Part. + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Abstract_State); + Analyze_If_Present (Pragma_Initializes); - Add_Contract_Item (N, Pack_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Pack_Id); end Initial_Condition; ------------------------ @@ -15441,11 +15293,6 @@ package body Sem_Prag is Pack_Id : Entity_Id; begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); @@ -15469,25 +15316,31 @@ package body Sem_Prag is Pack_Id := Defining_Entity (Pack_Decl); + -- Chain the pragma on the contract for further processing by + -- Analyze_Initializes_In_Decl_Part. + + Add_Contract_Item (N, Pack_Id); + + -- The legality checks of pragmas Abstract_State, Initializes, and + -- Initial_Condition are affected by the SPARK mode in effect. In + -- addition, these three pragmas are subject to an inherent order: + + -- 1) Abstract_State + -- 2) Initializes + -- 3) Initial_Condition + + -- Analyze all these pragmas in the order outlined above + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Abstract_State); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. Mark_Pragma_As_Ghost (N, Pack_Id); Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); - -- Verify the declaration order of pragmas Abstract_State and - -- Initializes when SPARK checks are enabled. - - if SPARK_Mode /= Off then - Check_Declaration_Order - (First => Get_Pragma (Pack_Id, Pragma_Abstract_State), - Second => N); - end if; - - -- Chain the pragma on the contract for further processing by - -- Analyze_Initializes_In_Decl_Part. - - Add_Contract_Item (N, Pack_Id); + Analyze_If_Present (Pragma_Initial_Condition); end Initializes; ------------ @@ -17760,11 +17613,17 @@ package body Sem_Prag is Legal => Legal); if Legal then - State_Id := Entity (State); + + -- Add the pragma to the contract of the item. This aids with + -- the detection of a missing but required Part_Of indicator. + + Add_Contract_Item (N, Item_Id); -- The Part_Of indicator turns an object into a constituent of -- the encapsulating state. + State_Id := Entity (State); + if Ekind_In (Item_Id, E_Constant, E_Variable) then Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); Set_Encapsulating_State (Item_Id, State_Id); @@ -17778,11 +17637,6 @@ package body Sem_Prag is State_Id => State_Id, Instance => Stmt); end if; - - -- Add the pragma to the contract of the item. This aids with - -- the detection of a missing but required Part_Of indicator. - - Add_Contract_Item (N, Item_Id); end if; end Part_Of; @@ -18974,10 +18828,9 @@ package body Sem_Prag is -- the related generic subprogram body is instantiated. when Pragma_Refined_Depends => Refined_Depends : declare - Body_Id : Entity_Id; - Legal : Boolean; - Ref_Global : Node_Id; - Spec_Id : Entity_Id; + Body_Id : Entity_Id; + Legal : Boolean; + Spec_Id : Entity_Id; begin Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal); @@ -18989,34 +18842,20 @@ package body Sem_Prag is Add_Contract_Item (N, Body_Id); - -- Pragmas Refined_Global and Refined_Depends must be analyzed - -- in a specific order, as the latter depends on the former. - -- When the two pragmas appear out of order, their analysis is - -- triggered by pragma Refined_Global. + -- The legality checks of pragmas Refined_Depends and + -- Refined_Global are affected by the SPARK mode in effect and + -- the volatility of the context. In addition these two pragmas + -- are subject to an inherent order: - -- pragma Refined_Depends ...; - -- pragma Refined_Global ...; + -- 1) Refined_Global + -- 2) Refined_Depends - -- Wait until pragma Refined_Global is enountered + -- Analyze all these pragmas in the order outlined above - if Is_Followed_By_Pragma (Name_Refined_Global) then - null; - - -- Otherwise pragma Refined_Depends is the last of the pair. - -- Analyze both pragmas when they appear in order. - - -- pragma Refined_Global ...; - -- pragma Refined_Depends ...; - - else - Ref_Global := Get_Pragma (Body_Id, Pragma_Refined_Global); - - if Present (Ref_Global) then - Analyze_Refined_Global_In_Decl_Part (Ref_Global); - end if; - - Analyze_Refined_Depends_In_Decl_Part (N); - end if; + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_If_Present (Pragma_Refined_Global); + Analyze_Refined_Depends_In_Decl_Part (N); end if; end Refined_Depends; @@ -19057,10 +18896,9 @@ package body Sem_Prag is -- the related generic subprogram body is instantiated. when Pragma_Refined_Global => Refined_Global : declare - Body_Id : Entity_Id; - Legal : Boolean; - Ref_Depends : Node_Id; - Spec_Id : Entity_Id; + Body_Id : Entity_Id; + Legal : Boolean; + Spec_Id : Entity_Id; begin Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal); @@ -19072,34 +18910,20 @@ package body Sem_Prag is Add_Contract_Item (N, Body_Id); - -- Pragmas Refined_Global and Refined_Depends must be analyzed - -- in a specific order, as the latter depends on the former. - -- When the two pragmas are in order, their analysis must be - -- triggered by pragma Refined_Depends. - - -- pragma Refined_Global ...; - -- pragma Refined_Depends ...; - - -- Wait until pragma Refined_Depends is encountered + -- The legality checks of pragmas Refined_Depends and + -- Refined_Global are affected by the SPARK mode in effect and + -- the volatility of the context. In addition these two pragmas + -- are subject to an inherent order: - if Is_Followed_By_Pragma (Name_Refined_Depends) then - null; - - -- Otherwise pragma Refined_Global is the last of the pair. - -- Analyze both pragmas when they are out of order. + -- 1) Refined_Global + -- 2) Refined_Depends - -- pragma Refined_Depends ...; - -- pragma Refined_Global ...; + -- Analyze all these pragmas in the order outlined above - else - Analyze_Refined_Global_In_Decl_Part (N); - - Ref_Depends := Get_Pragma (Body_Id, Pragma_Refined_Depends); - - if Present (Ref_Depends) then - Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); - end if; - end if; + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_Refined_Global_In_Decl_Part (N); + Analyze_If_Present (Pragma_Refined_Depends); end if; end Refined_Global; @@ -19140,16 +18964,23 @@ package body Sem_Prag is -- body because it cannot benefit from forward references. if Legal then + + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Body_Id); + + -- The legality checks of pragma Refined_Post are affected by + -- the SPARK mode in effect and the volatility of the context. + -- Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); Analyze_Pre_Post_Condition_In_Decl_Part (N); -- Currently it is not possible to inline pre/postconditions on -- a subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - - -- Chain the pragma on the contract for completeness - - Add_Contract_Item (N, Body_Id); end if; end Refined_Post; @@ -19196,11 +19027,6 @@ package body Sem_Prag is Spec_Id : Entity_Id; begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); @@ -19222,6 +19048,16 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec (Pack_Decl); + -- Chain the pragma on the contract for further processing by + -- Analyze_Refined_State_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Pack_Decl)); + + -- The legality checks of pragma Refined_State are affected by the + -- SPARK mode in effect. Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -19241,11 +19077,6 @@ package body Sem_Prag is & "states", N, Spec_Id); return; end if; - - -- Chain the pragma on the contract for further processing by - -- Analyze_Refined_State_In_Decl_Part. - - Add_Contract_Item (N, Defining_Entity (Pack_Decl)); end Refined_State; ----------------------- @@ -21092,6 +20923,7 @@ package body Sem_Prag is Prag := Contract_Test_Cases (Items); while Present (Prag) loop if Pragma_Name (Prag) = Name_Test_Case + and then Prag /= N and then String_Equal (Name, Get_Name_From_CTC_Pragma (Prag)) then @@ -21115,11 +20947,6 @@ package body Sem_Prag is -- Start of processing for Test_Case begin - -- Reset the Analyzed flag because the pragma requires further - -- analysis. - - Set_Analyzed (N, False); - GNAT_Pragma; Check_At_Least_N_Arguments (2); Check_At_Most_N_Arguments (4); @@ -21194,7 +21021,7 @@ package body Sem_Prag is and then Nkind_In (Context, N_Generic_Package_Declaration, N_Package_Declaration) then - Subp_Id := Defining_Entity (Subp_Decl); + null; -- Otherwise the placement is illegal @@ -21203,6 +21030,13 @@ package body Sem_Prag is return; end if; + Subp_Id := Defining_Entity (Subp_Decl); + + -- Chain the pragma on the contract for further processing by + -- Analyze_Test_Case_In_Decl_Part. + + Add_Contract_Item (N, Subp_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -21239,13 +21073,14 @@ package body Sem_Prag is if Nkind_In (Subp_Decl, N_Subprogram_Body, N_Subprogram_Body_Stub) then + -- The legality checks of pragma Test_Case are affected by the + -- SPARK mode in effect and the volatility of the context. + -- Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); Analyze_Test_Case_In_Decl_Part (N); end if; - - -- Chain the pragma on the contract for further processing by - -- Analyze_Test_Case_In_Decl_Part. - - Add_Contract_Item (N, Subp_Id); end Test_Case; -------------------------- @@ -22113,6 +21948,16 @@ package body Sem_Prag is return; end if; + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Spec_Id); + + -- The legality checks of pragma Volatile_Function are affected by + -- the SPARK mode in effect. Analyze all pragmas in a specific + -- order. + + Analyze_If_Present (Pragma_SPARK_Mode); + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -22147,8 +21992,6 @@ package body Sem_Prag is if Present (Arg1) then Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); end if; - - Add_Contract_Item (N, Spec_Id); end Volatile_Function; ---------------------- @@ -25221,11 +25064,18 @@ package body Sem_Prag is if Is_Entity_Name (State) then State_Id := Entity_Of (State); + -- When the abstract state is undefined, it appears as Any_Id. Do + -- not continue with the analysis of the clause. + + if State_Id = Any_Id then + return; + -- Catch any attempts to re-refine a state or refine a state that -- is not defined in the package declaration. - if Ekind (State_Id) = E_Abstract_State then + elsif Ekind (State_Id) = E_Abstract_State then Check_Matching_State; + else SPARK_Msg_NE ("& must denote an abstract state", State, State_Id); diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 7e73617ef08..57067f49428 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -251,7 +251,7 @@ package body Sem_Res is (N : Node_Id; Op : Entity_Id; Typ : Entity_Id); - -- An operator can rename another, e.g. in an instantiation. In that + -- An operator can rename another, e.g. in an instantiation. In that -- case, the proper operator node must be constructed and resolved. procedure Set_String_Literal_Subtype (N : Node_Id; Typ : Entity_Id); @@ -2285,7 +2285,7 @@ package body Sem_Res is then exit Interp_Loop; - elsif Nkind (N) in N_Unary_Op + elsif Nkind (N) in N_Unary_Op and then Etype (Right_Opnd (N)) = Any_Type then exit Interp_Loop; @@ -11234,7 +11234,7 @@ package body Sem_Res is New_N : Node_Id; begin - if Nkind (N) in N_Binary_Op then + if Nkind (N) in N_Binary_Op then Append (Left_Opnd (N), Actuals); end if; diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb index 64f019bde32..d5be94ec90e 100644 --- a/gcc/ada/sem_type.adb +++ b/gcc/ada/sem_type.adb @@ -1977,7 +1977,7 @@ package body Sem_Type is return It2; end if; - elsif Nkind (N) in N_Unary_Op then + elsif Nkind (N) in N_Unary_Op then if Etype (Right_Opnd (N)) = Etype (First_Formal (Nam1)) then return It1; else -- 2.30.2