sem_prag.adb (Analyze_Global_In_Decl_Part): Remove local variable Contract_Seen.

2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Global_In_Decl_Part): Remove local
	variable Contract_Seen. Add local variable Proof_Seen.
	(Analyze_Global_List): Remove the processing for mode
	Contract_In. Add support for mode Proof_In.
	(Analyze_Pragma): Update the grammar of pragmas Global and
	Refined_Global.
	* snames.ads-tmpl: Remove predefined name Contract_In. Add
	predefined name Proof_In.

From-SVN: r203525

gcc/ada/ChangeLog

+2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Global_In_Decl_Part): Remove local
+	variable Contract_Seen. Add local variable Proof_Seen.
+	(Analyze_Global_List): Remove the processing for mode
+	Contract_In. Add support for mode Proof_In.
+	(Analyze_Pragma): Update the grammar of pragmas Global and
+	Refined_Global.
+	* snames.ads-tmpl: Remove predefined name Contract_In. Add
+	predefined name Proof_In.
+
 2013-10-14  Robert Dewar  <dewar@adacore.com>
 
 	* exp_prag.adb (Expand_Pragma_Check): Generate proper string

gcc/ada/sem_prag.adb

@@ -1350,10 +1350,10 @@ package body Sem_Prag is
       Subp_Id : Entity_Id;
       --  The entity of the subprogram subject to pragma Global
 
-      Contract_Seen : Boolean := False;
-      In_Out_Seen   : Boolean := False;
-      Input_Seen    : Boolean := False;
-      Output_Seen   : Boolean := False;
+      In_Out_Seen : Boolean := False;
+      Input_Seen  : Boolean := False;
+      Output_Seen : Boolean := False;
+      Proof_Seen  : Boolean := False;
       --  Flags used to verify the consistency of modes
 
       procedure Analyze_Global_List
@@ -1643,10 +1643,7 @@ package body Sem_Prag is
                   Mode := First (Choices (Assoc));
 
                   if Nkind (Mode) = N_Identifier then
-                     if Chars (Mode) = Name_Contract_In then
-                        Check_Duplicate_Mode (Mode, Contract_Seen);
-
-                     elsif Chars (Mode) = Name_In_Out then
+                     if Chars (Mode) = Name_In_Out then
                         Check_Duplicate_Mode (Mode, In_Out_Seen);
                         Check_Mode_Restriction_In_Function (Mode);
 
@@ -1657,6 +1654,9 @@ package body Sem_Prag is
                         Check_Duplicate_Mode (Mode, Output_Seen);
                         Check_Mode_Restriction_In_Function (Mode);
 
+                     elsif Chars (Mode) = Name_Proof_In then
+                        Check_Duplicate_Mode (Mode, Proof_Seen);
+
                      else
                         Error_Msg_N ("invalid mode selector", Mode);
                      end if;
@@ -12443,7 +12443,7 @@ package body Sem_Prag is
 
          --  MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
 
-         --  MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
+         --  MODE_SELECTOR ::= In_Out | Input | Output | Proof_In
          --  GLOBAL_LIST   ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
          --  GLOBAL_ITEM   ::= NAME
 
@@ -16650,7 +16650,7 @@ package body Sem_Prag is
 
          --  MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
 
-         --  MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
+         --  MODE_SELECTOR ::= In_Out | Input | Output | Proof_In
          --  GLOBAL_LIST   ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
          --  GLOBAL_ITEM   ::= NAME
 

gcc/ada/snames.ads-tmpl

@@ -694,7 +694,6 @@ package Snames is
    Name_Code                           : constant Name_Id := N + $;
    Name_Component                      : constant Name_Id := N + $;
    Name_Component_Size_4               : constant Name_Id := N + $;
-   Name_Contract_In                    : constant Name_Id := N + $;
    Name_Copy                           : constant Name_Id := N + $;
    Name_D_Float                        : constant Name_Id := N + $;
    Name_Decreases                      : constant Name_Id := N + $;
@@ -761,6 +760,7 @@ package Snames is
    Name_Policy                         : constant Name_Id := N + $;
    Name_Parameter_Types                : constant Name_Id := N + $;
    Name_Part_Of                        : constant Name_Id := N + $;
+   Name_Proof_In                       : constant Name_Id := N + $;
    Name_Reason                         : constant Name_Id := N + $;
    Name_Reference                      : constant Name_Id := N + $;
    Name_Requires                       : constant Name_Id := N + $;