diff options
Diffstat (limited to 'gcc/ada')
-rw-r--r-- | gcc/ada/ChangeLog | 49 | ||||
-rw-r--r-- | gcc/ada/aspects.adb | 1 | ||||
-rw-r--r-- | gcc/ada/aspects.ads | 10 | ||||
-rw-r--r-- | gcc/ada/exp_ch3.adb | 33 | ||||
-rw-r--r-- | gcc/ada/freeze.adb | 30 | ||||
-rw-r--r-- | gcc/ada/par-prag.adb | 1 | ||||
-rw-r--r-- | gcc/ada/sem_attr.adb | 134 | ||||
-rw-r--r-- | gcc/ada/sem_ch10.adb | 79 | ||||
-rw-r--r-- | gcc/ada/sem_ch13.adb | 10 | ||||
-rw-r--r-- | gcc/ada/sem_ch6.adb | 128 | ||||
-rw-r--r-- | gcc/ada/sem_prag.adb | 416 | ||||
-rw-r--r-- | gcc/ada/sem_prag.ads | 19 | ||||
-rw-r--r-- | gcc/ada/snames.ads-tmpl | 2 |
13 files changed, 632 insertions, 280 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 97642d5e669..74d518b7893 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,52 @@ +2013-10-10 Hristian Kirtchev <kirtchev@adacore.com> + + * aspects.adb: Add an entry for Aspect_Refined_Post in table + Canonical_Aspect. + * aspects.ads: Add an entry for Aspect_Refined_Post in tables + Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay, + Aspect_On_Body_Or_Stub_OK. Update the comment on the use of + table Aspect_On_Body_Or_Stub_OK. + * par-prag.adb: Add pragma Refined_Post to the list of pragmas + that do not require special processing by the parser. + * sem_attr.adb (Analyze_Attribute): Add special analysis for + attributes 'Old and 'Result when code generation is disabled and + they appear in aspect/pragma Refined_Post. + (In_Refined_Post): New routine. + * sem_ch6.adb (Analyze_Expression_Function): Move various + aspects and/or pragmas that apply to an expression function to the + corresponding spec or body. + (Collect_Body_Postconditions): New routine. + (Process_PPCs): Use routine Collect_Body_Postconditions + to gather all postcondition pragmas. + * sem_ch10.adb (Analyze_Proper_Body): Use routine + Relocate_Pragmas_To_Body to move all source pragmas that follow + a body stub to the proper body. + (Move_Stub_Pragmas_To_Body): Removed. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing + for aspect Refined_Post. + (Check_Aspect_At_Freeze_Point): Aspect + Refined_Post does not need delayed processing at the freeze point. + * sem_prag.adb: Add an entry for pragma Refined_Post in + table Sig_Flags. + (Analyze_Pragma): Add processing for pragma + Refined_Post. Update the processing of pragma Refined_Pre + to use common routine Analyze_Refined_Pre_Post. + (Analyze_Refined_Pre_Post): New routine. + (Relocate_Pragmas_To_Body): New routine. + * sem_prag.ads: Table Pragma_On_Stub_OK is now known as + Pragma_On_Body_Or_Stub_OK. Update the comment on usage of + table Pragma_On_Body_Or_Stub_OK. + (Relocate_Pragmas_To_Body): New routine. + * snames.ads-tmpl: Add new predefined name for Refined_Post. Add + new Pragma_Id for Refined_Post. + +2013-10-10 Robert Dewar <dewar@adacore.com> + + * exp_ch3.adb (Expand_N_Variant_Part): Now null, expansion of + last choice to others is moved to Freeze_Record_Type. + * freeze.adb (Freeze_Record_Type): Expand last variant to others + if necessary (moved here from Expand_N_Variant_Part + 2013-10-10 Robert Dewar <dewar@adacore.com> * lib-xref-spark_specific.adb, par-ch13.adb, sem_prag.adb, sem_prag.ads, diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index e20cae4782f..638fdbedc29 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -466,6 +466,7 @@ package body Aspects is Aspect_Pure_05 => Aspect_Pure_05, Aspect_Pure_12 => Aspect_Pure_12, Aspect_Pure_Function => Aspect_Pure_Function, + Aspect_Refined_Post => Aspect_Refined_Post, Aspect_Refined_Pre => Aspect_Refined_Pre, Aspect_Remote_Access_Type => Aspect_Remote_Access_Type, Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 66c4b857da0..d2f5d6939a6 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -111,6 +111,7 @@ package Aspects is Aspect_Predicate, -- GNAT Aspect_Priority, Aspect_Read, + Aspect_Refined_Post, -- GNAT Aspect_Refined_Pre, -- GNAT Aspect_Relative_Deadline, Aspect_Scalar_Storage_Order, -- GNAT @@ -320,6 +321,7 @@ package Aspects is Aspect_Predicate => Expression, Aspect_Priority => Expression, Aspect_Read => Name, + Aspect_Refined_Post => Expression, Aspect_Refined_Pre => Expression, Aspect_Relative_Deadline => Expression, Aspect_Scalar_Storage_Order => Expression, @@ -417,6 +419,7 @@ package Aspects is Aspect_Pure_12 => Name_Pure_12, Aspect_Pure_Function => Name_Pure_Function, Aspect_Read => Name_Read, + Aspect_Refined_Post => Name_Refined_Post, Aspect_Refined_Pre => Name_Refined_Pre, Aspect_Relative_Deadline => Name_Relative_Deadline, Aspect_Remote_Access_Type => Name_Remote_Access_Type, @@ -639,6 +642,7 @@ package Aspects is Aspect_Convention => Never_Delay, Aspect_Dimension => Never_Delay, Aspect_Dimension_System => Never_Delay, + Aspect_Refined_Post => Never_Delay, Aspect_Refined_Pre => Never_Delay, Aspect_SPARK_Mode => Never_Delay, Aspect_Synchronization => Never_Delay, @@ -695,8 +699,12 @@ package Aspects is -- package P with SPARK_Mode ...; -- package body P with SPARK_Mode is ...; + -- The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit + -- Sem_Prag if the aspects below are implemented by a pragma. + Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean := - (Aspect_Refined_Pre => True, + (Aspect_Refined_Post => True, + Aspect_Refined_Pre => True, Aspect_SPARK_Mode => True, Aspect_Warnings => True, others => False); diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 8e1124aca4b..98ad0e21cf2 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -5846,31 +5846,18 @@ package body Exp_Ch3 is -- Expand_N_Variant_Part -- --------------------------- - procedure Expand_N_Variant_Part (N : Node_Id) is - Last_Var : constant Node_Id := Last_Non_Pragma (Variants (N)); - Others_Node : Node_Id; + -- Note: this procedure no longer has any effect. It used to be that we + -- would replace the choices in the last variant by a when others, and + -- also expanded static predicates in variant choices here, but both of + -- those activities were being done too early, since we can't check the + -- choices until the statically predicated subtypes are frozen, which can + -- happen as late as the free point of the record, and we can't change the + -- last choice to an others before checking the choices, which is now done + -- at the freeze point of the record. + procedure Expand_N_Variant_Part (N : Node_Id) is begin - -- If the last variant does not contain the Others choice, replace it - -- with an N_Others_Choice node since Gigi always wants an Others. Note - -- that we do not bother to call Analyze on the modified variant part, - -- since its only effect would be to compute the Others_Discrete_Choices - -- node laboriously, and of course we already know the list of choices - -- corresponding to the others choice (it's the list we're replacing!) - - if Nkind (First (Discrete_Choices (Last_Var))) /= N_Others_Choice then - Others_Node := Make_Others_Choice (Sloc (Last_Var)); - Set_Others_Discrete_Choices - (Others_Node, Discrete_Choices (Last_Var)); - Set_Discrete_Choices (Last_Var, New_List (Others_Node)); - end if; - - -- We have one more expansion activity, which is to deal with static - -- predicates in the variant choices. But we have to defer that to - -- the freeze point, because the statically predicated subtype won't - -- be fully processed till then, so this expansion activity is carried - -- out in Freeze_Record_Type. - + null; end Expand_N_Variant_Part; --------------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index ac9f570fda9..e8a2d9fb52b 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2639,7 +2639,7 @@ package body Freeze is C : Node_Id; V : Node_Id; - Others_Present : Boolean; + Others_Present : Boolean; pragma Warnings (Off, Others_Present); -- Indicates others present, not used in this case @@ -2748,12 +2748,38 @@ package body Freeze is end if; end if; - -- If we have a variant part, check choices + -- Case of variant part present if Present (C) and then Present (Variant_Part (C)) then V := Variant_Part (C); + + -- Check choices + Check_Choices (V, Variants (V), Etype (Name (V)), Others_Present); + + -- If the last variant does not contain the Others choice, + -- replace it with an N_Others_Choice node since Gigi always + -- wants an Others. Note that we do not bother to call Analyze + -- on the modified variant part, since its only effect would be + -- to compute the Others_Discrete_Choices node laboriously, and + -- of course we already know the list of choices corresponding + -- to the others choice (it's the list we're replacing!) + + declare + Last_Var : constant Node_Id := + Last_Non_Pragma (Variants (V)); + Others_Node : Node_Id; + begin + if Nkind (First (Discrete_Choices (Last_Var))) /= + N_Others_Choice + then + Others_Node := Make_Others_Choice (Sloc (Last_Var)); + Set_Others_Discrete_Choices + (Others_Node, Discrete_Choices (Last_Var)); + Set_Discrete_Choices (Last_Var, New_List (Others_Node)); + end if; + end; end if; end Check_Variant_Part; end Freeze_Record_Type; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 91e9b96b138..85ebe3bdeb7 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1250,6 +1250,7 @@ begin Pragma_Pure_12 | Pragma_Pure_Function | Pragma_Queuing_Policy | + Pragma_Refined_Post | Pragma_Refined_Pre | Pragma_Relative_Deadline | Pragma_Remote_Access_Type | diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 53f66b011db..91079a836f2 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -303,10 +303,6 @@ package body Sem_Attr is -- Verify that prefix of attribute N is a float type and that -- two attribute expressions are present - procedure Legal_Formal_Attribute; - -- Common processing for attributes Definite and Has_Discriminants. - -- Checks that prefix is generic indefinite formal type. - procedure Check_SPARK_Restriction_On_Attribute; -- Issue an error in formal mode because attribute N is allowed @@ -377,6 +373,14 @@ package body Sem_Attr is pragma No_Return (Error_Attr); -- Like Error_Attr, but error is posted at the start of the prefix + function In_Refined_Post return Boolean; + -- Determine whether the current attribute appears in pragma + -- Refined_Post. + + procedure Legal_Formal_Attribute; + -- Common processing for attributes Definite and Has_Discriminants. + -- Checks that prefix is generic indefinite formal type. + procedure Standard_Attribute (Val : Int); -- Used to process attributes whose prefix is package Standard which -- yield values of type Universal_Integer. The attribute reference @@ -1927,6 +1931,60 @@ package body Sem_Attr is Error_Attr; end Error_Attr_P; + --------------------- + -- In_Refined_Post -- + --------------------- + + function In_Refined_Post return Boolean is + function Is_Refined_Post (Prag : Node_Id) return Boolean; + -- Determine whether Prag denotes one of the incarnations of pragma + -- Refined_Post (either as is or pragma Check (Refined_Post, ...). + + --------------------- + -- Is_Refined_Post -- + --------------------- + + function Is_Refined_Post (Prag : Node_Id) return Boolean is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + Nam : constant Name_Id := Pragma_Name (Prag); + + begin + if Nam = Name_Refined_Post then + return True; + + elsif Nam = Name_Check then + pragma Assert (Present (Args)); + + return Chars (Expression (First (Args))) = Name_Refined_Post; + end if; + + return False; + end Is_Refined_Post; + + -- Local variables + + Stmt : Node_Id; + + -- Start of processing for In_Refined_Post + + begin + Stmt := Parent (N); + while Present (Stmt) loop + if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Stmt) then + exit; + end if; + + Stmt := Parent (Stmt); + end loop; + + return False; + end In_Refined_Post; + ---------------------------- -- Legal_Formal_Attribute -- ---------------------------- @@ -4281,7 +4339,32 @@ package body Sem_Attr is Error_Attr ("% attribute can only appear in postcondition", P); end if; - -- Body case, where we must be inside a generated _Postcondition + -- Check the legality of attribute 'Old when it appears inside pragma + -- Refined_Post. These specialized checks are required only when code + -- generation is disabled. In the general case pragma Refined_Post is + -- transformed into pragma Check by Process_PPCs which in turn is + -- relocated to procedure _Postconditions. From then on the legality + -- of 'Old is determined as usual. + + elsif not Expander_Active and then In_Refined_Post then + Preanalyze_And_Resolve (P); + P_Type := Etype (P); + Set_Etype (N, P_Type); + + if Is_Limited_Type (P_Type) then + Error_Attr ("attribute % cannot apply to limited objects", P); + end if; + + if Is_Entity_Name (P) + and then Is_Constant_Object (Entity (P)) + then + Error_Msg_N + ("??attribute Old applied to constant has no effect", P); + end if; + + return; + + -- Body case, where we must be inside a generated _Postconditions -- procedure, or else the attribute use is definitely misplaced. The -- postcondition itself may have generated transient scopes, and is -- not necessarily the current one. @@ -4302,8 +4385,8 @@ package body Sem_Attr is -- If the attribute reference is generated for a Requires clause, -- then no expressions follow. Otherwise it is a primary, in which - -- case, if expressions follow, the attribute reference must be - -- an indexable object, so rewrite the node accordingly. + -- case, if expressions follow, the attribute reference must be an + -- indexable object, so rewrite the node accordingly. if Present (E1) then Rewrite (N, @@ -4320,8 +4403,8 @@ package body Sem_Attr is Check_E0; - -- Prefix has not been analyzed yet, and its full analysis will - -- take place during expansion (see below). + -- Prefix has not been analyzed yet, and its full analysis will take + -- place during expansion (see below). Preanalyze_And_Resolve (P); P_Type := Etype (P); @@ -4725,7 +4808,32 @@ package body Sem_Attr is Set_Is_Overloaded (P, False); end if; - -- Body case, where we must be inside a generated _Postcondition + -- Check the legality of attribute 'Result when it appears inside + -- pragma Refined_Post. These specialized checks are required only + -- when code generation is disabled. In the general case pragma + -- Refined_Post is transformed into pragma Check by Process_PPCs + -- which in turn is relocated to procedure _Postconditions. From + -- then on the legality of 'Result is determined as usual. + + elsif not Expander_Active and then In_Refined_Post then + PS := Current_Scope; + + -- The prefix denotes the proper related function + + if Is_Entity_Name (P) + and then Ekind (Entity (P)) = E_Function + and then Entity (P) = PS + then + null; + + else + Error_Msg_Name_2 := Chars (PS); + Error_Attr ("incorrect prefix for % attribute, expected %", P); + end if; + + Set_Etype (N, Etype (PS)); + + -- Body case, where we must be inside a generated _Postconditions -- procedure, and the prefix must be on the scope stack, or else the -- attribute use is definitely misplaced. The postcondition itself -- may have generated transient scopes, and is not necessarily the @@ -4763,9 +4871,9 @@ package body Sem_Attr is null; else - Error_Msg_NE - ("incorrect prefix for % attribute, expected &", P, PS); - Error_Attr; + Error_Msg_Name_2 := Chars (PS); + Error_Attr + ("incorrect prefix for % attribute, expected %", P); end if; Rewrite (N, Make_Identifier (Sloc (N), Name_uResult)); diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index c68c5caa46a..8d64964ac78 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -1596,85 +1596,12 @@ package body Sem_Ch10 is Subunit_Name : constant Unit_Name_Type := Get_Unit_Name (N); Unum : Unit_Number_Type; - procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id); - -- Relocate all pragmas that apply to a subprogram body stub to the - -- declarations of proper body Bod. - -- Should we do this for the reamining body stub kinds??? - procedure Optional_Subunit; -- This procedure is called when the main unit is a stub, or when we -- are not generating code. In such a case, we analyze the subunit if -- present, which is user-friendly and in fact required for ASIS, but -- we don't complain if the subunit is missing. - ------------------------------- - -- Move_Stub_Pragmas_To_Body -- - ------------------------------- - - procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id) is - procedure Move_Pragma (Prag : Node_Id); - -- Relocate one pragma to the declarations of Bod - - ----------------- - -- Move_Pragma -- - ----------------- - - procedure Move_Pragma (Prag : Node_Id) is - Decls : List_Id := Declarations (Bod); - - begin - if No (Decls) then - Decls := New_List; - Set_Declarations (Bod, Decls); - end if; - - -- Unhook the pragma from its current list - - Remove (Prag); - Prepend (Prag, Decls); - end Move_Pragma; - - -- Local variables - - Next_Stmt : Node_Id; - Stmt : Node_Id; - - -- Start of processing for Move_Stub_Pragmas_To_Body - - begin - pragma Assert (Nkind (N) = N_Subprogram_Body_Stub); - - -- Perform a bit of a lookahead - peek at any subsequent source - -- pragmas while skipping internally generated code. - - Stmt := Next (N); - while Present (Stmt) loop - Next_Stmt := Next (Stmt); - - -- Move a source pragma that applies to a subprogram stub to the - -- declarations of the proper body. - - if Comes_From_Source (Stmt) - and then Nkind (Stmt) = N_Pragma - and then Pragma_On_Stub_OK (Get_Pragma_Id (Stmt)) - then - Move_Pragma (Stmt); - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - - -- No valid pragmas are available for relocation - - else - exit; - end if; - - Stmt := Next_Stmt; - end loop; - end Move_Stub_Pragmas_To_Body; - ---------------------- -- Optional_Subunit -- ---------------------- @@ -1932,11 +1859,11 @@ package body Sem_Ch10 is Move_Or_Merge_Aspects (From => N, To => Prop_Body); - -- Propagate all source pragmas associated with a - -- subprogram body stub to the proper body. + -- Move all source pragmas that follow the body stub and + -- apply to it to the declarations of the proper body. if Nkind (N) = N_Subprogram_Body_Stub then - Move_Stub_Pragmas_To_Body (Prop_Body); + Relocate_Pragmas_To_Body (N, Target_Body => Prop_Body); end if; -- Analyze the unit if semantics active diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 3a2bb22b4e4..7f6c9acb943 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1928,6 +1928,15 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_SPARK_Mode); + -- Refined_Post + + when Aspect_Refined_Post => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Refined_Post); + -- Refined_Pre when Aspect_Refined_Pre => @@ -7788,6 +7797,7 @@ package body Sem_Ch13 is Aspect_Postcondition | Aspect_Pre | Aspect_Precondition | + Aspect_Refined_Post | Aspect_Refined_Pre | Aspect_SPARK_Mode | Aspect_Test_Case => diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index b1c59086297..e313f3518d8 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -349,15 +349,25 @@ package body Sem_Ch6 is Make_Handled_Sequence_Of_Statements (LocX, Statements => New_List (Ret))); + -- If the expression completes a generic subprogram, we must create a + -- separate node for the body, because at instantiation the original + -- node of the generic copy must be a generic subprogram body, and + -- cannot be a expression function. Otherwise we just rewrite the + -- expression with the non-generic body. + if Present (Prev) and then Ekind (Prev) = E_Generic_Function then + Insert_After (N, New_Body); - -- If the expression completes a generic subprogram, we must create a - -- separate node for the body, because at instantiation the original - -- node of the generic copy must be a generic subprogram body, and - -- cannot be a expression function. Otherwise we just rewrite the - -- expression with the non-generic body. + -- Propagate any aspects or pragmas that apply to the expression + -- function to the proper body when the expression function acts + -- as a completion. + + if Has_Aspects (N) then + Move_Aspects (N, To => New_Body); + end if; + + Relocate_Pragmas_To_Body (New_Body); - Insert_After (N, New_Body); Rewrite (N, Make_Null_Statement (Loc)); Set_Has_Completion (Prev, False); Analyze (N); @@ -371,6 +381,12 @@ package body Sem_Ch6 is Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True); Rewrite (N, New_Body); + + -- Propagate any pragmas that apply to the expression function to the + -- proper body when the expression function acts as a completion. + -- Aspects are automatically transfered because of node rewriting. + + Relocate_Pragmas_To_Body (N); Analyze (N); -- Prev is the previous entity with the same name, but it is can @@ -11274,6 +11290,11 @@ package body Sem_Ch6 is -- under the same visibility conditions as for other invariant checks, -- the type invariant must be applied to the returned value. + procedure Collect_Body_Postconditions (Post_Nam : Name_Id); + -- Examine the declarations of the body, looking for pragmas with name + -- Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or + -- Name_Refined_Post. Chain any relevant postconditions to Plist. + function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id; -- Prag contains an analyzed precondition or postcondition pragma. This -- function copies the pragma, changes it to the corresponding Check @@ -11365,6 +11386,60 @@ package body Sem_Ch6 is end if; end Check_Access_Invariants; + --------------------------------- + -- Collect_Body_Postconditions -- + --------------------------------- + + procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is + Next_Prag : Node_Id; + + begin + pragma Assert + (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post)); + + Prag := First (Declarations (N)); + while Present (Prag) loop + Next_Prag := Next (Prag); + + if Nkind (Prag) = N_Pragma then + + -- Capture postcondition pragmas + + if Pragma_Name (Prag) = Post_Nam then + Analyze (Prag); + + -- All Refined_Post pragmas must be relocated to the body + -- of the generated _Postconditions routine, otherwise they + -- will be duplicated twice - once in the declarations of + -- the body and once in _Postconditions. + + if Pragma_Name (Prag) = Name_Refined_Post then + Remove (Prag); + end if; + + -- If expansion is disabled, as in a generic unit, save + -- pragma for later expansion. + + if not Expander_Active then + Prepend (Grab_PPC, Declarations (N)); + else + Append_Enabled_Item (Grab_PPC, Plist); + end if; + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Prag) then + null; + + else + exit; + end if; + + Prag := Next_Prag; + end loop; + end Collect_Body_Postconditions; + -------------- -- Grab_PPC -- -------------- @@ -11791,6 +11866,8 @@ package body Sem_Ch6 is -- procedure _postconditions [(_Result : resulttype)] is -- begin + -- pragma Check (Refined_Post, condition); + -- pragma Check (Refined_Post, condition); -- pragma Check (Postcondition, condition [,message]); -- pragma Check (Postcondition, condition [,message]); -- ... @@ -11801,43 +11878,8 @@ package body Sem_Ch6 is -- First we deal with the postconditions in the body - if Is_Non_Empty_List (Declarations (N)) then - - -- Loop through declarations - - Prag := First (Declarations (N)); - while Present (Prag) loop - if Nkind (Prag) = N_Pragma then - - -- Capture postcondition pragmas - - if Pragma_Name (Prag) = Name_Postcondition then - Analyze (Prag); - - -- If expansion is disabled, as in a generic unit, save - -- pragma for later expansion. - - if not Expander_Active then - Prepend (Grab_PPC, Declarations (N)); - else - Append_Enabled_Item (Grab_PPC, Plist); - end if; - end if; - - Next (Prag); - - -- Not a pragma, if comes from source, then end scan - - elsif Comes_From_Source (Prag) then - exit; - - -- Skip stuff not coming from source - - else - Next (Prag); - end if; - end loop; - end if; + Collect_Body_Postconditions (Name_Refined_Post); + Collect_Body_Postconditions (Name_Postcondition); -- Now deal with any postconditions from the spec diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 6f77c958d0b..d8c32ddf996 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -1922,6 +1922,16 @@ package body Sem_Prag is -- In Ada 95 or 05 mode, these are implementation defined pragmas, so -- should be caught by the No_Implementation_Pragmas restriction. + procedure Analyze_Refined_Pre_Post + (Body_Decl : out Node_Id; + Spec_Id : out Entity_Id; + Legal : out Boolean); + -- Subsidiary routine to the analysis of pragmas Refined_Pre and + -- Refined_Post. Body_Decl is the declaration of the subprogram body + -- [stub] subject to the pragma. Spec_Id is the corresponding spec of + -- the subprogram body [stub]. Flag Legal denotes whether the pragma + -- passes all legality rules. + procedure Check_Ada_83_Warning; -- Issues a warning message for the current pragma if operating in Ada -- 83 mode (used for language pragmas that are not a standard part of @@ -2448,6 +2458,129 @@ package body Sem_Prag is end if; end Ada_2012_Pragma; + ------------------------------ + -- Analyze_Refined_Pre_Post -- + ------------------------------ + + procedure Analyze_Refined_Pre_Post + (Body_Decl : out Node_Id; + Spec_Id : out Entity_Id; + Legal : out Boolean) + is + Pack_Spec : Node_Id; + Spec_Decl : Node_Id; + Stmt : Node_Id; + + begin + -- Assume that the pragma is illegal + + Body_Decl := Parent (N); + Spec_Id := Empty; + Legal := False; + + GNAT_Pragma; + Check_Arg_Count (1); + Check_No_Identifiers; + + -- Verify the placement of the pragma and check for duplicates + + Stmt := Prev (N); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Pragma_Name (Stmt) = Pname then + Error_Msg_Name_1 := Pname; + Error_Msg_Sloc := Sloc (Stmt); + Error_Msg_N ("pragma % duplicates pragma declared #", N); + end if; + + -- Emit an error when the pragma applies to an expression function + -- that does not act as a completion. + + elsif Nkind (Stmt) = N_Subprogram_Declaration + and then Nkind (Original_Node (Stmt)) = N_Expression_Function + and then not + Has_Completion (Defining_Unit_Name (Specification (Stmt))) + then + Error_Pragma + ("pragma % cannot apply to a stand alone expression " + & "function"); + return; + + -- The pragma applies to a subprogram body stub + + elsif Nkind (Stmt) = N_Subprogram_Body_Stub then + Body_Decl := Stmt; + exit; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + null; + + -- The pragma does not apply to a legal construct, issue an error + -- and stop the analysis. + + else + Pragma_Misplaced; + return; + end if; + + Stmt := Prev (Stmt); + end loop; + + -- Pragma Refined_Pre/Post must apply to a subprogram body [stub] + + if not Nkind_In (Body_Decl, N_Subprogram_Body, + N_Subprogram_Body_Stub) + then + Pragma_Misplaced; + return; + end if; + + -- The body [stub] must not act as a spec, in other words it has to + -- be paired with a corresponding spec. + + if Nkind (Body_Decl) = N_Subprogram_Body then + Spec_Id := Corresponding_Spec (Body_Decl); + else + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + end if; + + if No (Spec_Id) then + Error_Pragma ("pragma % cannot apply to a stand alone body"); + return; + end if; + + -- Refined_Pre/Post may only apply to the body [stub] of a subprogram + -- declared in the visible part of a package. Retrieve the context of + -- the subprogram declaration. + + Spec_Decl := Parent (Parent (Spec_Id)); + + pragma Assert + (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration, + N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration)); + + Pack_Spec := Parent (Spec_Decl); + + if Nkind (Pack_Spec) /= N_Package_Specification + or else List_Containing (Spec_Decl) /= + Visible_Declarations (Pack_Spec) + then + Error_Pragma + ("pragma % must apply to the body of a visible subprogram"); + return; + end if; + + -- If we get here, the placement and legality of the pragma is OK + + Legal := True; + end Analyze_Refined_Pre_Post; + -------------------------- -- Check_Ada_83_Warning -- -------------------------- @@ -15933,145 +16066,79 @@ package body Sem_Prag is when Pragma_Rational => Set_Rational_Profile; - ----------------- - -- Refined_Pre -- - ----------------- + ------------------ + -- Refined_Post -- + ------------------ - -- pragma Refined_Pre (boolean_EXPRESSION); + -- pragma Refined_Post (boolean_EXPRESSION); - when Pragma_Refined_Pre => Refined_Pre : declare - Body_Decl : Node_Id := Parent (N); - Pack_Spec : Node_Id; - Restore : Boolean := False; - Spec_Decl : Node_Id; + when Pragma_Refined_Post => Refined_Post : declare + Body_Decl : Node_Id; + Legal : Boolean; Spec_Id : Entity_Id; - Stmt : Node_Id; begin - GNAT_Pragma; - Check_Arg_Count (1); - Check_No_Identifiers; - - -- Verify the placement of the pragma and check for duplicates - - Stmt := Prev (N); - while Present (Stmt) loop - - -- Skip prior pragmas, but check for duplicates - - if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared #", N); - end if; - - -- The pragma applies to a subprogram body stub - - elsif Nkind (Stmt) = N_Subprogram_Body_Stub then - Body_Decl := Stmt; - exit; - - -- The pragma applies to an expression function that does not - -- act as a completion of a previous function declaration. - - elsif Nkind (Stmt) = N_Subprogram_Declaration - and then Nkind (Original_Node (Stmt)) = N_Expression_Function - and then not - Has_Completion (Defining_Unit_Name (Specification (Stmt))) - then - Error_Pragma ("pragma % cannot apply to a stand alone body"); - return; - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. - - else - Pragma_Misplaced; - return; - end if; + -- Verify the legal placement of the pragma. The pragma is left + -- intentionally semi-analyzed. Process_PPCs does the remaining + -- analysis of the expression when Refined_Post is converted into + -- pragma Check. - Stmt := Prev (Stmt); - end loop; - - -- Pragma Refined_Pre must apply to a subprogram body [stub] - - if not Nkind_In (Body_Decl, N_Subprogram_Body, - N_Subprogram_Body_Stub) - then - Pragma_Misplaced; - return; - end if; - - -- The body [stub] must not act as a spec + Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal); - if Nkind (Body_Decl) = N_Subprogram_Body then - Spec_Id := Corresponding_Spec (Body_Decl); - else - Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); - end if; + -- Analyze the expression when code generation is disabled because + -- the contract of the related subprogram will never be processed. - if No (Spec_Id) then - Error_Pragma ("pragma % cannot apply to a stand alone body"); - return; + if Legal and then not Expander_Active then + Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean); end if; + end Refined_Post; - -- Refined_Pre may only apply to the body [stub] of a subprogram - -- declared in the visible part of a package. Retrieve the context - -- of the subprogram declaration. - - Spec_Decl := Parent (Parent (Spec_Id)); + ----------------- + -- Refined_Pre -- + ----------------- - pragma Assert - (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration, - N_Generic_Subprogram_Declaration, - N_Subprogram_Declaration)); + -- pragma Refined_Pre (boolean_EXPRESSION); - Pack_Spec := Parent (Spec_Decl); + when Pragma_Refined_Pre => Refined_Pre : declare + Body_Decl : Node_Id; + Legal : Boolean; + Restore : Boolean := False; + Spec_Id : Entity_Id; - if Nkind (Pack_Spec) /= N_Package_Specification - or else List_Containing (Spec_Decl) /= - Visible_Declarations (Pack_Spec) - then - Error_Pragma - ("pragma % must apply to the body of a visible subprogram"); - end if; + begin + Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal); - -- When the pragma applies to a subprogram stub without a proper - -- body, we have to restore the visibility of the stub and its - -- formals to perform analysis. + if Legal then + pragma Assert (Present (Body_Decl)); + pragma Assert (Present (Spec_Id)); - if Nkind (Body_Decl) = N_Subprogram_Body_Stub - and then No (Library_Unit (Body_Decl)) - and then Current_Scope /= Spec_Id - then - Restore := True; - Push_Scope (Spec_Id); - Install_Formals (Spec_Id); - end if; + if Nkind (Body_Decl) = N_Subprogram_Body_Stub + and then No (Library_Unit (Body_Decl)) + and then Current_Scope /= Spec_Id + then + Restore := True; + Push_Scope (Spec_Id); + Install_Formals (Spec_Id); + end if; - -- Convert pragma Refined_Pre into pragma Check. The analysis of - -- the generated pragma will take care of the expression. + -- Convert pragma Refined_Pre into pragma Check. The analysis + -- of the generated pragma will take care of the expression. - Rewrite (N, - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Pname)), + Rewrite (N, + Make_Pragma (Loc, + Chars => Name_Check, + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Pname)), - Make_Pragma_Argument_Association (Sloc (Arg1), - Expression => Relocate_Node (Get_Pragma_Arg (Arg1)))))); + Make_Pragma_Argument_Association (Sloc (Arg1), + Expression => Relocate_Node (Get_Pragma_Arg (Arg1)))))); - Analyze (N); + Analyze (N); - if Restore then - Pop_Scope; + if Restore then + Pop_Scope; + end if; end if; end Refined_Pre; @@ -19158,6 +19225,7 @@ package body Sem_Prag is Pragma_Queuing_Policy => -1, Pragma_Rational => -1, Pragma_Ravenscar => -1, + Pragma_Refined_Post => -1, Pragma_Refined_Pre => -1, Pragma_Relative_Deadline => -1, Pragma_Remote_Access_Type => -1, @@ -19593,6 +19661,116 @@ package body Sem_Prag is end Process_Compilation_Unit_Pragmas; + ------------------------------ + -- Relocate_Pragmas_To_Body -- + ------------------------------ + + procedure Relocate_Pragmas_To_Body + (Subp_Body : Node_Id; + Target_Body : Node_Id := Empty) + is + procedure Relocate_Pragma (Prag : Node_Id); + -- Remove a single pragma from its current list and add it to the + -- declarations of the proper body (either Subp_Body or Target_Body). + + --------------------- + -- Relocate_Pragma -- + --------------------- + + procedure Relocate_Pragma (Prag : Node_Id) is + Decls : List_Id; + Target : Node_Id; + + begin + -- When subprogram stubs or expression functions are involves, the + -- destination declaration list belongs to the proper body. + + if Present (Target_Body) then + Target := Target_Body; + else + Target := Subp_Body; + end if; + + Decls := Declarations (Target); + + if No (Decls) then + Decls := New_List; + Set_Declarations (Target, Decls); + end if; + + -- Unhook the pragma from its current list + + Remove (Prag); + Prepend (Prag, Decls); + end Relocate_Pragma; + + -- Local variables + + Body_Id : constant Entity_Id := + Defining_Unit_Name (Specification (Subp_Body)); + Next_Stmt : Node_Id; + Stmt : Node_Id; + + -- Start of processing for Relocate_Pragmas_To_Body + + begin + -- Do not process a body that comes from a separate unit as no construct + -- can possibly follow it. + + if not Is_List_Member (Subp_Body) then + return; + + -- Do not relocate pragmas that follow a stub if the stub does not have + -- a proper body. + + elsif Nkind (Subp_Body) = N_Subprogram_Body_Stub + and then No (Target_Body) + then + return; + + -- Do not process internally generated routine _Postconditions + + elsif Ekind (Body_Id) = E_Procedure + and then Chars (Body_Id) = Name_uPostconditions + then + return; + end if; + + -- Look at what is following the body. We are interested in certain kind + -- of pragmas (either from source or byproducts of expansion) that can + -- apply to a body [stub]. + + Stmt := Next (Subp_Body); + while Present (Stmt) loop + + -- Preserve the following statement for iteration purposes due to a + -- possible relocation of a pragma. + + Next_Stmt := Next (Stmt); + + -- Move a candidate pragma following the body to the declarations of + -- the body. + + if Nkind (Stmt) = N_Pragma + and then Pragma_On_Body_Or_Stub_OK (Get_Pragma_Id (Stmt)) + then + Relocate_Pragma (Stmt); + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + null; + + -- No candidate pragmas are available for relocation + + else + exit; + end if; + + Stmt := Next_Stmt; + end loop; + end Relocate_Pragmas_To_Body; + ---------------------------- -- Rewrite_Assertion_Kind -- ---------------------------- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 13ec1a3b99d..492eb9f779f 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -33,11 +33,15 @@ with Types; use Types; package Sem_Prag is -- The following table lists all the implementation-defined pragmas that - -- may apply to a body stub (no language defined pragmas apply). + -- may apply to a body stub (no language defined pragmas apply). The table + -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if + -- the pragmas below implement an aspect. - Pragma_On_Stub_OK : constant array (Pragma_Id) of Boolean := - (Pragma_Refined_Pre => True, + Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean := + (Pragma_Refined_Post => True, + Pragma_Refined_Pre => True, Pragma_SPARK_Mode => True, + Pragma_Warnings => True, others => False); ----------------- @@ -164,6 +168,15 @@ package Sem_Prag is -- Suppress_All at this stage, since it can appear after the unit instead -- of before (actually we allow it to appear anywhere). + procedure Relocate_Pragmas_To_Body + (Subp_Body : Node_Id; + Target_Body : Node_Id := Empty); + -- Resocate all pragmas that follow and apply to subprogram body Subp_Body + -- to its own declaration list. Candidate pragmas are classified in table + -- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved + -- to the declarations of Target_Body. This formal should be set when + -- dealing with subprogram body stubs or expression functions. + procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id); -- This routine is used to set an encoded interface name. The node S is an -- N_String_Literal node for the external name to be set, and E is an diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index ed483f4c333..d32f5065dfc 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -580,6 +580,7 @@ package Snames is Name_Pure_05 : constant Name_Id := N + $; -- GNAT Name_Pure_12 : constant Name_Id := N + $; -- GNAT Name_Pure_Function : constant Name_Id := N + $; -- GNAT + Name_Refined_Post : constant Name_Id := N + $; -- GNAT Name_Refined_Pre : constant Name_Id := N + $; -- GNAT Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05 Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT @@ -1861,6 +1862,7 @@ package Snames is Pragma_Pure_05, Pragma_Pure_12, Pragma_Pure_Function, + Pragma_Refined_Post, Pragma_Refined_Pre, Pragma_Relative_Deadline, Pragma_Remote_Access_Type, |