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