[multiple changes]

2013-10-14  Robert Dewar  <dewar@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): Generate proper string
	for invariant
	* gnat_rm.texi: Add documentation for pragmas
	Type_Invariant[_Class]
	* par-prag.adb: Add entries for pragmas Type_Invariant[_Class]
	* sem_ch13.adb: Minor reformatting
	* sem_prag.adb: Implement pragmas Type_Invariant[_Class]
	* snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class]

2013-10-14  Johannes Kanig  <kanig@adacore.com>

	* debug.adb: Release now unused debug switches that were only
	relevant for gnat2why backend, not the frontend
	* frontend.adb (Frontend) Do not stop when -gnatd.H is present,
	was unused

From-SVN: r203524

gcc/ada/ChangeLog

+2013-10-14  Robert Dewar  <dewar@adacore.com>
+
+	* exp_prag.adb (Expand_Pragma_Check): Generate proper string
+	for invariant
+	* gnat_rm.texi: Add documentation for pragmas
+	Type_Invariant[_Class]
+	* par-prag.adb: Add entries for pragmas Type_Invariant[_Class]
+	* sem_ch13.adb: Minor reformatting
+	* sem_prag.adb: Implement pragmas Type_Invariant[_Class]
+	* snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class]
+
+2013-10-14  Johannes Kanig  <kanig@adacore.com>
+
+	* debug.adb: Release now unused debug switches that were only
+	relevant for gnat2why backend, not the frontend
+	* frontend.adb (Frontend) Do not stop when -gnatd.H is present,
+	was unused
+
 2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Analyze_Global_Item): Allow

gcc/ada/debug.adb

@@ -125,16 +125,16 @@ package body Debug is
    --  d.E
    --  d.F  SPARK mode
    --  d.G  Frame condition mode for gnat2why
-   --  d.H  Standard package only mode for gnat2why
+   --  d.H
    --  d.I  Do not ignore enum representation clauses in CodePeer mode
    --  d.J  Disable parallel SCIL generation mode
-   --  d.K  SPARK check mode for gnat2why
+   --  d.K
    --  d.L  Depend on back end for limited types in if and case expressions
    --  d.M  Relaxed RM semantics
    --  d.N  Add node to all entities
    --  d.O  Dump internal SCO tables
    --  d.P  Previous (non-optimized) handling of length comparisons
-   --  d.Q  Flow Analysis mode for gnat2why
+   --  d.Q
    --  d.R  Restrictions in ali files in positional form
    --  d.S  Force Optimize_Alignment (Space)
    --  d.T  Force Optimize_Alignment (Time)
@@ -143,7 +143,7 @@ package body Debug is
    --  d.W  Print out debugging information for Walk_Library_Items
    --  d.X
    --  d.Y
-   --  d.Z  Dump flow analysis graphs, for debugging purposes (gnat2why)
+   --  d.Z
 
    --  d1   Error msgs have node numbers where possible
    --  d2   Eliminate error flags in verbose form error messages
@@ -596,7 +596,7 @@ package body Debug is
 
    --  d.D  SPARK strict mode. Interpret compiler permissions as strictly as
    --       possible in SPARK mode.
-
+   --
    --  d.F  SPARK mode. Generate AST in a form suitable for formal
    --       verification, as well as additional cross reference information in
    --       ALI files to compute effects of subprograms. Note that ALI files
@@ -606,10 +606,6 @@ package body Debug is
    --       generate Why code. Instead, it generates ALI files with an extra
    --       section which contains the effects of subprograms.
 
-   --  d.H  Standard package only mode for gnat2why. In this mode, gnat2why
-   --       will only generate Why code for package Standard. Any given input
-   --       file will be ignored.
-
    --  d.I  Do not ignore enum representation clauses in CodePeer mode.
    --       The default of ignoring representation clauses for enumeration
    --       types in CodePeer is good for the majority of Ada code, but in some
@@ -620,9 +616,6 @@ package body Debug is
    --       done in parallel to speed processing. This switch disables this
    --       behavior.
 
