From ff7a7e12be85d18d68c1919346f267d5da7d0d61 Mon Sep 17 00:00:00 2001 From: Robert Dewar Date: Sun, 13 Oct 2013 16:34:01 +0000 Subject: [PATCH] gnat_rm.texi: Add documentation for pragmas Pre[_Class] Post[_Class]. 2013-10-13 Robert Dewar * gnat_rm.texi: Add documentation for pragmas Pre[_Class] Post[_Class]. * par-ch2.adb (Skip_Pragma_Semicolon): Handle extra semicolon nicely. * par-prag.adb: Add entries for pragmas Pre[_Class] and Post[_Class]. * sem_prag.adb: Add handling of pragmas Pre[_Class] and Post[_Class]. * sem_util.adb (Original_Aspect_Name): Moved here from Sem_Prag.Original_Name, and modified to handle pragmas Pre/Post/Pre_Class/Post_Class. * sem_util.ads (Original_Aspect_Name): Moved here from Sem_Prag.Original_Name. * snames.ads-tmpl: Add entries for pragmas Pre[_Class] and Post[_Class]. 2013-10-13 Robert Dewar * einfo.adb, sem_ch6.adb: Minor reformatting. From-SVN: r203505 --- gcc/ada/ChangeLog | 21 ++++ gcc/ada/einfo.adb | 22 ++-- gcc/ada/gnat_rm.texi | 139 ++++++++++++++++++++- gcc/ada/par-ch2.adb | 18 +-- gcc/ada/par-prag.adb | 4 + gcc/ada/sem_ch6.adb | 1 - gcc/ada/sem_prag.adb | 268 ++++++++++++++++++++++++++++------------ gcc/ada/sem_util.adb | 114 ++++++++++++++++- gcc/ada/sem_util.ads | 10 ++ gcc/ada/snames.ads-tmpl | 11 +- 10 files changed, 496 insertions(+), 112 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 65093fa655c..0b09903605f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2013-10-13 Robert Dewar + + * gnat_rm.texi: Add documentation for pragmas Pre[_Class] + Post[_Class]. + * par-ch2.adb (Skip_Pragma_Semicolon): Handle extra semicolon nicely. + * par-prag.adb: Add entries for pragmas Pre[_Class] and + Post[_Class]. + * sem_prag.adb: Add handling of pragmas Pre[_Class] and + Post[_Class]. + * sem_util.adb (Original_Aspect_Name): Moved here from + Sem_Prag.Original_Name, and modified to handle pragmas + Pre/Post/Pre_Class/Post_Class. + * sem_util.ads (Original_Aspect_Name): Moved here from + Sem_Prag.Original_Name. + * snames.ads-tmpl: Add entries for pragmas Pre[_Class] and + Post[_Class]. + +2013-10-13 Robert Dewar + + * einfo.adb, sem_ch6.adb: Minor reformatting. + 2013-10-13 Hristian Kirtchev * einfo.adb: Add node/list usage for Refined_State diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index e9c262afaac..fa0daa98ce6 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -6292,16 +6292,18 @@ package body Einfo is ---------------- function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is - Is_CDG : constant Boolean := - Id = Pragma_Depends - or else Id = Pragma_Global - or else Id = Pragma_Refined_Depends - or else Id = Pragma_Refined_Global; - Is_CTC : constant Boolean := - Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; - Is_PPC : constant Boolean := - Id = Pragma_Precondition - or else Id = Pragma_Postcondition; + Is_CDG : constant Boolean := + Id = Pragma_Depends or else + Id = Pragma_Global or else + Id = Pragma_Refined_Depends or else + Id = Pragma_Refined_Global; + Is_CTC : constant Boolean := + Id = Pragma_Contract_Cases or else + Id = Pragma_Test_Case; + Is_PPC : constant Boolean := + Id = Pragma_Precondition or else + Id = Pragma_Postcondition; + In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC; Item : Node_Id; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index cd518647e40..833922e4650 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -206,11 +206,15 @@ Implementation Defined Pragmas * Pragma Passive:: * Pragma Persistent_BSS:: * Pragma Polling:: +* Pragma Post:: * Pragma Postcondition:: +* Pragma Post_Class:: +* Pragma Pre:: * Pragma Precondition:: * Pragma Predicate:: * Pragma Preelaborable_Initialization:: * Pragma Preelaborate_05:: +* Pragma Pre_Class:: * Pragma Priority_Specific_Dispatching:: * Pragma Profile:: * Pragma Profile_Warnings:: @@ -1022,11 +1026,15 @@ consideration, the use of these pragmas should be minimized. * Pragma Passive:: * Pragma Persistent_BSS:: * Pragma Polling:: +* Pragma Post:: * Pragma Postcondition:: +* Pragma Post_Class:: +* Pragma Pre:: * Pragma Precondition:: * Pragma Predicate:: * Pragma Preelaborable_Initialization:: * Pragma Preelaborate_05:: +* Pragma Pre_Class:: * Pragma Priority_Specific_Dispatching:: * Pragma Profile:: * Pragma Profile_Warnings:: @@ -1393,7 +1401,10 @@ are implementation defined additions recognized by the GNAT compiler. The pragma applies in both cases to pragmas and aspects with matching names, e.g. @code{Pre} applies to the Pre aspect, and @code{Precondition} applies to both the @code{Precondition} pragma -and the aspect @code{Precondition}. +and the aspect @code{Precondition}. Note that the identifiers for +pragmas Pre_Class and Post_Class are Pre'Class and Post'Class (not +Pre_Class and Post_Class), since these pragmas are intended to be +identical to the corresponding aspects). If the policy is @code{CHECK}, then assertions are enabled, i.e. the corresponding pragma or aspect is activated. @@ -5016,6 +5027,28 @@ Note that polling can also be enabled by use of the @option{-gnatP} switch. @xref{Switches for gcc,,, gnat_ugn, @value{EDITION} User's Guide}, for details. +@node Pragma Post +@unnumberedsec Pragma Post +@cindex Post +@cindex Checks, postconditions +@findex Postconditions +@noindent +Syntax: + +@smallexample @c ada +pragma Post (Boolean_Expression); +@end smallexample + +@noindent +The @code{Post} pragma is intended to be an exact replacement for +the language-defined +@code{Post} aspect, and shares its restrictions and semantics. +It must appear either immediately following the corresponding +subprogram declaration (only other pragmas may intervene), or +if there is no separate subprogram declaration, then it can +appear at the start of the declarations in a subprogram body +(preceded only by other pragmas). + @node Pragma Postcondition @unnumberedsec Pragma Postcondition @cindex Postcondition @@ -5173,6 +5206,69 @@ inlining (-gnatN option set) are accepted and legality-checked by the compiler, but are ignored at run-time even if postcondition checking is enabled. +Note that pragma @code{Postcondition} differs from the language-defined +@code{Post} aspect (and corresponding @code{Post} pragma) in allowing +multiple occurrences, allowing occurences in the body even if there +is a separate spec, and allowing a second string parameter, and the +use of the pragma identifier @code{Check}. Historically, pragma +@code{Postcondition} was implemented prior to the development of +Ada 2012, and has been retained in its original form for +compatibility purposes. + +@node Pragma Post_Class +@unnumberedsec Pragma Post_Class +@cindex Post +@cindex Checks, postconditions +@findex Postconditions +@noindent +Syntax: + +@smallexample @c ada +pragma Post_Class (Boolean_Expression); +@end smallexample + +@noindent +The @code{Post_Class} pragma is intended to be an exact replacement for +the language-defined +@code{Post'Class} aspect, and shares its restrictions and semantics. +It must appear either immediately following the corresponding +subprogram declaration (only other pragmas may intervene), or +if there is no separate subprogram declaration, then it can +appear at the start of the declarations in a subprogram body +(preceded only by other pragmas). + +Note: This pragma is called @code{Post_Class} rather than +@code{Post'Class} because the latter would not be strictly +conforming to the allowed syntax for pragmas. The motivation +for provinding pragmas equivalent to the aspects is to allow a program +to be written using the pragmas, and then compiled if necessary +using an Ada compiler that does not recognize the pragmas or +aspects, but is prepared to ignore the pragmas. The assertion +policy that controls this pragma is @code{Post'Class}, not +@code{Post_Class}. + +@node Pragma Pre +@unnumberedsec Pragma Pre +@cindex Pre +@cindex Checks, preconditions +@findex Preconditions +@noindent +Syntax: + +@smallexample @c ada +pragma Pre (Boolean_Expression); +@end smallexample + +@noindent +The @code{Pre} pragma is intended to be an exact replacement for +the language-defined +@code{Pre} aspect, and shares its restrictions and semantics. +It must appear either immediately following the corresponding +subprogram declaration (only other pragmas may intervene), or +if there is no separate subprogram declaration, then it can +appear at the start of the declarations in a subprogram body +(preceded only by other pragmas). + @node Pragma Precondition @unnumberedsec Pragma Precondition @cindex Preconditions @@ -5221,6 +5317,15 @@ inlining (-gnatN option set) are accepted and legality-checked by the compiler, but are ignored at run-time even if precondition checking is enabled. +Note that pragma @code{Precondition} differs from the language-defined +@code{Pre} aspect (and corresponding @code{Pre} pragma) in allowing +multiple occurrences, allowing occurences in the body even if there +is a separate spec, and allowing a second string parameter, and the +use of the pragma identifier @code{Check}. Historically, pragma +@code{Precondition} was implemented prior to the development of +Ada 2012, and has been retained in its original form for +compatibility purposes. + @node Pragma Predicate @unnumberedsec Pragma Predicate @findex Predicate @@ -5295,6 +5400,38 @@ equivalent to @code{pragma Prelaborate} when operating in later Ada versions. This is used to handle some cases where packages not previously preelaborable became so in Ada 2005. +@node Pragma Pre_Class +@unnumberedsec Pragma Pre_Class +@cindex Pre_Class +@cindex Checks, preconditions +@findex Preconditions +@noindent +Syntax: + +@smallexample @c ada +pragma Pre_Class (Boolean_Expression); +@end smallexample + +@noindent +The @code{Pre_Class} pragma is intended to be an exact replacement for +the language-defined +@code{Pre'Class} aspect, and shares its restrictions and semantics. +It must appear either immediately following the corresponding +subprogram declaration (only other pragmas may intervene), or +if there is no separate subprogram declaration, then it can +appear at the start of the declarations in a subprogram body +(preceded only by other pragmas). + +Note: This pragma is called @code{Pre_Class} rather than +@code{Pre'Class} because the latter would not be strictly +conforming to the allowed syntax for pragmas. The motivation +for providing pragmas equivalent to the aspects is to allow a program +to be written using the pragmas, and then compiled if necessary +using an Ada compiler that does not recognize the pragmas or +aspects, but is prepared to ignore the pragmas. The assertion +policy that controls this pragma is @code{Pre'Class}, not +@code{Pre_Class}. + @node Pragma Priority_Specific_Dispatching @unnumberedsec Pragma Priority_Specific_Dispatching @findex Priority_Specific_Dispatching diff --git a/gcc/ada/par-ch2.adb b/gcc/ada/par-ch2.adb index 224c63b7eb9..2218dacb17e 100644 --- a/gcc/ada/par-ch2.adb +++ b/gcc/ada/par-ch2.adb @@ -250,23 +250,15 @@ package body Ch2 is procedure Skip_Pragma_Semicolon is begin - if Token /= Tok_Semicolon then + -- If skipping the pragma, ignore a missing semicolon - -- If skipping the pragma, ignore a missing semicolon + if Token /= Tok_Semicolon and then Skipping then + null; - if Skipping then - null; - - -- Otherwise demand a semicolon - - else - T_Semicolon; - end if; - - -- Scan past semicolon if present + -- Otherwise demand a semicolon else - Scan; + T_Semicolon; end if; end Skip_Pragma_Semicolon; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index bf23bc7d609..aed45f96982 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1234,11 +1234,15 @@ begin Pragma_Preelaborable_Initialization | Pragma_Polling | Pragma_Persistent_BSS | + Pragma_Post | Pragma_Postcondition | + Pragma_Post_Class | + Pragma_Pre | Pragma_Precondition | Pragma_Predicate | Pragma_Preelaborate | Pragma_Preelaborate_05 | + Pragma_Pre_Class | Pragma_Priority | Pragma_Priority_Specific_Dispatching | Pragma_Profile | diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index aee35fbda3a..acf1aeb812b 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1995,7 +1995,6 @@ package body Sem_Ch6 is while Present (Prag) loop if Pragma_Name (Prag) = Name_Refined_Depends then Analyze_Refined_Depends_In_Decl_Part (Prag); - elsif Pragma_Name (Prag) = Name_Refined_Global then Has_Refined_Global := True; Analyze_Refined_Global_In_Decl_Part (Prag); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 4ef1867c112..4fbbfd73cf9 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -236,16 +236,6 @@ package body Sem_Prag is -- Get_SPARK_Mode_Id. Convert a name into a corresponding value of type -- SPARK_Mode_Id. - function Original_Name (N : Node_Id) return Name_Id; - -- N is a pragma node or aspect specification node. This function returns - -- the name of the pragma or aspect in original source form, taking into - -- account possible rewrites, and also cases where a pragma comes from an - -- aspect (in such cases, the name can be different from the pragma name, - -- e.g. a Pre aspect generates a Precondition pragma). This also deals with - -- the presence of 'Class, which results in one of the special names - -- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being - -- returned to represent the corresponding aspects with x'Class names. - procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id); -- Preanalyze the boolean expressions in the Requires and Ensures arguments -- of a Test_Case pragma if present (possibly Empty). We treat these as @@ -1979,6 +1969,13 @@ package body Sem_Prag is -- In this version of the procedure, the identifier name is given as -- a string with lower case letters. + procedure Check_Pre_Post; + -- Called to perform checks for Pre, Pre_Class, Post, Post_Class + -- pragmas. These are processed by transformation to equivalent + -- Precondition and Postcondition pragmas, but Pre and Post need an + -- additional check that they are not used in a subprogram body when + -- there is a separate spec present. + procedure Check_Precondition_Postcondition (In_Body : out Boolean); -- Called to process a precondition or postcondition pragma. There are -- three cases: @@ -3392,6 +3389,97 @@ package body Sem_Prag is Check_Optional_Identifier (Arg, Name_Find); end Check_Optional_Identifier; + -------------------- + -- Check_Pre_Post -- + -------------------- + + procedure Check_Pre_Post is + P : Node_Id; + PO : Node_Id; + + begin + if not Is_List_Member (N) then + Pragma_Misplaced; + end if; + + -- If we are within an inlined body, the legality of the pragma + -- has been checked already. + + if In_Inlined_Body then + return; + end if; + + -- Search prior declarations + + P := N; + while Present (Prev (P)) loop + P := Prev (P); + + -- If the previous node is a generic subprogram, do not go to to + -- the original node, which is the unanalyzed tree: we need to + -- attach the pre/postconditions to the analyzed version at this + -- point. They get propagated to the original tree when analyzing + -- the corresponding body. + + if Nkind (P) not in N_Generic_Declaration then + PO := Original_Node (P); + else + PO := P; + end if; + + -- Skip past prior pragma + + if Nkind (PO) = N_Pragma then + null; + + -- Skip stuff not coming from source + + elsif not Comes_From_Source (PO) then + + -- The condition may apply to a subprogram instantiation + + if Nkind (PO) = N_Subprogram_Declaration + and then Present (Generic_Parent (Specification (PO))) + then + return; + + elsif Nkind (PO) = N_Subprogram_Declaration + and then In_Instance + then + return; + + -- For all other cases of non source code, do nothing + + else + null; + end if; + + -- Only remaining possibility is subprogram declaration + + else + return; + end if; + end loop; + + -- If we fall through loop, pragma is at start of list, so see if it + -- is at the start of declarations of a subprogram body. + + PO := Parent (N); + + if Nkind (PO) = N_Subprogram_Body + and then List_Containing (N) = Declarations (PO) + then + -- This is only allowed if there is no separate specification + + if Present (Corresponding_Spec (PO)) then + Error_Pragma + ("pragma% must apply to subprogram specification"); + end if; + + return; + end if; + end Check_Pre_Post; + -------------------------------------- -- Check_Precondition_Postcondition -- -------------------------------------- @@ -3431,7 +3519,7 @@ package body Sem_Prag is -- compatibility with earlier uses of the Ada pragma, apply this -- rule only to aspect specifications. - -- The above discrpency needs documentation. Robert is dubious + -- The above discrepency needs documentation. Robert is dubious -- about whether it is a good idea ??? elsif Nkind (PO) = N_Subprogram_Declaration @@ -4286,7 +4374,7 @@ package body Sem_Prag is -- Get name from corresponding aspect - Error_Msg_Name_1 := Original_Name (N); + Error_Msg_Name_1 := Original_Aspect_Name (N); end if; end Fix_Error; @@ -8180,7 +8268,7 @@ package body Sem_Prag is -- Here to start processing for recognized pragma Prag_Id := Get_Pragma_Id (Pname); - Pname := Original_Name (N); + Pname := Original_Aspect_Name (N); -- Check applicable policy. We skip this if Is_Checked or Is_Ignored -- is already set, indicating that we have already checked the policy @@ -15056,6 +15144,32 @@ package body Sem_Prag is Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off); Polling_Required := (Chars (Get_Pragma_Arg (Arg1)) = Name_On); + ------------------ + -- Post[_Class] -- + ------------------ + + -- pragma Post (Boolean_EXPRESSION); + -- pragma Post_Class (Boolean_EXPRESSION); + + when Pragma_Post | Pragma_Post_Class => Post : declare + PC_Pragma : Node_Id; + + begin + GNAT_Pragma; + Check_At_Least_N_Arguments (1); + Check_At_Most_N_Arguments (1); + Check_No_Identifiers; + Check_Pre_Post; + + Set_Class_Present (N, Prag_Id = Pragma_Pre_Class); + PC_Pragma := New_Copy (N); + Set_Pragma_Identifier + (PC_Pragma, Make_Identifier (Loc, Name_Postcondition)); + Rewrite (N, PC_Pragma); + Set_Analyzed (N, False); + Analyze (N); + end Post; + ------------------- -- Postcondition -- ------------------- @@ -15090,6 +15204,32 @@ package body Sem_Prag is end if; end Postcondition; + ----------------- + -- Pre[_Class] -- + ----------------- + + -- pragma Pre (Boolean_EXPRESSION); + -- pragma Pre_Class (Boolean_EXPRESSION); + + when Pragma_Pre | Pragma_Pre_Class => Pre : declare + PC_Pragma : Node_Id; + + begin + GNAT_Pragma; + Check_At_Least_N_Arguments (1); + Check_At_Most_N_Arguments (1); + Check_No_Identifiers; + Check_Pre_Post; + + Set_Class_Present (N, Prag_Id = Pragma_Pre_Class); + PC_Pragma := New_Copy (N); + Set_Pragma_Identifier + (PC_Pragma, Make_Identifier (Loc, Name_Precondition)); + Rewrite (N, PC_Pragma); + Set_Analyzed (N, False); + Analyze (N); + end Pre; + ------------------ -- Precondition -- ------------------ @@ -18405,6 +18545,7 @@ package body Sem_Prag is Subp_Id : Entity_Id) is Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag)); + Nam : constant Name_Id := Original_Aspect_Name (Prag); Expr : Node_Id; Restore_Scope : Boolean := False; @@ -18540,14 +18681,37 @@ package body Sem_Prag is begin if not Present (T) then - Error_Msg_Name_1 := - Chars (Identifier (Corresponding_Aspect (Prag))); - Error_Msg_Name_2 := Name_Class; + -- Pre'Class/Post'Class aspect cases - Error_Msg_N - ("aspect `%''%` can only be specified for a primitive " - & "operation of a tagged type", Corresponding_Aspect (Prag)); + if From_Aspect_Specification (Prag) then + if Nam = Name_uPre then + Error_Msg_Name_1 := Name_Pre; + else + Error_Msg_Name_1 := Name_Post; + end if; + + Error_Msg_Name_2 := Name_Class; + + Error_Msg_N + ("aspect `%''%` can only be specified for a primitive " + & "operation of a tagged type", + Corresponding_Aspect (Prag)); + + -- Pre_Class, Post_Class pragma cases + + else + if Nam = Name_uPre then + Error_Msg_Name_1 := Name_Pre_Class; + else + Error_Msg_Name_1 := Name_Post_Class; + end if; + + Error_Msg_N + ("pragma% can only be specified for a primitive " + & "operation of a tagged type", + Corresponding_Aspect (Prag)); + end if; end if; Replace_Type (Get_Pragma_Arg (Arg1)); @@ -20073,7 +20237,7 @@ package body Sem_Prag is PP : Node_Id; Policy : Name_Id; - Ename : constant Name_Id := Original_Name (N); + Ename : constant Name_Id := Original_Aspect_Name (N); begin -- No effect if not valid assertion kind name @@ -20686,12 +20850,16 @@ package body Sem_Prag is Pragma_Passive => -1, Pragma_Persistent_BSS => 0, Pragma_Polling => -1, + Pragma_Post => -1, Pragma_Postcondition => -1, + Pragma_Post_Class => -1, + Pragma_Pre => -1, Pragma_Precondition => -1, Pragma_Predicate => -1, Pragma_Preelaborable_Initialization => -1, Pragma_Preelaborate => -1, Pragma_Preelaborate_05 => -1, + Pragma_Pre_Class => -1, Pragma_Priority => -1, Pragma_Priority_Specific_Dispatching => -1, Pragma_Profile => 0, @@ -21023,66 +21191,6 @@ package body Sem_Prag is end if; end Make_Aspect_For_PPC_In_Gen_Sub_Decl; - ------------------- - -- Original_Name -- - ------------------- - - function Original_Name (N : Node_Id) return Name_Id is - Pras : Node_Id; - Name : Name_Id; - - begin - pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma)); - Pras := N; - - if Is_Rewrite_Substitution (Pras) - and then Nkind (Original_Node (Pras)) = N_Pragma - then - Pras := Original_Node (Pras); - end if; - - -- Case where we came from aspect specication - - if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then - Pras := Corresponding_Aspect (Pras); - end if; - - -- Get name from aspect or pragma - - if Nkind (Pras) = N_Pragma then - Name := Pragma_Name (Pras); - else - Name := Chars (Identifier (Pras)); - end if; - - -- Deal with 'Class - - if Class_Present (Pras) then - case Name is - - -- Names that need converting to special _xxx form - - when Name_Pre => Name := Name_uPre; - when Name_Post => Name := Name_uPost; - when Name_Invariant => Name := Name_uInvariant; - when Name_Type_Invariant => Name := Name_uType_Invariant; - - -- Names already in special _xxx form (leave them alone) - - when Name_uPre => null; - when Name_uPost => null; - when Name_uInvariant => null; - when Name_uType_Invariant => null; - - -- Anything else is impossible with Class_Present set True - - when others => raise Program_Error; - end case; - end if; - - return Name; - end Original_Name; - ------------------------- -- Preanalyze_CTC_Args -- ------------------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 7a0341bf67c..80ba002a711 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -215,6 +215,7 @@ package body Sem_Util is procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is Items : constant Node_Id := Contract (Subp_Id); Nam : Name_Id; + N : Node_Id; begin -- The related subprogram [body] must have a contract and the item to be @@ -223,7 +224,7 @@ package body Sem_Util is pragma Assert (Present (Items)); pragma Assert (Nkind (Prag) = N_Pragma); - Nam := Pragma_Name (Prag); + Nam := Original_Aspect_Name (Prag); -- Contract items related to subprogram bodies @@ -241,7 +242,41 @@ package body Sem_Util is -- Contract items related to subprogram declarations else - if Nam_In (Nam, Name_Precondition, Name_Postcondition) then + if Nam_In (Nam, Name_Precondition, + Name_Postcondition, + Name_Pre, + Name_Post, + Name_uPre, + Name_uPost) + then + -- Before we add a precondition or postcondition to the list, + -- make sure we do not have a disallowed duplicate, which can + -- happen if we use a pragma for Pre{_Class] or Post[_Class] + -- instead of the corresponding aspect. + + if not From_Aspect_Specification (Prag) + and then Nam_In (Nam, Name_Pre_Class, + Name_Pre, + Name_uPre, + Name_Post_Class, + Name_Post, + Name_uPost) + then + N := Pre_Post_Conditions (Items); + while Present (N) loop + if not Split_PPC (N) + and then Original_Aspect_Name (N) = Nam + then + Error_Msg_Sloc := Sloc (N); + Error_Msg_NE + ("duplication of aspect for & given#", Prag, Subp_Id); + return; + else + N := Next_Pragma (N); + end if; + end loop; + end if; + Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); Set_Pre_Post_Conditions (Items, Prag); @@ -4411,7 +4446,6 @@ package body Sem_Util is procedure Ensure_Freeze_Node (E : Entity_Id) is FN : Node_Id; - begin if No (Freeze_Node (E)) then FN := Make_Freeze_Entity (Sloc (E)); @@ -4704,9 +4738,14 @@ package body Sem_Util is -- Inherited discriminants and components in derived record types are -- immediately visible. Itypes are not. + -- Unless the Itype is for a record type with a corresponding remote + -- type (what is that about, it was not commented ???) + if Ekind_In (Def_Id, E_Discriminant, E_Component) - or else (No (Corresponding_Remote_Type (Def_Id)) - and then not Is_Itype (Def_Id)) + or else + ((not Is_Record_Type (Def_Id) + or else No (Corresponding_Remote_Type (Def_Id))) + and then not Is_Itype (Def_Id)) then Set_Is_Immediately_Visible (Def_Id); Set_Current_Entity (Def_Id); @@ -12833,6 +12872,71 @@ package body Sem_Util is end if; end Object_Access_Level; + -------------------------- + -- Original_Aspect_Name -- + -------------------------- + + function Original_Aspect_Name (N : Node_Id) return Name_Id is + Pras : Node_Id; + Name : Name_Id; + + begin + pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma)); + Pras := N; + + if Is_Rewrite_Substitution (Pras) + and then Nkind (Original_Node (Pras)) = N_Pragma + then + Pras := Original_Node (Pras); + end if; + + -- Case where we came from aspect specication + + if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then + Pras := Corresponding_Aspect (Pras); + end if; + + -- Get name from aspect or pragma + + if Nkind (Pras) = N_Pragma then + Name := Pragma_Name (Pras); + else + Name := Chars (Identifier (Pras)); + end if; + + -- Deal with 'Class + + if Class_Present (Pras) then + case Name is + + -- Names that need converting to special _xxx form + + when Name_Pre | + Name_Pre_Class => + Name := Name_uPre; + + when Name_Post | + Name_Post_Class => + Name := Name_uPost; + + when Name_Invariant => + Name := Name_uInvariant; + + when Name_Type_Invariant | + Name_Type_Invariant_Class => + Name := Name_uType_Invariant; + + -- Nothing to do for other cases (e.g. a Check that derived + -- from Pre_Class and has the flag set). Also we do nothing + -- if the name is already in special _xxx form. + + when others => + null; + end case; + end if; + + return Name; + end Original_Aspect_Name; -------------------------------------- -- Original_Corresponding_Operation -- -------------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 621cb01d2d9..13ee3b3dbe3 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1365,6 +1365,16 @@ package Sem_Util is -- convenience, qualified expressions applied to object names are also -- allowed as actuals for this function. + function Original_Aspect_Name (N : Node_Id) return Name_Id; + -- N is a pragma node or aspect specification node. This function returns + -- the name of the pragma or aspect in original source form, taking into + -- account possible rewrites, and also cases where a pragma comes from an + -- aspect (in such cases, the name can be different from the pragma name, + -- e.g. a Pre aspect generates a Precondition pragma). This also deals with + -- the presence of 'Class, which results in one of the special names + -- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being + -- returned to represent the corresponding aspects with x'Class names. + function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean; -- Returns True if the names of both entities correspond with matching -- primitives. This routine includes support for the case in which one diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index ceb50f848cd..aacaf8a505f 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -142,11 +142,10 @@ package Snames is Name_Dimension : constant Name_Id := N + $; Name_Dimension_System : constant Name_Id := N + $; Name_Dynamic_Predicate : constant Name_Id := N + $; - Name_Post : constant Name_Id := N + $; - Name_Pre : constant Name_Id := N + $; Name_Static_Predicate : constant Name_Id := N + $; Name_Synchronization : constant Name_Id := N + $; Name_Type_Invariant : constant Name_Id := N + $; + Name_Type_Invariant_Class : constant Name_Id := N + $; -- Some special names used by the expander. Note that the lower case u's -- at the start of these names get translated to extra underscores. These @@ -562,12 +561,16 @@ package Snames is Name_Pack : constant Name_Id := N + $; Name_Page : constant Name_Id := N + $; Name_Passive : constant Name_Id := N + $; -- GNAT + Name_Post : constant Name_Id := N + $; -- GNAT Name_Postcondition : constant Name_Id := N + $; -- GNAT + Name_Post_Class : constant Name_Id := N + $; -- GNAT + Name_Pre : constant Name_Id := N + $; -- GNAT Name_Precondition : constant Name_Id := N + $; -- GNAT Name_Predicate : constant Name_Id := N + $; -- GNAT Name_Preelaborable_Initialization : constant Name_Id := N + $; -- Ada 05 Name_Preelaborate : constant Name_Id := N + $; Name_Preelaborate_05 : constant Name_Id := N + $; -- GNAT + Name_Pre_Class : constant Name_Id := N + $; -- GNAT -- Note: Priority is not in this list because its name matches the name of -- the corresponding attribute. However, it is included in the definition @@ -1860,12 +1863,16 @@ package Snames is Pragma_Pack, Pragma_Page, Pragma_Passive, + Pragma_Post, Pragma_Postcondition, + Pragma_Post_Class, + Pragma_Pre, Pragma_Precondition, Pragma_Predicate, Pragma_Preelaborable_Initialization, Pragma_Preelaborate, Pragma_Preelaborate_05, + Pragma_Pre_Class, Pragma_Psect_Object, Pragma_Pure, Pragma_Pure_05,