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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e5fcfaca1bdc39d62321ec062c47d72343189f9b..b8277e96cb65e9de1feb6a9698bcc3a703679400 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,14 @@
+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

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 30816d5ee0e3760d899dc50afa8ae10a468c8b67..a2684f0a20cf4a01576e9a10aa6750f1b8f278bf 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/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
 

diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index cca70eb9a7c09122e60faa808d5111cc7c8d89a9..5254b57b36605ce73c02cde692ece1d1c2a7e322 100644 (file)
--- a/gcc/ada/snames.ads-tmpl
+++ b/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 + $;