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",
