[Ada] Syntax error detection on Ghost abstract states

[Ada] Syntax error detection on Ghost abstract states

[Arnaud Charlet]

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

This patch modifies the analysis of pragma Abstract_State to detect a syntax
error related to a state with a simple option.

------------
-- Source --
------------

--  malformed_state.ads

package Malformed_State
  with SPARK_Mode,
       Abstract_State => (State1, State2 => Ghost)
is
end Malformed_State;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c malformed_state.ads
malformed_state.ads:3:42: malformed abstract state declaration
malformed_state.ads:3:42: use "with" to specify simple option

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

2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Abstract_State): Use routine
	Malformed_State_Error to issue general errors.
	(Analyze_Pragma): Diagnose a syntax error related to a state
	declaration with a simple option.
	(Malformed_State_Error): New routine.


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

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 221175)
+++ sem_prag.adb	(working copy)
@@ -9526,6 +9526,12 @@
             --  visibility chain. Pack_Id denotes the entity or the related
             --  package where pragma Abstract_State appears.
 
+            procedure Malformed_State_Error (State : Node_Id);
+            --  Emit an error concerning the illegal declaration of abstract
+            --  state State. This routine diagnoses syntax errors that lead to
+            --  a different parse tree. The error is issued regardless of the
+            --  SPARK mode in effect.
+
             ----------------------------
             -- Analyze_Abstract_State --
             ----------------------------
@@ -10059,11 +10065,10 @@
                      Next (Opt);
                   end loop;
 
-               --  Any other attempt to declare a state is illegal. This is a
-               --  syntax error, always report.
+               --  Any other attempt to declare a state is illegal
 
                else
-                  Error_Msg_N ("malformed abstract state declaration", State);
+                  Malformed_State_Error (State);
                   return;
                end if;
 
@@ -10096,11 +10101,29 @@
                end if;
             end Analyze_Abstract_State;
 
+            ---------------------------
+            -- Malformed_State_Error --
+            ---------------------------
+
+            procedure Malformed_State_Error (State : Node_Id) is
+            begin
+               Error_Msg_N ("malformed abstract state declaration", State);
+
+               --  An abstract state with a simple option is being declared
+               --  with "=>" rather than the legal "with". The state appears
+               --  as a component association.
+
+               if Nkind (State) = N_Component_Association then
+                  Error_Msg_N ("\\use WITH to specify simple option", State);
+               end if;
+            end Malformed_State_Error;
+
             --  Local variables
 
             Pack_Decl : Node_Id;
             Pack_Id   : Entity_Id;
             State     : Node_Id;
+            States    : Node_Id;
 
          --  Start of processing for Abstract_State
 
@@ -10137,22 +10160,34 @@
                Set_Is_Ghost_Entity (Pack_Id);
             end if;
 
-            State := Expression (Get_Argument (N));
+            States := Expression (Get_Argument (N));
 
             --  Multiple non-null abstract states appear as an aggregate
 
-            if Nkind (State) = N_Aggregate then
-               State := First (Expressions (State));
+            if Nkind (States) = N_Aggregate then
+               State := First (Expressions (States));
                while Present (State) loop
                   Analyze_Abstract_State (State, Pack_Id);
                   Next (State);
                end loop;
 
+               --  An abstract state with a simple option is being illegaly
+               --  declared with "=>" rather than "with". In this case the
+               --  state declaration appears as a component association.
+
+               if Present (Component_Associations (States)) then
+                  State := First (Component_Associations (States));
+                  while Present (State) loop
+                     Malformed_State_Error (State);
+                     Next (State);
+                  end loop;
+               end if;
+
             --  Various forms of a single abstract state. Note that these may
             --  include malformed state declarations.
 
             else
-               Analyze_Abstract_State (State, Pack_Id);
+               Analyze_Abstract_State (States, Pack_Id);
             end if;
 
             --  Save the pragma for retrieval by other tools