+2013-10-13 Robert Dewar <dewar@adacore.com>
+
+ * 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 <dewar@adacore.com>
+
+ * einfo.adb, sem_ch6.adb: Minor reformatting.
+
2013-10-13 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb: Add node/list usage for Refined_State
----------------
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;
* 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::
* 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::
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.
@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
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
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
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
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;
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 |
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);
-- 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
-- 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:
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 --
--------------------------------------
-- 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
-- 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;
-- 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
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 --
-------------------
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 --
------------------
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;
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));
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
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,
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 --
-------------------------
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
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
-- 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);
procedure Ensure_Freeze_Node (E : Entity_Id) is
FN : Node_Id;
-
begin
if No (Freeze_Node (E)) then
FN := Make_Freeze_Entity (Sloc (E));
-- 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);
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 --
--------------------------------------
-- 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
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
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
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,