[multiple changes]
2014-07-17 Robert Dewar <dewar@adacore.com> * sem_aux.ads: Minor comment addition. 2014-07-17 Ed Schonberg <schonberg@adacore.com> * sem_res.adb (Make_Call_Into_Operator): If the call is already a rewriting of an operator node, there are no actuals to be propagated from original node to rewritten node when in ASIS mode. 2014-07-17 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch6.adb (Analyze_Subprogram_Body_Contract, Analyze_Subprogram_Contract): Add new local variable Mode. Save and restore the SPARK mode of the related construct in a stack-like fashion. * sem_ch7.adb (Analyze_Package_Body_Contract, Analyze_Package_Contract): Add new local variable Mode. Save and restore the SPARK mode of the related construct in a stack-like fashion. * sem_util.adb Remove with and use clause for Opt. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): New routine. * sem_util.ads Add with and use clause for Opt. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): New routine. 2014-07-17 Hristian Kirtchev <kirtchev@adacore.com> * exp_util.adb (Is_Aliased): Transient objects within an expression with actions cannot be considered aliased. From-SVN: r212721
This commit is contained in:
parent
3629577991
commit
c61ef4169e
@ -1,3 +1,34 @@
|
|||||||
|
2014-07-17 Robert Dewar <dewar@adacore.com>
|
||||||
|
|
||||||
|
* sem_aux.ads: Minor comment addition.
|
||||||
|
|
||||||
|
2014-07-17 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
|
* sem_res.adb (Make_Call_Into_Operator): If the call is already
|
||||||
|
a rewriting of an operator node, there are no actuals to be
|
||||||
|
propagated from original node to rewritten node when in ASIS mode.
|
||||||
|
|
||||||
|
2014-07-17 Hristian Kirtchev <kirtchev@adacore.com>
|
||||||
|
|
||||||
|
* sem_ch6.adb (Analyze_Subprogram_Body_Contract,
|
||||||
|
Analyze_Subprogram_Contract): Add new local variable Mode. Save
|
||||||
|
and restore the SPARK mode of the related construct in a
|
||||||
|
stack-like fashion.
|
||||||
|
* sem_ch7.adb (Analyze_Package_Body_Contract,
|
||||||
|
Analyze_Package_Contract): Add new local variable Mode. Save and
|
||||||
|
restore the SPARK mode of the related construct in a stack-like fashion.
|
||||||
|
* sem_util.adb Remove with and use clause for Opt.
|
||||||
|
(Restore_SPARK_Mode): New routine.
|
||||||
|
(Save_SPARK_Mode_And_Set): New routine.
|
||||||
|
* sem_util.ads Add with and use clause for Opt.
|
||||||
|
(Restore_SPARK_Mode): New routine.
|
||||||
|
(Save_SPARK_Mode_And_Set): New routine.
|
||||||
|
|
||||||
|
2014-07-17 Hristian Kirtchev <kirtchev@adacore.com>
|
||||||
|
|
||||||
|
* exp_util.adb (Is_Aliased): Transient objects
|
||||||
|
within an expression with actions cannot be considered aliased.
|
||||||
|
|
||||||
2014-07-17 Thomas Quinot <quinot@adacore.com>
|
2014-07-17 Thomas Quinot <quinot@adacore.com>
|
||||||
|
|
||||||
* sem.ads (Scope_Stack_Entry): Reorganize storage of action lists;
|
* sem.ads (Scope_Stack_Entry): Reorganize storage of action lists;
|
||||||
|
@ -4557,6 +4557,15 @@ package body Exp_Util is
|
|||||||
-- Start of processing for Is_Aliased
|
-- Start of processing for Is_Aliased
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
-- Aliasing in expression with actions does not matter because the
|
||||||
|
-- scope of the transient object is always limited by the scope of
|
||||||
|
-- the EWA. Such objects are always hooked and always finalized at
|
||||||
|
-- the end of the EWA's scope.
|
||||||
|
|
||||||
|
if Nkind (Rel_Node) = N_Expression_With_Actions then
|
||||||
|
return False;
|
||||||
|
end if;
|
||||||
|
|
||||||
Stmt := First_Stmt;
|
Stmt := First_Stmt;
|
||||||
while Present (Stmt) loop
|
while Present (Stmt) loop
|
||||||
if Nkind (Stmt) = N_Object_Declaration then
|
if Nkind (Stmt) = N_Object_Declaration then
|
||||||
@ -7343,7 +7352,7 @@ package body Exp_Util is
|
|||||||
elsif Is_Access_Type (Obj_Typ)
|
elsif Is_Access_Type (Obj_Typ)
|
||||||
and then Present (Status_Flag_Or_Transient_Decl (Obj_Id))
|
and then Present (Status_Flag_Or_Transient_Decl (Obj_Id))
|
||||||
and then Nkind (Status_Flag_Or_Transient_Decl (Obj_Id)) =
|
and then Nkind (Status_Flag_Or_Transient_Decl (Obj_Id)) =
|
||||||
N_Object_Declaration
|
N_Object_Declaration
|
||||||
and then Is_Finalizable_Transient
|
and then Is_Finalizable_Transient
|
||||||
(Status_Flag_Or_Transient_Decl (Obj_Id), Decl)
|
(Status_Flag_Or_Transient_Decl (Obj_Id), Decl)
|
||||||
then
|
then
|
||||||
|
@ -255,6 +255,12 @@ package Sem_Aux is
|
|||||||
-- Defined in tagged types. Set if an External_Tag rep. clause has been
|
-- Defined in tagged types. Set if an External_Tag rep. clause has been
|
||||||
-- given for this type. Use to avoid the generation of the default
|
-- given for this type. Use to avoid the generation of the default
|
||||||
-- External_Tag.
|
-- External_Tag.
|
||||||
|
--
|
||||||
|
-- Note: we used to use an entity flag for this purpose, but that was wrong
|
||||||
|
-- because it was not propagated from the private view to the full view. We
|
||||||
|
-- could have added that propagation, but it would have been an annoying
|
||||||
|
-- irregularity compared to other representation aspects, and the cost of
|
||||||
|
-- looking up the aspect when needed is small.
|
||||||
|
|
||||||
function Has_Unconstrained_Elements (T : Entity_Id) return Boolean;
|
function Has_Unconstrained_Elements (T : Entity_Id) return Boolean;
|
||||||
-- True if T has discriminants and is unconstrained, or is an array type
|
-- True if T has discriminants and is unconstrained, or is an array type
|
||||||
|
@ -2033,12 +2033,15 @@ package body Sem_Ch6 is
|
|||||||
|
|
||||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
|
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
|
||||||
Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
|
Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
|
||||||
|
Mode : SPARK_Mode_Type;
|
||||||
Prag : Node_Id;
|
Prag : Node_Id;
|
||||||
Ref_Depends : Node_Id := Empty;
|
Ref_Depends : Node_Id := Empty;
|
||||||
Ref_Global : Node_Id := Empty;
|
Ref_Global : Node_Id := Empty;
|
||||||
Spec_Id : Entity_Id;
|
Spec_Id : Entity_Id;
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||||
|
|
||||||
-- When a subprogram body declaration is illegal, its defining entity is
|
-- When a subprogram body declaration is illegal, its defining entity is
|
||||||
-- left unanalyzed. There is nothing left to do in this case because the
|
-- left unanalyzed. There is nothing left to do in this case because the
|
||||||
-- body lacks a contract, or even a proper Ekind.
|
-- body lacks a contract, or even a proper Ekind.
|
||||||
@ -2112,6 +2115,8 @@ package body Sem_Ch6 is
|
|||||||
Body_Decl, Spec_Id);
|
Body_Decl, Spec_Id);
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
Restore_SPARK_Mode (Mode);
|
||||||
end Analyze_Subprogram_Body_Contract;
|
end Analyze_Subprogram_Body_Contract;
|
||||||
|
|
||||||
------------------------------------
|
------------------------------------
|
||||||
@ -3680,6 +3685,7 @@ package body Sem_Ch6 is
|
|||||||
Case_Prag : Node_Id := Empty;
|
Case_Prag : Node_Id := Empty;
|
||||||
Depends : Node_Id := Empty;
|
Depends : Node_Id := Empty;
|
||||||
Global : Node_Id := Empty;
|
Global : Node_Id := Empty;
|
||||||
|
Mode : SPARK_Mode_Type;
|
||||||
Nam : Name_Id;
|
Nam : Name_Id;
|
||||||
Post_Prag : Node_Id := Empty;
|
Post_Prag : Node_Id := Empty;
|
||||||
Prag : Node_Id;
|
Prag : Node_Id;
|
||||||
@ -3687,6 +3693,8 @@ package body Sem_Ch6 is
|
|||||||
Seen_In_Post : Boolean := False;
|
Seen_In_Post : Boolean := False;
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
Save_SPARK_Mode_And_Set (Subp, Mode);
|
||||||
|
|
||||||
if Present (Items) then
|
if Present (Items) then
|
||||||
|
|
||||||
-- Analyze pre- and postconditions
|
-- Analyze pre- and postconditions
|
||||||
@ -3808,6 +3816,8 @@ package body Sem_Ch6 is
|
|||||||
("function postcondition does not mention result?T?", Post_Prag);
|
("function postcondition does not mention result?T?", Post_Prag);
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
Restore_SPARK_Mode (Mode);
|
||||||
end Analyze_Subprogram_Contract;
|
end Analyze_Subprogram_Contract;
|
||||||
|
|
||||||
------------------------------------
|
------------------------------------
|
||||||
|
@ -180,9 +180,12 @@ package body Sem_Ch7 is
|
|||||||
|
|
||||||
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
|
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
|
||||||
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
|
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
|
||||||
|
Mode : SPARK_Mode_Type;
|
||||||
Prag : Node_Id;
|
Prag : Node_Id;
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||||
|
|
||||||
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
|
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
|
||||||
|
|
||||||
-- The analysis of pragma Refined_State detects whether the spec has
|
-- The analysis of pragma Refined_State detects whether the spec has
|
||||||
@ -200,6 +203,8 @@ package body Sem_Ch7 is
|
|||||||
then
|
then
|
||||||
Error_Msg_N ("package & requires state refinement", Spec_Id);
|
Error_Msg_N ("package & requires state refinement", Spec_Id);
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
Restore_SPARK_Mode (Mode);
|
||||||
end Analyze_Package_Body_Contract;
|
end Analyze_Package_Body_Contract;
|
||||||
|
|
||||||
---------------------------------
|
---------------------------------
|
||||||
@ -839,9 +844,12 @@ package body Sem_Ch7 is
|
|||||||
------------------------------
|
------------------------------
|
||||||
|
|
||||||
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
|
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
|
||||||
|
Mode : SPARK_Mode_Type;
|
||||||
Prag : Node_Id;
|
Prag : Node_Id;
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
Save_SPARK_Mode_And_Set (Pack_Id, Mode);
|
||||||
|
|
||||||
-- Analyze the initialization related pragmas. Initializes must come
|
-- Analyze the initialization related pragmas. Initializes must come
|
||||||
-- before Initial_Condition due to item dependencies.
|
-- before Initial_Condition due to item dependencies.
|
||||||
|
|
||||||
@ -867,6 +875,8 @@ package body Sem_Ch7 is
|
|||||||
Check_Missing_Part_Of (Pack_Id);
|
Check_Missing_Part_Of (Pack_Id);
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
Restore_SPARK_Mode (Mode);
|
||||||
end Analyze_Package_Contract;
|
end Analyze_Package_Contract;
|
||||||
|
|
||||||
---------------------------------
|
---------------------------------
|
||||||
|
@ -1564,9 +1564,13 @@ package body Sem_Res is
|
|||||||
-- the call has already been constant-folded, nothing to do. We
|
-- the call has already been constant-folded, nothing to do. We
|
||||||
-- relocate the operand nodes rather than copy them, to preserve
|
-- relocate the operand nodes rather than copy them, to preserve
|
||||||
-- original_node pointers, given that the operands themselves may
|
-- original_node pointers, given that the operands themselves may
|
||||||
-- have been rewritten.
|
-- have been rewritten. If the call was itself a rewriting of an
|
||||||
|
-- operator node, nothing to do.
|
||||||
|
|
||||||
if ASIS_Mode and then Nkind (N) in N_Op then
|
if ASIS_Mode
|
||||||
|
and then Nkind (N) in N_Op
|
||||||
|
and then Nkind (Original_Node (N)) = N_Function_Call
|
||||||
|
then
|
||||||
if Is_Binary then
|
if Is_Binary then
|
||||||
Rewrite (First (Parameter_Associations (Original_Node (N))),
|
Rewrite (First (Parameter_Associations (Original_Node (N))),
|
||||||
Relocate_Node (Left_Opnd (N)));
|
Relocate_Node (Left_Opnd (N)));
|
||||||
|
@ -41,7 +41,6 @@ with Namet.Sp; use Namet.Sp;
|
|||||||
with Nlists; use Nlists;
|
with Nlists; use Nlists;
|
||||||
with Nmake; use Nmake;
|
with Nmake; use Nmake;
|
||||||
with Output; use Output;
|
with Output; use Output;
|
||||||
with Opt; use Opt;
|
|
||||||
with Restrict; use Restrict;
|
with Restrict; use Restrict;
|
||||||
with Rident; use Rident;
|
with Rident; use Rident;
|
||||||
with Rtsfind; use Rtsfind;
|
with Rtsfind; use Rtsfind;
|
||||||
@ -15321,6 +15320,15 @@ package body Sem_Util is
|
|||||||
Reset_Analyzed (N);
|
Reset_Analyzed (N);
|
||||||
end Reset_Analyzed_Flags;
|
end Reset_Analyzed_Flags;
|
||||||
|
|
||||||
|
------------------------
|
||||||
|
-- Restore_SPARK_Mode --
|
||||||
|
------------------------
|
||||||
|
|
||||||
|
procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type) is
|
||||||
|
begin
|
||||||
|
SPARK_Mode := Mode;
|
||||||
|
end Restore_SPARK_Mode;
|
||||||
|
|
||||||
--------------------------------
|
--------------------------------
|
||||||
-- Returns_Unconstrained_Type --
|
-- Returns_Unconstrained_Type --
|
||||||
--------------------------------
|
--------------------------------
|
||||||
@ -15624,6 +15632,28 @@ package body Sem_Util is
|
|||||||
end if;
|
end if;
|
||||||
end Same_Value;
|
end Same_Value;
|
||||||
|
|
||||||
|
-----------------------------
|
||||||
|
-- Save_SPARK_Mode_And_Set --
|
||||||
|
-----------------------------
|
||||||
|
|
||||||
|
procedure Save_SPARK_Mode_And_Set
|
||||||
|
(Context : Entity_Id;
|
||||||
|
Mode : out SPARK_Mode_Type)
|
||||||
|
is
|
||||||
|
Prag : constant Node_Id := SPARK_Pragma (Context);
|
||||||
|
|
||||||
|
begin
|
||||||
|
-- Save the current mode in effect
|
||||||
|
|
||||||
|
Mode := SPARK_Mode;
|
||||||
|
|
||||||
|
-- Set the mode of the context as the current SPARK mode
|
||||||
|
|
||||||
|
if Present (Prag) then
|
||||||
|
SPARK_Mode := Get_SPARK_Mode_From_Pragma (Prag);
|
||||||
|
end if;
|
||||||
|
end Save_SPARK_Mode_And_Set;
|
||||||
|
|
||||||
------------------------
|
------------------------
|
||||||
-- Scope_Is_Transient --
|
-- Scope_Is_Transient --
|
||||||
------------------------
|
------------------------
|
||||||
|
@ -28,6 +28,7 @@
|
|||||||
with Einfo; use Einfo;
|
with Einfo; use Einfo;
|
||||||
with Exp_Tss; use Exp_Tss;
|
with Exp_Tss; use Exp_Tss;
|
||||||
with Namet; use Namet;
|
with Namet; use Namet;
|
||||||
|
with Opt; use Opt;
|
||||||
with Snames; use Snames;
|
with Snames; use Snames;
|
||||||
with Types; use Types;
|
with Types; use Types;
|
||||||
with Uintp; use Uintp;
|
with Uintp; use Uintp;
|
||||||
@ -1689,6 +1690,10 @@ package Sem_Util is
|
|||||||
procedure Reset_Analyzed_Flags (N : Node_Id);
|
procedure Reset_Analyzed_Flags (N : Node_Id);
|
||||||
-- Reset the Analyzed flags in all nodes of the tree whose root is N
|
-- Reset the Analyzed flags in all nodes of the tree whose root is N
|
||||||
|
|
||||||
|
procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type);
|
||||||
|
-- Set the current SPARK_Mode to whatever Mode denotes. This routime must
|
||||||
|
-- be used in tandem with Save_SPARK_Mode_And_Set.
|
||||||
|
|
||||||
function Returns_Unconstrained_Type (Subp : Entity_Id) return Boolean;
|
function Returns_Unconstrained_Type (Subp : Entity_Id) return Boolean;
|
||||||
-- Return true if Subp is a function that returns an unconstrained type
|
-- Return true if Subp is a function that returns an unconstrained type
|
||||||
|
|
||||||
@ -1740,6 +1745,13 @@ package Sem_Util is
|
|||||||
-- A result of False does not necessarily mean they have different values,
|
-- A result of False does not necessarily mean they have different values,
|
||||||
-- just that it is not possible to determine they have the same value.
|
-- just that it is not possible to determine they have the same value.
|
||||||
|
|
||||||
|
procedure Save_SPARK_Mode_And_Set
|
||||||
|
(Context : Entity_Id;
|
||||||
|
Mode : out SPARK_Mode_Type);
|
||||||
|
-- Save the current SPARK_Mode in effect in Mode. Establish the SPARK_Mode
|
||||||
|
-- (if any) of a package or a subprogram denoted by Context. This routine
|
||||||
|
-- must be used in tandem with Restore_SPARK_Mode.
|
||||||
|
|
||||||
function Scope_Within_Or_Same (Scope1, Scope2 : Entity_Id) return Boolean;
|
function Scope_Within_Or_Same (Scope1, Scope2 : Entity_Id) return Boolean;
|
||||||
-- Determines if the entity Scope1 is the same as Scope2, or if it is
|
-- Determines if the entity Scope1 is the same as Scope2, or if it is
|
||||||
-- inside it, where both entities represent scopes. Note that scopes
|
-- inside it, where both entities represent scopes. Note that scopes
|
||||||
|
Loading…
Reference in New Issue
Block a user