[Ada] Malformed argument with pragma Refined_State

[Ada] Malformed argument with pragma Refined_State

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 512 bytes --]

This patch modifies the grammars of pragmas Abstract_State, Depends, Global,
Initializes, Refined_Depends, Refined_Global and Refined_State to explicitly
request a single argument. No need for a test as this is a documentation
enhancement.

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-11-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Update the grammars of pragmas
	Abstract_State, Depends, Global, Initializes, Refined_Depends,
	Refined_Global and Refined_State.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 3736 bytes --]

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 230522)
+++ sem_prag.adb	(working copy)
@@ -9998,7 +9998,7 @@
          --  ABSTRACT_STATE_LIST ::=
          --     null
          --  |  STATE_NAME_WITH_OPTIONS
-         --  | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} )
+         --  | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS})
 
          --  STATE_NAME_WITH_OPTIONS ::=
          --     STATE_NAME
@@ -10018,7 +10018,7 @@
 
          --  EXTERNAL_PROPERTY_LIST ::=
          --     EXTERNAL_PROPERTY
-         --  | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )
+         --  | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY})
 
          --  EXTERNAL_PROPERTY ::=
          --    Async_Readers    [=> boolean_EXPRESSION]
@@ -13412,8 +13412,8 @@
          --  pragma Depends (DEPENDENCY_RELATION);
 
          --  DEPENDENCY_RELATION ::=
-         --    null
-         --  | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
+         --     null
+         --  | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE})
 
          --  DEPENDENCY_CLAUSE ::=
          --    OUTPUT_LIST =>[+] INPUT_LIST
@@ -14945,9 +14945,9 @@
          --  pragma Global (GLOBAL_SPECIFICATION);
 
          --  GLOBAL_SPECIFICATION ::=
-         --    null
-         --  | GLOBAL_LIST
-         --  | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
+         --     null
+         --  | (GLOBAL_LIST)
+         --  | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST})
 
          --  MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
 
@@ -15689,20 +15689,18 @@
          -- Initializes --
          -----------------
 
-         --  pragma Initializes (INITIALIZATION_SPEC);
+         --  pragma Initializes (INITIALIZATION_LIST);
 
-         --  INITIALIZATION_SPEC ::= null | INITIALIZATION_LIST
-
          --  INITIALIZATION_LIST ::=
-         --    INITIALIZATION_ITEM
-         --    | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})
+         --     null
+         --  | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})
 
          --  INITIALIZATION_ITEM ::= name [=> INPUT_LIST]
 
          --  INPUT_LIST ::=
-         --    null
-         --    | INPUT
-         --    | (INPUT {, INPUT})
+         --     null
+         --  |  INPUT
+         --  | (INPUT {, INPUT})
 
          --  INPUT ::= name
 
@@ -19287,8 +19285,8 @@
          --  pragma Refined_Depends (DEPENDENCY_RELATION);
 
          --  DEPENDENCY_RELATION ::=
-         --    null
-         --  | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
+         --     null
+         --  | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE})
 
          --  DEPENDENCY_CLAUSE ::=
          --    OUTPUT_LIST =>[+] INPUT_LIST
@@ -19363,9 +19361,9 @@
          --  pragma Refined_Global (GLOBAL_SPECIFICATION);
 
          --  GLOBAL_SPECIFICATION ::=
-         --    null
-         --  | GLOBAL_LIST
-         --  | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
+         --     null
+         --  | (GLOBAL_LIST)
+         --  | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST})
 
          --  MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
 
@@ -19488,15 +19486,14 @@
          --  pragma Refined_State (REFINEMENT_LIST);
 
          --  REFINEMENT_LIST ::=
-         --    REFINEMENT_CLAUSE
-         --    | (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
+         --    (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
 
          --  REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST
 
          --  CONSTITUENT_LIST ::=
-         --    null
-         --    | CONSTITUENT
-         --    | (CONSTITUENT {, CONSTITUENT})
+         --     null
+         --  |  CONSTITUENT
+         --  | (CONSTITUENT {, CONSTITUENT})
 
          --  CONSTITUENT ::= object_NAME | state_NAME