-   --  d.K  SPARK check mode for gnat2why. In this mode, gnat2why does not
-   --       generate Why code.
-
    --  d.L  Normally the front end generates special expansion for conditional
    --       expressions of a limited type. This debug flag removes this special
    --       case expansion, leaving it up to the back end to handle conditional
@@ -644,9 +637,6 @@ package body Debug is
    --       This is there in case we find a situation where the optimization
    --       malfunctions, to provide a work around.
 
-   --  d.Q  Flow Analysis mode for gnat2why. When this flag is given,
-   --       gnat2why will do flow analysis, and no translation to Why is done.
-
    --  d.R  As documented in lib-writ.ads, restrictions in the ali file can
    --       have two forms, positional and named. The named notation is the
    --       current preferred form, but the use of this debug switch will force
@@ -671,11 +661,6 @@ package body Debug is
    --       the order in which units are walked. This is primarily for use in
    --       debugging CodePeer mode.
 
-   --  d.Z  In gnat2why, in Flow analysis mode (-gnatd.Q), dump the different
-   --       graphs (control flow, control dependence) for debugging purposes.
-   --       This debug flag will be removed when flow analysis is sufficiently
-   --       stable.
-
    --  d.Y  Prevents the use of the N_Expression_With_Actions node even in the
    --       case of the gcc back end. Provided as a back up in case the new
    --       scheme has problems.

gcc/ada/exp_prag.adb

@@ -311,6 +311,10 @@ package body Exp_Prag is
       --  at" is omitted for name = Assertion, since it is redundant, given
       --  that the name of the exception is Assert_Failure.)
 
+      --  Also, instead of "XXX failed at", we generate slightly
+      --  different messages for some of the contract assertions (see
+      --  code below for details).
+
       --  An alternative expansion is used when the No_Exception_Propagation
       --  restriction is active and there is a local Assert_Failure handler.
       --  This is not a common combination of circumstances, but it occurs in
@@ -400,6 +404,15 @@ package body Exp_Prag is
                   Insert_Str_In_Name_Buffer ("failed ", 1);
                   Add_Str_To_Name_Buffer (" from ");
 
+               --  For special case of Invariant, the string is "failed
+               --  invariant from yy", to be consistent with the string that is
+               --  generated for the aspect case (the code later on checks for
+               --  this specific string to modify it in some cases, so this is
+               --  functionally important).
+
+               elsif Nam = Name_Invariant then
+                  Add_Str_To_Name_Buffer ("failed invariant from ");
+
                --  For all other checks, the string is "xxx failed at yyy"
                --  where xxx is the check name with current source file casing.
 

gcc/ada/frontend.adb

@@ -99,13 +99,6 @@ begin
 
    CStand.Create_Standard;
 
-   --  If the -gnatd.H flag is present, we are only interested in the Standard
-   --  package, so the frontend has done its job here.
-
-   if Debug_Flag_Dot_HH then
-      return;
-   end if;
-
    --  Check possible symbol definitions specified by -gnateD switches
 
    Prepcomp.Process_Command_Line_Symbol_Definitions;

gcc/ada/gnat_rm.texi

@@ -253,6 +253,8 @@ Implementation Defined Pragmas
 * Pragma Thread_Local_Storage::
 * Pragma Time_Slice::
 * Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
 * Pragma Unchecked_Union::
 * Pragma Unimplemented_Unit::
 * Pragma Universal_Aliasing ::
@@ -1073,6 +1075,8 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Thread_Local_Storage::
 * Pragma Time_Slice::
 * Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
 * Pragma Unchecked_Union::
 * Pragma Unimplemented_Unit::
 * Pragma Universal_Aliasing ::
@@ -5367,6 +5371,21 @@ subtype Q is R with
   Dynamic_Predicate => F(Q) or G(Q);
 @end smallexample
 
