gnat_rm.texi: Add documentation for pragmas Pre[_Class] Post[_Class].

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.

From-SVN: r203505

gcc/ada/ChangeLog

+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

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;

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

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;
 

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                        |

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);

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 --
    --------------------------------------

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

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,