diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2013-10-14 12:39:11 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-10-14 14:39:11 +0200 |
| commit | b447a7578e82b2d2bbe284fa3044f0070a2d8c12 (patch) | |
| tree | da081ec5a38918f14c64cc38c982a32170e93c1d /gcc | |
| parent | 577ee3a966170affb106f7a768f5253c692ef230 (diff) | |
| download | gcc-b447a7578e82b2d2bbe284fa3044f0070a2d8c12.zip gcc-b447a7578e82b2d2bbe284fa3044f0070a2d8c12.tar.gz gcc-b447a7578e82b2d2bbe284fa3044f0070a2d8c12.tar.bz2 | |
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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 11 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 2 |
3 files changed, 22 insertions, 11 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e5fcfac..b8277e9 100644 --- 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 30816d5..a2684f0 100644 --- 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 cca70eb..5254b57 100644 --- 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 + $; |