This patch modifies the analysis of aspects Abstract_State, Initializes and Initial_Condition to ensure that they are inserted after pragma SPARK_Mode. The proper placement allows for SPARK_Mode to be analyzed first and dictate the mode of the related package.
------------ -- Source -- ------------ -- initializes_illegal_2.ads package Initializes_Illegal_2 with SPARK_Mode, Initializes => (S, X), Abstract_State => S is X : Integer; end Initializes_Illegal_2; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c initializes_illegal_2.ads initializes_illegal_2.ads:4:08: aspect "Abstract_State" cannot come after aspect "Initializes" Tested on x86_64-pc-linux-gnu, committed on trunk 2014-07-16 Hristian Kirtchev <kirtc...@adacore.com> * sem_ch13.adb (Insert_After_SPARK_Mode): Moved to the outer level of routine Analyze_Aspect_Specifications. Ensure that the corresponding pragmas of aspects Initial_Condition and Initializes are inserted after pragma SPARK_Mode.
Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 212640) +++ sem_ch13.adb (working copy) @@ -1158,6 +1158,15 @@ -- Establish the linkages between an aspect and its corresponding -- pragma. Flag Delayed should be set when both constructs are delayed. + procedure Insert_After_SPARK_Mode + (Prag : Node_Id; + Ins_Nod : Node_Id; + Decls : List_Id); + -- Subsidiary to the analysis of aspects Abstract_State, Initializes and + -- Initial_Condition. Insert node Prag before node Ins_Nod. If Ins_Nod + -- denotes pragma SPARK_Mode, then SPARK_Mode is skipped. Decls is the + -- associated declarative list where Prag is to reside. + procedure Insert_Delayed_Pragma (Prag : Node_Id); -- Insert a postcondition-like pragma into the tree depending on the -- context. Prag must denote one of the following: Pre, Post, Depends, @@ -1182,6 +1191,37 @@ Set_Parent (Prag, Asp); end Decorate_Aspect_And_Pragma; + ----------------------------- + -- Insert_After_SPARK_Mode -- + ----------------------------- + + procedure Insert_After_SPARK_Mode + (Prag : Node_Id; + Ins_Nod : Node_Id; + Decls : List_Id) + is + Decl : Node_Id := Ins_Nod; + + begin + -- Skip SPARK_Mode + + if Present (Decl) + and then Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Name_SPARK_Mode + then + Decl := Next (Decl); + end if; + + if Present (Decl) then + Insert_Before (Decl, Prag); + + -- Aitem acts as the last declaration + + else + Append_To (Decls, Prag); + end if; + end Insert_After_SPARK_Mode; + --------------------------- -- Insert_Delayed_Pragma -- --------------------------- @@ -2007,51 +2047,10 @@ -- immediately. when Aspect_Abstract_State => Abstract_State : declare - procedure Insert_After_SPARK_Mode - (Ins_Nod : Node_Id; - Decls : List_Id); - -- Insert Aitem before node Ins_Nod. If Ins_Nod denotes - -- pragma SPARK_Mode, then SPARK_Mode is skipped. Decls is - -- the associated declarative list where Aitem is to reside. - - ----------------------------- - -- Insert_After_SPARK_Mode -- - ----------------------------- - - procedure Insert_After_SPARK_Mode - (Ins_Nod : Node_Id; - Decls : List_Id) - is - Decl : Node_Id := Ins_Nod; - - begin - -- Skip SPARK_Mode - - if Present (Decl) - and then Nkind (Decl) = N_Pragma - and then Pragma_Name (Decl) = Name_SPARK_Mode - then - Decl := Next (Decl); - end if; - - if Present (Decl) then - Insert_Before (Decl, Aitem); - - -- Aitem acts as the last declaration - - else - Append_To (Decls, Aitem); - end if; - end Insert_After_SPARK_Mode; - - -- Local variables - Context : Node_Id := N; Decl : Node_Id; Decls : List_Id; - -- Start of processing for Abstract_State - begin -- When aspect Abstract_State appears on a generic package, -- it is propageted to the package instance. The context in @@ -2080,6 +2079,7 @@ -- inserted after the association renamings. if Present (Decls) then + Decl := First (Decls); -- The visible declarations of a generic instance have -- the following structure: @@ -2089,35 +2089,26 @@ -- <first source declaration> -- The pragma must be inserted before the first source - -- declaration. + -- declaration, skip the instance "header". if Is_Generic_Instance (Defining_Entity (Context)) then - - -- Skip the instance "header" - - Decl := First (Decls); while Present (Decl) and then not Comes_From_Source (Decl) loop Decl := Next (Decl); end loop; + end if; - -- Pragma Abstract_State must be inserted after - -- pragma SPARK_Mode in the tree. This ensures that - -- any error messages dependent on SPARK_Mode will - -- be properly enabled/suppressed. + -- Pragma Abstract_State must be inserted after pragma + -- SPARK_Mode in the tree. This ensures that any error + -- messages dependent on SPARK_Mode will be properly + -- enabled/suppressed. - Insert_After_SPARK_Mode (Decl, Decls); + Insert_After_SPARK_Mode + (Prag => Aitem, + Ins_Nod => Decl, + Decls => Decls); - -- The related package is not a generic instance, the - -- corresponding pragma must be the first declaration - -- except when SPARK_Mode is already in the list. In - -- that case pragma Abstract_State is placed second. - - else - Insert_After_SPARK_Mode (First (Decls), Decls); - end if; - -- Otherwise the pragma forms a new declarative list else @@ -2211,8 +2202,16 @@ Set_Visible_Declarations (Context, Decls); end if; - Prepend_To (Decls, Aitem); + -- When aspects Abstract_State, Initial_Condition and + -- Initializes are out of order, ensure that pragma + -- SPARK_Mode is always at the top of the declarative + -- list to properly enable/suppress errors. + Insert_After_SPARK_Mode + (Prag => Aitem, + Ins_Nod => First (Decls), + Decls => Decls); + else Error_Msg_NE ("aspect & must apply to a package declaration", @@ -2233,9 +2232,9 @@ Decls : List_Id; begin - -- When aspect Abstract_State appears on a generic package, - -- it is propageted to the package instance. The context in - -- this case is the instance spec. + -- When aspect Initializes appears on a generic package, + -- it is propageted to the package instance. The context + -- in this case is the instance spec. if Nkind (Context) = N_Package_Instantiation then Context := Instance_Spec (Context); @@ -2260,8 +2259,16 @@ Set_Visible_Declarations (Context, Decls); end if; - Prepend_To (Decls, Aitem); + -- When aspects Abstract_State, Initial_Condition and + -- Initializes are out of order, ensure that pragma + -- SPARK_Mode is always at the top of the declarative + -- list to properly enable/suppress errors. + Insert_After_SPARK_Mode + (Prag => Aitem, + Ins_Nod => First (Decls), + Decls => Decls); + else Error_Msg_NE ("aspect & must apply to a package declaration",