[multiple changes]
2014-07-16 Hristian Kirtchev <kirtchev@adacore.com> * exp_ch4.ads, exp_ch4.adb (Find_Hook_Context): Relocated to Exp_Util. * exp_ch7.adb (Process_Declarations): There is no need to check that a transient object being hooked is controlled as it would not have been hooked in the first place. * exp_ch9.adb Remove with and use clause for Exp_Ch4. * exp_util.adb (Find_Hook_Context): Relocated from Exp_Ch4. (Is_Aliased): A renaming of a transient controlled object is not considered aliasing when it occurs within an expression with actions. (Requires_Cleanup_Actions): There is no need to check that a transient object being hooked is controlled as it would not have been hooked in the first place. * exp_util.ads (Find_Hook_Context): Relocated from Exp_Ch4. 2014-07-16 Hristian Kirtchev <kirtchev@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. 2014-07-16 Ed Schonberg <schonberg@adacore.com> * sem_attr.adb (Analyze_Attribute, case 'Update): Handle properly a choice list with more than one choice, where each is an aggregate denoting a sequence of array indices for a multidimentional array. For SPARK use. From-SVN: r212646
This commit is contained in:
parent
8942b30c7c
commit
e59243faa1
@ -1,3 +1,33 @@
|
||||
2014-07-16 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* exp_ch4.ads, exp_ch4.adb (Find_Hook_Context): Relocated to Exp_Util.
|
||||
* exp_ch7.adb (Process_Declarations): There is no need to check
|
||||
that a transient object being hooked is controlled as it would
|
||||
not have been hooked in the first place.
|
||||
* exp_ch9.adb Remove with and use clause for Exp_Ch4.
|
||||
* exp_util.adb (Find_Hook_Context): Relocated from Exp_Ch4.
|
||||
(Is_Aliased): A renaming of a transient controlled object is
|
||||
not considered aliasing when it occurs within an expression
|
||||
with actions.
|
||||
(Requires_Cleanup_Actions): There is no need to
|
||||
check that a transient object being hooked is controlled as it
|
||||
would not have been hooked in the first place.
|
||||
* exp_util.ads (Find_Hook_Context): Relocated from Exp_Ch4.
|
||||
|
||||
2014-07-16 Hristian Kirtchev <kirtchev@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.
|
||||
|
||||
2014-07-16 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_attr.adb (Analyze_Attribute, case 'Update): Handle
|
||||
properly a choice list with more than one choice, where each
|
||||
is an aggregate denoting a sequence of array indices for a
|
||||
multidimentional array. For SPARK use.
|
||||
|
||||
2014-07-16 Vadim Godunko <godunko@adacore.com>
|
||||
|
||||
* a-coinho-shared.adb (Adjust): Create
|
||||
|
@ -11390,145 +11390,6 @@ package body Exp_Ch4 is
|
||||
Adjust_Result_Type (N, Typ);
|
||||
end Expand_Short_Circuit_Operator;
|
||||
|
||||
-----------------------
|
||||
-- Find_Hook_Context --
|
||||
-----------------------
|
||||
|
||||
function Find_Hook_Context (N : Node_Id) return Node_Id is
|
||||
Par : Node_Id;
|
||||
Top : Node_Id;
|
||||
|
||||
Wrapped_Node : Node_Id;
|
||||
-- Note: if we are in a transient scope, we want to reuse it as
|
||||
-- the context for actions insertion, if possible. But if N is itself
|
||||
-- part of the stored actions for the current transient scope,
|
||||
-- then we need to insert at the appropriate (inner) location in
|
||||
-- the not as an action on Node_To_Be_Wrapped.
|
||||
|
||||
In_Cond_Expr : constant Boolean := Within_Case_Or_If_Expression (N);
|
||||
|
||||
begin
|
||||
-- When the node is inside a case/if expression, the lifetime of any
|
||||
-- temporary controlled object is extended. Find a suitable insertion
|
||||
-- node by locating the topmost case or if expressions.
|
||||
|
||||
if In_Cond_Expr then
|
||||
Par := N;
|
||||
Top := N;
|
||||
while Present (Par) loop
|
||||
if Nkind_In (Original_Node (Par), N_Case_Expression,
|
||||
N_If_Expression)
|
||||
then
|
||||
Top := Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
-- The topmost case or if expression is now recovered, but it may
|
||||
-- still not be the correct place to add generated code. Climb to
|
||||
-- find a parent that is part of a declarative or statement list,
|
||||
-- and is not a list of actuals in a call.
|
||||
|
||||
Par := Top;
|
||||
while Present (Par) loop
|
||||
if Is_List_Member (Par)
|
||||
and then not Nkind_In (Par, N_Component_Association,
|
||||
N_Discriminant_Association,
|
||||
N_Parameter_Association,
|
||||
N_Pragma_Argument_Association)
|
||||
and then not Nkind_In
|
||||
(Parent (Par), N_Function_Call,
|
||||
N_Procedure_Call_Statement,
|
||||
N_Entry_Call_Statement)
|
||||
|
||||
then
|
||||
return Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
return Par;
|
||||
|
||||
else
|
||||
Par := N;
|
||||
while Present (Par) loop
|
||||
|
||||
-- Keep climbing past various operators
|
||||
|
||||
if Nkind (Parent (Par)) in N_Op
|
||||
or else Nkind_In (Parent (Par), N_And_Then, N_Or_Else)
|
||||
then
|
||||
Par := Parent (Par);
|
||||
else
|
||||
exit;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
Top := Par;
|
||||
|
||||
-- The node may be located in a pragma in which case return the
|
||||
-- pragma itself:
|
||||
|
||||
-- pragma Precondition (... and then Ctrl_Func_Call ...);
|
||||
|
||||
-- Similar case occurs when the node is related to an object
|
||||
-- declaration or assignment:
|
||||
|
||||
-- Obj [: Some_Typ] := ... and then Ctrl_Func_Call ...;
|
||||
|
||||
-- Another case to consider is when the node is part of a return
|
||||
-- statement:
|
||||
|
||||
-- return ... and then Ctrl_Func_Call ...;
|
||||
|
||||
-- Another case is when the node acts as a formal in a procedure
|
||||
-- call statement:
|
||||
|
||||
-- Proc (... and then Ctrl_Func_Call ...);
|
||||
|
||||
if Scope_Is_Transient then
|
||||
Wrapped_Node := Node_To_Be_Wrapped;
|
||||
else
|
||||
Wrapped_Node := Empty;
|
||||
end if;
|
||||
|
||||
while Present (Par) loop
|
||||
if Par = Wrapped_Node
|
||||
or else Nkind_In (Par, N_Assignment_Statement,
|
||||
N_Object_Declaration,
|
||||
N_Pragma,
|
||||
N_Procedure_Call_Statement,
|
||||
N_Simple_Return_Statement)
|
||||
then
|
||||
return Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
-- Return the topmost short circuit operator
|
||||
|
||||
return Top;
|
||||
end if;
|
||||
end Find_Hook_Context;
|
||||
|
||||
-------------------------------------
|
||||
-- Fixup_Universal_Fixed_Operation --
|
||||
-------------------------------------
|
||||
|
@ -103,11 +103,4 @@ package Exp_Ch4 is
|
||||
-- have special circuitry in Expand_N_Type_Conversion to promote both of
|
||||
-- the operands to type Integer.
|
||||
|
||||
function Find_Hook_Context (N : Node_Id) return Node_Id;
|
||||
-- Determine a suitable node on which to attach actions related to N
|
||||
-- that need to be elaborated unconditionally (i.e. in general the topmost
|
||||
-- expression of which N is a subexpression, which may or may not be
|
||||
-- evaluated, for example if N is the right operand of a short circuit
|
||||
-- operator).
|
||||
|
||||
end Exp_Ch4;
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -1825,8 +1825,6 @@ package body Exp_Ch7 is
|
||||
and then Present (Status_Flag_Or_Transient_Decl (Obj_Id))
|
||||
and then Nkind (Status_Flag_Or_Transient_Decl (Obj_Id)) =
|
||||
N_Object_Declaration
|
||||
and then Is_Finalizable_Transient
|
||||
(Status_Flag_Or_Transient_Decl (Obj_Id), Decl)
|
||||
then
|
||||
Processing_Actions (Has_No_Init => True);
|
||||
|
||||
|
@ -29,7 +29,6 @@ with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Ch3; use Exp_Ch3;
|
||||
with Exp_Ch4; use Exp_Ch4;
|
||||
with Exp_Ch6; use Exp_Ch6;
|
||||
with Exp_Ch11; use Exp_Ch11;
|
||||
with Exp_Dbug; use Exp_Dbug;
|
||||
|
@ -2598,6 +2598,145 @@ package body Exp_Util is
|
||||
raise Program_Error;
|
||||
end Find_Protection_Type;
|
||||
|
||||
-----------------------
|
||||
-- Find_Hook_Context --
|
||||
-----------------------
|
||||
|
||||
function Find_Hook_Context (N : Node_Id) return Node_Id is
|
||||
Par : Node_Id;
|
||||
Top : Node_Id;
|
||||
|
||||
Wrapped_Node : Node_Id;
|
||||
-- Note: if we are in a transient scope, we want to reuse it as
|
||||
-- the context for actions insertion, if possible. But if N is itself
|
||||
-- part of the stored actions for the current transient scope,
|
||||
-- then we need to insert at the appropriate (inner) location in
|
||||
-- the not as an action on Node_To_Be_Wrapped.
|
||||
|
||||
In_Cond_Expr : constant Boolean := Within_Case_Or_If_Expression (N);
|
||||
|
||||
begin
|
||||
-- When the node is inside a case/if expression, the lifetime of any
|
||||
-- temporary controlled object is extended. Find a suitable insertion
|
||||
-- node by locating the topmost case or if expressions.
|
||||
|
||||
if In_Cond_Expr then
|
||||
Par := N;
|
||||
Top := N;
|
||||
while Present (Par) loop
|
||||
if Nkind_In (Original_Node (Par), N_Case_Expression,
|
||||
N_If_Expression)
|
||||
then
|
||||
Top := Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
-- The topmost case or if expression is now recovered, but it may
|
||||
-- still not be the correct place to add generated code. Climb to
|
||||
-- find a parent that is part of a declarative or statement list,
|
||||
-- and is not a list of actuals in a call.
|
||||
|
||||
Par := Top;
|
||||
while Present (Par) loop
|
||||
if Is_List_Member (Par)
|
||||
and then not Nkind_In (Par, N_Component_Association,
|
||||
N_Discriminant_Association,
|
||||
N_Parameter_Association,
|
||||
N_Pragma_Argument_Association)
|
||||
and then not Nkind_In
|
||||
(Parent (Par), N_Function_Call,
|
||||
N_Procedure_Call_Statement,
|
||||
N_Entry_Call_Statement)
|
||||
|
||||
then
|
||||
return Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
return Par;
|
||||
|
||||
else
|
||||
Par := N;
|
||||
while Present (Par) loop
|
||||
|
||||
-- Keep climbing past various operators
|
||||
|
||||
if Nkind (Parent (Par)) in N_Op
|
||||
or else Nkind_In (Parent (Par), N_And_Then, N_Or_Else)
|
||||
then
|
||||
Par := Parent (Par);
|
||||
else
|
||||
exit;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
Top := Par;
|
||||
|
||||
-- The node may be located in a pragma in which case return the
|
||||
-- pragma itself:
|
||||
|
||||
-- pragma Precondition (... and then Ctrl_Func_Call ...);
|
||||
|
||||
-- Similar case occurs when the node is related to an object
|
||||
-- declaration or assignment:
|
||||
|
||||
-- Obj [: Some_Typ] := ... and then Ctrl_Func_Call ...;
|
||||
|
||||
-- Another case to consider is when the node is part of a return
|
||||
-- statement:
|
||||
|
||||
-- return ... and then Ctrl_Func_Call ...;
|
||||
|
||||
-- Another case is when the node acts as a formal in a procedure
|
||||
-- call statement:
|
||||
|
||||
-- Proc (... and then Ctrl_Func_Call ...);
|
||||
|
||||
if Scope_Is_Transient then
|
||||
Wrapped_Node := Node_To_Be_Wrapped;
|
||||
else
|
||||
Wrapped_Node := Empty;
|
||||
end if;
|
||||
|
||||
while Present (Par) loop
|
||||
if Par = Wrapped_Node
|
||||
or else Nkind_In (Par, N_Assignment_Statement,
|
||||
N_Object_Declaration,
|
||||
N_Pragma,
|
||||
N_Procedure_Call_Statement,
|
||||
N_Simple_Return_Statement)
|
||||
then
|
||||
return Par;
|
||||
|
||||
-- Prevent the search from going too far
|
||||
|
||||
elsif Is_Body_Or_Package_Declaration (Par) then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
-- Return the topmost short circuit operator
|
||||
|
||||
return Top;
|
||||
end if;
|
||||
end Find_Hook_Context;
|
||||
|
||||
----------------------
|
||||
-- Force_Evaluation --
|
||||
----------------------
|
||||
@ -4423,7 +4562,18 @@ package body Exp_Util is
|
||||
elsif Nkind (Stmt) = N_Object_Renaming_Declaration then
|
||||
Ren_Obj := Find_Renamed_Object (Stmt);
|
||||
|
||||
if Present (Ren_Obj) and then Ren_Obj = Trans_Id then
|
||||
if Present (Ren_Obj)
|
||||
and then Ren_Obj = Trans_Id
|
||||
|
||||
-- When the related context is an expression with actions,
|
||||
-- both the transient controlled object and its renaming are
|
||||
-- bound by the "scope" of the expression with actions. In
|
||||
-- other words, the two cannot be visible outside the scope,
|
||||
-- therefore the lifetime of the transient object is not
|
||||
-- really extended by the renaming.
|
||||
|
||||
and then Nkind (Rel_Node) /= N_Expression_With_Actions
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
end if;
|
||||
@ -7194,8 +7344,6 @@ package body Exp_Util is
|
||||
and then Present (Status_Flag_Or_Transient_Decl (Obj_Id))
|
||||
and then Nkind (Status_Flag_Or_Transient_Decl (Obj_Id)) =
|
||||
N_Object_Declaration
|
||||
and then Is_Finalizable_Transient
|
||||
(Status_Flag_Or_Transient_Decl (Obj_Id), Decl)
|
||||
then
|
||||
return True;
|
||||
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -445,6 +445,13 @@ package Exp_Util is
|
||||
-- Given a protected type or its corresponding record, find the type of
|
||||
-- field _object.
|
||||
|
||||
function Find_Hook_Context (N : Node_Id) return Node_Id;
|
||||
-- Determine a suitable node on which to attach actions related to N that
|
||||
-- need to be elaborated unconditionally. In general this is the topmost
|
||||
-- expression of which N is a subexpression, which in turn may or may not
|
||||
-- be evaluated, for example if N is the right operand of a short circuit
|
||||
-- operator.
|
||||
|
||||
procedure Force_Evaluation
|
||||
(Exp : Node_Id;
|
||||
Name_Req : Boolean := False);
|
||||
|
@ -6127,6 +6127,7 @@ package body Sem_Attr is
|
||||
|
||||
when Attribute_Update => Update : declare
|
||||
Comps : Elist_Id := No_Elist;
|
||||
Expr : Node_Id;
|
||||
|
||||
procedure Check_Component_Reference
|
||||
(Comp : Entity_Id;
|
||||
@ -6310,8 +6311,10 @@ package body Sem_Attr is
|
||||
-- Choice is a sequence of indexes for each dimension
|
||||
|
||||
else
|
||||
Expr := First (Choices (Assoc));
|
||||
while Present (Expr) loop
|
||||
Index_Type := First_Index (P_Type);
|
||||
Index := First (Expressions (First (Choices (Assoc))));
|
||||
Index := First (Expressions (Expr));
|
||||
while Present (Index_Type)
|
||||
and then Present (Index)
|
||||
loop
|
||||
@ -6324,6 +6327,9 @@ package body Sem_Attr is
|
||||
Error_Msg_N
|
||||
("dimension mismatch in index list", Assoc);
|
||||
end if;
|
||||
|
||||
Next (Expr);
|
||||
end loop;
|
||||
end if;
|
||||
end;
|
||||
|
||||
|
@ -1158,6 +1158,15 @@ package body Sem_Ch13 is
|
||||
-- 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 @@ package body Sem_Ch13 is
|
||||
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 @@ package body Sem_Ch13 is
|
||||
-- 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 @@ package body Sem_Ch13 is
|
||||
-- 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 @@ package body Sem_Ch13 is
|
||||
-- <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;
|
||||
|
||||
-- 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);
|
||||
|
||||
-- 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;
|
||||
|
||||
-- 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
|
||||
(Prag => Aitem,
|
||||
Ins_Nod => Decl,
|
||||
Decls => Decls);
|
||||
|
||||
-- Otherwise the pragma forms a new declarative list
|
||||
|
||||
else
|
||||
@ -2211,7 +2202,15 @@ package body Sem_Ch13 is
|
||||
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
|
||||
@ -2233,9 +2232,9 @@ package body Sem_Ch13 is
|
||||
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,7 +2259,15 @@ package body Sem_Ch13 is
|
||||
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
|
||||
|
Loading…
Reference in New Issue
Block a user