+Note that there is are no pragmas @code{Dynamic_Predicate}
+or @code{Static_Predicate}. That is
+because these pragmas would affect legality and semantics of
+the program and thus do not have a neutral effect if ignored.
+The motivation behind providing pragmas equivalent to
+corresponding aspects is to allow a program to be written
+using the pragmas, and then compiled with a compiler that
+will ignore the pragmas. That doesn't work in the case of
+static and dynamic predicates, since if the corresponding
+pragmas are ignored, then the behavior of the program is
+fundamentally changed (for example a membership test
+@code{A in B} would not take into account a predicate
+defined for subtype B). When following this approach, the
+use of predicates should be avoided.
+
 @node Pragma Preelaborable_Initialization
 @unnumberedsec Pragma Preelaborable_Initialization
 @findex Preelaborable_Initialization
@@ -6786,6 +6805,56 @@ for this pragma, i.e.@: the parameters may be given in any order if named
 notation is used, and named and positional notation can be mixed
 following the normal rules for procedure calls in Ada.
 
+@node Pragma Type_Invariant
+@unnumberedsec Pragma Type_Invariant
+@findex Invariant
+@findex Type_Invariant pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant
+  ([Entity =>] type_LOCAL_NAME,
+   [Check  =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant}
+aspect, and shares its restrictions and semantics. It differs
+from the language defined @code{Invariant} pragma in that it
+does not permit a string parameter, and it is
+controlled by the assertion identifier @code{Type_Invariant}
+rather than @code{Invariant}.
+
+@node Pragma Type_Invariant_Class
+@unnumberedsec Pragma Type_Invariant_Class
+@findex Invariant
+@findex Type_Invariant_Class pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant_Class
+  ([Entity =>] type_LOCAL_NAME,
+   [Check  =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant_Class} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant'Class}
+aspect, and shares its restrictions and semantics.
+
+Note: This pragma is called @code{Type_Invariant_Class} rather than
+@code{Type_Invariant'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{Type_Invariant'Class},
+not @code{Type_Invariant_Class}.
+
 @node Pragma Unchecked_Union
 @unnumberedsec Pragma Unchecked_Union
 @cindex Unions in C

gcc/ada/par-prag.adb

@@ -1293,6 +1293,8 @@ begin
            Pragma_Thread_Local_Storage           |
            Pragma_Time_Slice                     |
            Pragma_Title                          |
+           Pragma_Type_Invariant                 |
+           Pragma_Type_Invariant_Class           |
            Pragma_Unchecked_Union                |
            Pragma_Unimplemented_Unit             |
            Pragma_Universal_Aliasing             |

gcc/ada/sem_ch13.adb

@@ -5961,7 +5961,6 @@ package body Sem_Ch13 is
 
       if Present (SId) then
          PDecl := Unit_Declaration_Node (SId);
-
       else
          PDecl := Build_Invariant_Procedure_Declaration (Typ);
       end if;

gcc/ada/sem_prag.adb

@@ -846,7 +846,7 @@ package body Sem_Prag is
 
          if Is_Input then
             if (Ekind (Item_Id) = E_Out_Parameter
-                  and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
+                 and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
               or else
                (Global_Seen and then not Appears_In (Subp_Inputs, Item_Id))
             then
@@ -11772,7 +11772,6 @@ package body Sem_Prag is
                 Name_Link_Name));
 
             Check_At_Least_N_Arguments (2);
-
             Check_At_Most_N_Arguments  (4);
             Process_Convention (C, Def_Id);
 
@@ -13716,7 +13715,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (2);
-            Check_At_Most_N_Arguments (3);
+            Check_At_Most_N_Arguments  (3);
             Check_Optional_Identifier (Arg1, Name_Entity);
             Check_Optional_Identifier (Arg2, Name_Check);
 
@@ -15316,7 +15315,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments (2);
+            Check_At_Most_N_Arguments  (2);
 
             --  Process first argument
 
@@ -15700,11 +15699,13 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments (1);
+            Check_Arg_Count (1);
             Check_No_Identifiers;
             Check_Pre_Post;
 
+            --  Rewrite Post[_Class] pragma as Precondition pragma setting the
+            --  flag Class_Present to True for the Post_Class case.
+
             Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
             PC_Pragma := New_Copy (N);
             Set_Pragma_Identifier
@@ -15760,11 +15761,13 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments (1);
+            Check_Arg_Count (1);
             Check_No_Identifiers;
             Check_Pre_Post;
 
+            --  Rewrite Pre[_Class] pragma as Precondition pragma setting the
+            --  flag Class_Present to True for the Pre_Class case.
+
             Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
             PC_Pragma := New_Copy (N);
             Set_Pragma_Identifier
@@ -15787,7 +15790,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments (2);
+            Check_At_Most_N_Arguments  (2);
             Check_Optional_Identifier (Arg1, Name_Check);
             Check_Precondition_Postcondition (In_Body);
 
@@ -18317,6 +18320,34 @@ package body Sem_Prag is
             end loop;
          end Title;
 
+         ----------------------------
+         -- Type_Invariant[_Class] --
+         ----------------------------
+
+         --  pragma Type_Invariant[_Class]
+         --    ([Entity =>] type_LOCAL_NAME,
+         --     [Check  =>] EXPRESSION);
+
+         when Pragma_Type_Invariant       |
+              Pragma_Type_Invariant_Class =>
+         Type_Invariant : declare
+            I_Pragma : Node_Id;
+
+         begin
+            Check_Arg_Count (2);
+
+            --  Rewrite Type_Invariant[_Class] pragma as an Invariant pragma,
+            --  setting Class_Present for the Type_Invariant_Class case.
+
+            Set_Class_Present (N, Prag_Id = Pragma_Type_Invariant_Class);
+            I_Pragma := New_Copy (N);
+            Set_Pragma_Identifier
+              (I_Pragma, Make_Identifier (Loc, Name_Invariant));
+            Rewrite (N, I_Pragma);
+            Set_Analyzed (N, False);
+            Analyze (N);
+         end Type_Invariant;
+
          ---------------------
          -- Unchecked_Union --
          ---------------------
@@ -21493,6 +21524,8 @@ package body Sem_Prag is
       Pragma_Thread_Local_Storage           =>  0,
       Pragma_Time_Slice                     => -1,
       Pragma_Title                          => -1,
+      Pragma_Type_Invariant                 => -1,
+      Pragma_Type_Invariant_Class           => -1,
       Pragma_Unchecked_Union                =>  0,
       Pragma_Unimplemented_Unit             => -1,
       Pragma_Universal_Aliasing             => -1,

gcc/ada/snames.ads-tmpl

@@ -144,8 +144,6 @@ package Snames is
    Name_Dynamic_Predicate              : 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
@@ -448,7 +446,7 @@ package Snames is
    Name_Wide_Character_Encoding        : constant Name_Id := N + $; -- GNAT
    Last_Configuration_Pragma_Name      : constant Name_Id := N + $;
 
-   --  Remaining pragma names
+   --  Remaining pragma names (non-configuration pragmas)
 
    Name_Abort_Defer                    : constant Name_Id := N + $; -- GNAT
    Name_Abstract_State                 : constant Name_Id := N + $; -- GNAT
@@ -621,6 +619,8 @@ package Snames is
    Name_Thread_Local_Storage           : constant Name_Id := N + $; -- GNAT
    Name_Time_Slice                     : constant Name_Id := N + $; -- GNAT
    Name_Title                          : constant Name_Id := N + $; -- GNAT
+   Name_Type_Invariant                 : constant Name_Id := N + $; -- GNAT
+   Name_Type_Invariant_Class           : constant Name_Id := N + $; -- GNAT
    Name_Unchecked_Union                : constant Name_Id := N + $; -- Ada 05
    Name_Unimplemented_Unit             : constant Name_Id := N + $; -- GNAT
    Name_Universal_Aliasing             : constant Name_Id := N + $; -- GNAT
@@ -1905,6 +1905,8 @@ package Snames is
       Pragma_Thread_Local_Storage,
       Pragma_Time_Slice,
       Pragma_Title,
+      Pragma_Type_Invariant,
+      Pragma_Type_Invariant_Class,
       Pragma_Unchecked_Union,
       Pragma_Unimplemented_Unit,
       Pragma_Universal_Aliasing,