+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>
* sem.ads (Scope_Stack_Entry): Reorganize storage of action lists;
-- Start of processing for Is_Aliased
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;
while Present (Stmt) loop
if Nkind (Stmt) = N_Object_Declaration then
elsif Is_Access_Type (Obj_Typ)
and then Present (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
(Status_Flag_Or_Transient_Decl (Obj_Id), Decl)
then
-- 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
-- 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;
-- True if T has discriminants and is unconstrained, or is an array type
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
Ref_Depends : Node_Id := Empty;
Ref_Global : Node_Id := Empty;
Spec_Id : Entity_Id;
begin
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
-- When a subprogram body declaration is illegal, its defining entity is
-- left unanalyzed. There is nothing left to do in this case because the
-- body lacks a contract, or even a proper Ekind.
Body_Decl, Spec_Id);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Subprogram_Body_Contract;
------------------------------------
Case_Prag : Node_Id := Empty;
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
Nam : Name_Id;
Post_Prag : Node_Id := Empty;
Prag : Node_Id;
Seen_In_Post : Boolean := False;
begin
+ Save_SPARK_Mode_And_Set (Subp, Mode);
+
if Present (Items) then
-- Analyze pre- and postconditions
("function postcondition does not mention result?T?", Post_Prag);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Subprogram_Contract;
------------------------------------
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
begin
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
-- The analysis of pragma Refined_State detects whether the spec has
then
Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Package_Body_Contract;
---------------------------------
------------------------------
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
begin
+ Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+
-- Analyze the initialization related pragmas. Initializes must come
-- before Initial_Condition due to item dependencies.
Check_Missing_Part_Of (Pack_Id);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Package_Contract;
---------------------------------
-- the call has already been constant-folded, nothing to do. We
-- relocate the operand nodes rather than copy them, to preserve
-- 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
Rewrite (First (Parameter_Associations (Original_Node (N))),
Relocate_Node (Left_Opnd (N)));
with Nlists; use Nlists;
with Nmake; use Nmake;
with Output; use Output;
-with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Rtsfind; use Rtsfind;
Reset_Analyzed (N);
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 --
--------------------------------
end if;
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 --
------------------------
with Einfo; use Einfo;
with Exp_Tss; use Exp_Tss;
with Namet; use Namet;
+with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
with Uintp; use Uintp;
procedure Reset_Analyzed_Flags (N : Node_Id);
-- 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;
-- Return true if Subp is a function that returns an unconstrained type
-- 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.
+ 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;
-- Determines if the entity Scope1 is the same as Scope2, or if it is
-- inside it, where both entities represent scopes. Note that scopes
projects / gcc.git / commitdiff