===================================================================
@@ -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
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.