Skip to content

R
riscv-gcc-1
Commit b6a56408 by Arnaud Charlet
Options

[multiple changes] 

2015-03-04  Robert Dewar  <dewar@adacore.com>

	* exp_ch7.adb: Minor reformatting.
	* exp_unst.adb (Build_Tables): Fix minor glitch for no separate
	spec case.
	* erroutc.adb (Delete_Msg): add missing decrement of info msg counter.

2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Build_Pragma_Check_Equivalent): Suppress
	references to formal parameters subject to pragma Unreferenced.
	(Suppress_Reference): New routine.
	* sem_attr.adb (Analyze_Attribute): Reimplement the analysis
	of attribute 'Old. Attributes 'Old and 'Result now share
	common processing.
	(Analyze_Old_Result_Attribute): New routine.
	(Check_Placement_In_Check): Removed.
	(Check_Placement_In_Contract_Cases): Removed.
	(Check_Placement_In_Test_Case): Removed.
	(Check_Use_In_Contract_Cases): Removed.
	(Check_Use_In_Test_Case): Removed.
	(In_Refined_Post): Removed.
	(Is_Within): Removed.
	* sem_warn.adb (Check_Low_Bound_Tested): Code cleanup.
	(Check_Low_Bound_Tested_For): New routine.

2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Object_Declaration):
	Generate a runtime check to test the expression of pragma
	Default_Initial_Condition when the object is default initialized.

From-SVN: r221176
parent 2322588a
Showing with 509 additions and 540 deletions
gcc/ada/ChangeLog
2015-03-04 Robert Dewar <dewar@adacore.com>
* exp_ch7.adb: Minor reformatting.
* exp_unst.adb (Build_Tables): Fix minor glitch for no separate
spec case.
* erroutc.adb (Delete_Msg): add missing decrement of info msg counter.
2015-03-04 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch6.adb (Build_Pragma_Check_Equivalent): Suppress
references to formal parameters subject to pragma Unreferenced.
(Suppress_Reference): New routine.
* sem_attr.adb (Analyze_Attribute): Reimplement the analysis
of attribute 'Old. Attributes 'Old and 'Result now share
common processing.
(Analyze_Old_Result_Attribute): New routine.
(Check_Placement_In_Check): Removed.
(Check_Placement_In_Contract_Cases): Removed.
(Check_Placement_In_Test_Case): Removed.
(Check_Use_In_Contract_Cases): Removed.
(Check_Use_In_Test_Case): Removed.
(In_Refined_Post): Removed.
(Is_Within): Removed.
* sem_warn.adb (Check_Low_Bound_Tested): Code cleanup.
(Check_Low_Bound_Tested_For): New routine.
2015-03-04 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_N_Object_Declaration):
Generate a runtime check to test the expression of pragma
Default_Initial_Condition when the object is default initialized.
2015-03-02 Robert Dewar <dewar@adacore.com>
* scng.adb (Scan): Ignore illegal character in relaxed
......
gcc/ada/erroutc.adb
......@@ -141,6 +141,10 @@ package body Erroutc is
if Errors.Table (D).Warn or else Errors.Table (D).Style then
Warnings_Detected := Warnings_Detected - 1;
if Errors.Table (D).Info then
Info_Messages := Info_Messages - 1;
end if;
-- Note: we do not need to decrement Warnings_Treated_As_Errors
-- because this only gets incremented if we actually output the
-- message, which we won't do if we are deleting it here!
......
gcc/ada/exp_ch3.adb
......@@ -6138,11 +6138,9 @@ package body Exp_Ch3 is
end;
end if;
-- At this point the object is fully initialized by either invoking the
-- related type init proc, routine [Deep_]Initialize or performing in-
-- place assingments for an array object. If the related type is subject
-- to pragma Default_Initial_Condition, add a runtime check to verify
-- the assumption of the pragma. Generate:
-- If the object is default initialized and its type is subject to
-- pragma Default_Initial_Condition, add a runtime check to verify
-- the assumption of the pragma (SPARK RM 7.3.3). Generate:
-- <Base_Typ>Default_Init_Cond (<Base_Typ> (Def_Id));
......@@ -6152,6 +6150,7 @@ package body Exp_Ch3 is
and then (Has_Default_Init_Cond (Base_Typ)
or else
Has_Inherited_Default_Init_Cond (Base_Typ))
and then not Has_Init_Expression (N)
then
declare
DIC_Call : constant Node_Id :=
......
gcc/ada/exp_ch6.adb
......@@ -7163,6 +7163,42 @@ package body Exp_Ch6 is
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty) return Node_Id
is
function Suppress_Reference (N : Node_Id) return Traverse_Result;
-- Detect whether node N references a formal parameter subject to
-- pragma Unreferenced. If this is the case, set Comes_From_Source
-- to False to suppress the generation of a reference when analyzing
-- N later on.
------------------------
-- Suppress_Reference --
------------------------
function Suppress_Reference (N : Node_Id) return Traverse_Result is
Formal : Entity_Id;
begin
if Is_Entity_Name (N) and then Present (Entity (N)) then
Formal := Entity (N);
-- The formal parameter is subject to pragma Unreferenced.
-- Prevent the generation of a reference by resetting the
-- Comes_From_Source flag.
if Is_Formal (Formal)
and then Has_Pragma_Unreferenced (Formal)
then
Set_Comes_From_Source (N, False);
end if;
end if;
return OK;
end Suppress_Reference;
procedure Suppress_References is
new Traverse_Proc (Suppress_Reference);
-- Local variables
Loc : constant Source_Ptr := Sloc (Prag);
Prag_Nam : constant Name_Id := Pragma_Name (Prag);
Check_Prag : Node_Id;
......@@ -7172,6 +7208,8 @@ package body Exp_Ch6 is
Nam : Name_Id;
Subp_Formal : Entity_Id;
-- Start of processing for Build_Pragma_Check_Equivalent
begin
Formals_Map := No_Elist;
......@@ -7208,8 +7246,26 @@ package body Exp_Ch6 is
-- Mark the pragma as being internally generated and reset the
-- Analyzed flag.
Set_Comes_From_Source (Check_Prag, False);
Set_Analyzed (Check_Prag, False);
Set_Comes_From_Source (Check_Prag, False);
-- The tree of the original pragma may contain references to the
-- formal parameters of the related subprogram. At the same time
-- the corresponding body may mark the formals as unreferenced:
-- procedure Proc (Formal : ...)
-- with Pre => Formal ...;
-- procedure Proc (Formal : ...) is
-- pragma Unreferenced (Formal);
-- ...
-- This creates problems because all pragma Check equivalents are
-- analyzed at the end of the body declarations. Since all source
-- references have already been accounted for, reset any references
-- to such formals in the generated pragma Check equivalent.
Suppress_References (Check_Prag);
if Present (Corresponding_Aspect (Prag)) then
Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
......
gcc/ada/exp_ch7.adb
......@@ -7853,12 +7853,10 @@ package body Exp_Ch7 is
(Loc : Source_Ptr;
Ptr_Typ : Entity_Id) return Node_Id
is
-- It is possible for Ptr_Typ to be a partial view, if the access
-- type is a full view declared in the private part of a nested package,
-- and the finalization actions take place when completing analysis
-- of the enclosing unit. For this reason we use Underlying_Type
-- in two places below.
-- It is possible for Ptr_Typ to be a partial view, if the access type
-- is a full view declared in the private part of a nested package, and
-- the finalization actions take place when completing analysis of the
-- enclosing unit. For this reason use Underlying_Type twice below.
Desig_Typ : constant Entity_Id :=
Available_View
......
gcc/ada/exp_unst.adb
......@@ -491,16 +491,16 @@ package body Exp_Unst is
-- then we won't catch it in the traversal of the body. But we do
-- want to visit the declaration in this case!
declare
Dummy : Traverse_Result;
Decl : constant Node_Id :=
Parent (Declaration_Node (Corresponding_Spec (Subp_Body)));
pragma Assert (Nkind (Decl) = N_Subprogram_Declaration);
begin
if not Acts_As_Spec (Subp_Body) then
if not Acts_As_Spec (Subp_Body) then
declare
Dummy : Traverse_Result;
Decl : constant Node_Id :=
Parent (Declaration_Node (Corresponding_Spec (Subp_Body)));
pragma Assert (Nkind (Decl) = N_Subprogram_Declaration);
begin
Dummy := Visit_Node (Decl);
end if;
end;
end;
end if;
-- Traverse the body to get the rest of the subprograms and calls
......
gcc/ada/sem_attr.adb
......@@ -241,6 +241,15 @@ package body Sem_Attr is
-- Used for Access, Unchecked_Access, Unrestricted_Access attributes.
-- Internally, Id distinguishes which of the three cases is involved.
procedure Analyze_Attribute_Old_Result
(Legal : out Boolean;
Spec_Id : out Entity_Id);
-- Common processing for attributes 'Old and 'Result. The routine checks
-- that the attribute appears in a postcondition-like aspect or pragma
-- associated with a suitable subprogram or a body. Flag Legal is set
-- when the above criterias are met. Spec_Id denotes the entity of the
-- subprogram [body] or Empty if the attribute is illegal.
procedure Bad_Attribute_For_Predicate;
-- Output error message for use of a predicate (First, Last, Range) not
-- allowed with a type that has predicates. If the type is a generic
......@@ -343,6 +352,9 @@ package body Sem_Attr is
procedure Check_Object_Reference (P : Node_Id);
-- Check that P is an object reference
procedure Check_PolyORB_Attribute;
-- Validity checking for PolyORB/DSA attribute
procedure Check_Program_Unit;
-- Verify that prefix of attribute N is a program unit
......@@ -364,9 +376,6 @@ package body Sem_Attr is
procedure Check_System_Prefix;
-- Verify that prefix of attribute N is package System
procedure Check_PolyORB_Attribute;
-- Validity checking for PolyORB/DSA attribute
procedure Check_Task_Prefix;
-- Verify that prefix of attribute N is a task or task type
......@@ -397,10 +406,6 @@ package body Sem_Attr is
pragma No_Return (Error_Attr);
-- Like Error_Attr, but error is posted at the start of the prefix
function In_Refined_Post return Boolean;
-- Determine whether the current attribute appears in pragma
-- Refined_Post.
procedure Legal_Formal_Attribute;
-- Common processing for attributes Definite and Has_Discriminants.
-- Checks that prefix is generic indefinite formal type.
......@@ -1072,6 +1077,263 @@ package body Sem_Attr is
end if;
end Analyze_Access_Attribute;
----------------------------------
-- Analyze_Attribute_Old_Result --
----------------------------------
procedure Analyze_Attribute_Old_Result
(Legal : out Boolean;
Spec_Id : out Entity_Id)
is
procedure Check_Placement_In_Check (Prag : Node_Id);
-- Verify that the attribute appears within pragma Check that mimics
-- a postcondition.
procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
-- Verify that the attribute appears within a consequence of aspect
-- or pragma Contract_Cases denoted by Prag.
procedure Check_Placement_In_Test_Case (Prag : Node_Id);
-- Verify that the attribute appears within the "Ensures" argument of
-- aspect or pragma Test_Case denoted by Prag.
function Is_Within
(Nod : Node_Id;
Encl_Nod : Node_Id) return Boolean;
-- Subsidiary to Check_Placemenet_In_XXX. Determine whether arbitrary
-- node Nod is within enclosing node Encl_Nod.
------------------------------
-- Check_Placement_In_Check --
------------------------------
procedure Check_Placement_In_Check (Prag : Node_Id) is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
Nam : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
begin
-- The "Name" argument of pragma Check denotes a postcondition
if Nam_In (Nam, Name_Post,
Name_Post_Class,
Name_Postcondition,
Name_Refined_Post)
then
null;
-- Otherwise the placement of the attribute is illegal
else
if Aname = Name_Old then
Error_Attr
("attribute % can only appear in postcondition", P);
-- Specialize the error message for attribute 'Result
else
Error_Attr
("attribute % can only appear in postcondition of "
& "function", P);
end if;
end if;
end Check_Placement_In_Check;
---------------------------------------
-- Check_Placement_In_Contract_Cases --
---------------------------------------
procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
Arg : Node_Id;
Cases : Node_Id;
CCase : Node_Id;
begin
-- Obtain the argument of the aspect or pragma
if Nkind (Prag) = N_Aspect_Specification then
Arg := Prag;
else
Arg := First (Pragma_Argument_Associations (Prag));
end if;
Cases := Expression (Arg);
if Present (Component_Associations (Cases)) then
CCase := First (Component_Associations (Cases));
while Present (CCase) loop
-- Detect whether the attribute appears within the
-- consequence of the current contract case.
if Nkind (CCase) = N_Component_Association
and then Is_Within (N, Expression (CCase))
then
return;
end if;
Next (CCase);
end loop;
end if;
-- Otherwise aspect or pragma Contract_Cases is either malformed
-- or the attribute does not appear within a consequence.
Error_Attr
("attribute % must appear in the consequence of a contract case",
P);
end Check_Placement_In_Contract_Cases;
----------------------------------
-- Check_Placement_In_Test_Case --
----------------------------------
procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
Arg : constant Node_Id :=
Test_Case_Arg
(Prag => Prag,
Arg_Nam => Name_Ensures,
From_Aspect => Nkind (Prag) = N_Aspect_Specification);
begin
-- Detect whether the attribute appears within the "Ensures"
-- expression of aspect or pragma Test_Case.
if Present (Arg) and then Is_Within (N, Arg) then
null;
else
Error_Attr
("attribute % must appear in the ensures expression of a "
& "test case", P);
end if;
end Check_Placement_In_Test_Case;
---------------
-- Is_Within --
---------------
function Is_Within
(Nod : Node_Id;
Encl_Nod : Node_Id) return Boolean
is
Par : Node_Id;
begin
Par := Nod;
while Present (Par) loop
if Par = Encl_Nod then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end Is_Within;
-- Local variables
Prag : Node_Id;
Prag_Nam : Name_Id;
Subp_Decl : Node_Id;
-- Start of processing for Analyze_Attribute_Old_Result
begin
-- Assume that the attribute is illegal
Legal := False;
Spec_Id := Empty;
-- Traverse the parent chain to find the aspect or pragma where the
-- attribute resides.
Prag := N;
while Present (Prag) loop
if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
exit;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Prag) then
exit;
end if;
Prag := Parent (Prag);
end loop;
-- The attribute is allowed to appear only in postcondition-like
-- aspects or pragmas.
if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
if Nkind (Prag) = N_Aspect_Specification then
Prag_Nam := Chars (Identifier (Prag));
else
Prag_Nam := Pragma_Name (Prag);
end if;
if Prag_Nam = Name_Check then
Check_Placement_In_Check (Prag);
elsif Prag_Nam = Name_Contract_Cases then
Check_Placement_In_Contract_Cases (Prag);
elsif Nam_In (Prag_Nam, Name_Post,
Name_Post_Class,
Name_Postcondition,
Name_Refined_Post)
then
null;
elsif Prag_Nam = Name_Test_Case then
Check_Placement_In_Test_Case (Prag);
else
Error_Attr ("attribute % can only appear in postcondition", P);
return;
end if;
-- Otherwise the placement of the attribute is illegal
else
Error_Attr ("attribute % can only appear in postcondition", P);
return;
end if;
-- Find the related subprogram subject to the aspect or pragma
if Nkind (Prag) = N_Aspect_Specification then
Subp_Decl := Parent (Prag);
else
Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
end if;
-- The aspect or pragma where the attribute resides should be
-- associated with a subprogram declaration or a body. If this is not
-- the case, then the aspect or pragma is illegal. Return as analysis
-- cannot be carried out.
if not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
N_Entry_Declaration,
N_Generic_Subprogram_Declaration,
N_Subprogram_Body,
N_Subprogram_Body_Stub,
N_Subprogram_Declaration)
then
return;
end if;
-- If we get here, then the attribute is legal
Legal := True;
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
end Analyze_Attribute_Old_Result;
---------------------------------
-- Bad_Attribute_For_Predicate --
---------------------------------
......@@ -2175,60 +2437,6 @@ package body Sem_Attr is
Error_Attr;
end Error_Attr_P;
---------------------
-- In_Refined_Post --
---------------------
function In_Refined_Post return Boolean is
function Is_Refined_Post (Prag : Node_Id) return Boolean;
-- Determine whether Prag denotes one of the incarnations of pragma
-- Refined_Post (either as is or pragma Check (Refined_Post, ...).
---------------------
-- Is_Refined_Post --
---------------------
function Is_Refined_Post (Prag : Node_Id) return Boolean is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
Nam : constant Name_Id := Pragma_Name (Prag);
begin
if Nam = Name_Refined_Post then
return True;
elsif Nam = Name_Check then
pragma Assert (Present (Args));
return Chars (Expression (First (Args))) = Name_Refined_Post;
end if;
return False;
end Is_Refined_Post;
-- Local variables
Stmt : Node_Id;
-- Start of processing for In_Refined_Post
begin
Stmt := Parent (N);
while Present (Stmt) loop
if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
Stmt := Parent (Stmt);
end loop;
return False;
end In_Refined_Post;
----------------------------
-- Legal_Formal_Attribute --
----------------------------
......@@ -4462,14 +4670,6 @@ package body Sem_Attr is
-- the related postcondition expression. Subp_Id is the subprogram to
-- which the related postcondition applies.
procedure Check_Use_In_Contract_Cases (Prag : Node_Id);
-- Perform various semantic checks related to the placement of the
-- attribute in pragma Contract_Cases.
procedure Check_Use_In_Test_Case (Prag : Node_Id);
-- Perform various semantic checks related to the placement of the
-- attribute in pragma Contract_Cases.
--------------------------------
-- Check_References_In_Prefix --
--------------------------------
......@@ -4504,7 +4704,7 @@ package body Sem_Attr is
-- case, then the scope of the local entity is nested within
-- that of the subprogram.
elsif Nkind (Nod) = N_Identifier
elsif Is_Entity_Name (Nod)
and then Present (Entity (Nod))
and then Scope_Within (Scope (Entity (Nod)), Subp_Id)
then
......@@ -4512,6 +4712,9 @@ package body Sem_Attr is
("prefix of attribute % cannot reference local entities",
Nod);
return Abandon;
-- Otherwise keep inspecting the prefix
else
return OK;
end if;
......@@ -4525,261 +4728,130 @@ package body Sem_Attr is
Check_References (P);
end Check_References_In_Prefix;
---------------------------------
-- Check_Use_In_Contract_Cases --
---------------------------------
procedure Check_Use_In_Contract_Cases (Prag : Node_Id) is
Cases : constant Node_Id :=
Get_Pragma_Arg
(First (Pragma_Argument_Associations (Prag)));
Expr : Node_Id;
begin
-- Climb the parent chain to reach the top of the expression where
-- attribute 'Old resides.
Expr := N;
while Parent (Parent (Expr)) /= Cases loop
Expr := Parent (Expr);
end loop;
-- Ensure that the obtained expression is the consequence of a
-- contract case as this is the only postcondition-like part of
-- the pragma. Otherwise, attribute 'Old appears in the condition
-- of a contract case. Emit an error since this is not a
-- postcondition-like context. (SPARK RM 6.1.3(2))
if Expr /= Expression (Parent (Expr)) then
Error_Attr
("attribute % cannot appear in the condition "
& "of a contract case", P);
end if;
end Check_Use_In_Contract_Cases;
----------------------------
-- Check_Use_In_Test_Case --
----------------------------
procedure Check_Use_In_Test_Case (Prag : Node_Id) is
Ensures : constant Node_Id := Test_Case_Arg (Prag, Name_Ensures);
Expr : Node_Id;
begin
-- Climb the parent chain to reach the top of the Ensures part of
-- pragma Test_Case.
Expr := N;
while Expr /= Prag loop
if Expr = Ensures then
return;
end if;
Expr := Parent (Expr);
end loop;
-- If we get there, then attribute 'Old appears in the requires
-- expression of pragma Test_Case which is not a postcondition-
-- like context.
Error_Attr
("attribute % cannot appear in the requires expression of a "
& "test case", P);
end Check_Use_In_Test_Case;
-- Local variables
CS : Entity_Id;
-- The enclosing scope, excluding loops for quantified expressions.
-- During analysis, it is the postcondition subprogram. During
-- pre-analysis, it is the scope of the subprogram declaration.
Prag : Node_Id;
-- During pre-analysis, Prag is the enclosing pragma node if any
Legal : Boolean;
Pref_Id : Entity_Id;
Pref_Typ : Entity_Id;
Spec_Id : Entity_Id;
-- Start of processing for Old
begin
Prag := Empty;
-- Find enclosing scopes, excluding loops
CS := Current_Scope;
while Ekind (CS) = E_Loop loop
CS := Scope (CS);
end loop;
-- Check the legality of attribute 'Old when it appears inside pragma
-- Refined_Post. These specialized checks are required only when code
-- generation is disabled. In the general case pragma Refined_Post is
-- transformed into pragma Check by Process_PPCs which in turn is
-- relocated to procedure _Postconditions. From then on the legality
-- of 'Old is determined as usual.
-- The attribute reference is a primary. If any expressions follow,
-- then the attribute reference is an indexable object. Transform the
-- attribute into an indexed component and analyze it.
if not Expander_Active and then In_Refined_Post then
Preanalyze_And_Resolve (P);
Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
if Present (E1) then
Rewrite (N,
Make_Indexed_Component (Loc,
Prefix =>
Make_Attribute_Reference (Loc,
Prefix => Relocate_Node (P),
Attribute_Name => Name_Old),
Expressions => Expressions (N)));
Analyze (N);
return;
end if;
if Is_Limited_Type (P_Type) then
Error_Attr ("attribute % cannot apply to limited objects", P);
end if;
Analyze_Attribute_Old_Result (Legal, Spec_Id);
if Is_Entity_Name (P)
and then Is_Constant_Object (Entity (P))
then
Error_Msg_N
("??attribute Old applied to constant has no effect", P);
end if;
-- The aspect or pragma where attribute 'Old resides should be
-- associated with a subprogram declaration or a body. If this is not
-- the case, then the aspect or pragma is illegal. Return as analysis
-- cannot be carried out.
if not Legal then
return;
end if;
-- A Contract_Cases, Postcondition or Test_Case pragma is in the
-- process of being preanalyzed. Perform the semantic checks now
-- before the pragma is relocated and/or expanded.
-- For a generic subprogram, postconditions are preanalyzed as well
-- for name capture, and still appear within an aspect spec.
elsif In_Spec_Expression or Inside_A_Generic then
Prag := N;
while Present (Prag)
and then not Nkind_In (Prag, N_Aspect_Specification,
N_Function_Specification,
N_Pragma,
N_Procedure_Specification,
N_Subprogram_Body)
loop
Prag := Parent (Prag);
end loop;
-- In ASIS mode, the aspect itself is analyzed, in addition to the
-- corresponding pragma. Don't issue errors when analyzing aspect.
-- The prefix must be preanalyzed as the full analysis will take
-- place during expansion.
if Nkind (Prag) = N_Aspect_Specification
and then Nam_In (Chars (Identifier (Prag)), Name_Post,
Name_Refined_Post)
then
null;
Preanalyze_And_Resolve (P);
-- In all other cases the related context must be a pragma
-- Ensure that the prefix does not contain attributes 'Old or 'Result
elsif Nkind (Prag) /= N_Pragma then
Error_Attr ("% attribute can only appear in postcondition", P);
Check_References_In_Prefix (Spec_Id);
-- Verify the placement of the attribute with respect to the
-- related pragma.
-- Set the type of the attribute now to prevent cascaded errors
else
case Get_Pragma_Id (Prag) is
when Pragma_Contract_Cases =>
Check_Use_In_Contract_Cases (Prag);
Pref_Typ := Etype (P);
Set_Etype (N, Pref_Typ);
when Pragma_Postcondition | Pragma_Refined_Post =>
null;
-- Legality checks
when Pragma_Test_Case =>
Check_Use_In_Test_Case (Prag);
if Is_Limited_Type (Pref_Typ) then
Error_Attr ("attribute % cannot apply to limited objects", P);
end if;
when others =>
Error_Attr
("% attribute can only appear in postcondition", P);
end case;
end if;
-- The prefix is a simple name
-- Body case, where we must be inside a generated _Postconditions
-- procedure, or else the attribute use is definitely misplaced. The
-- postcondition itself may have generated transient scopes, and is
-- not necessarily the current one.
if Is_Entity_Name (P) and then Present (Entity (P)) then
Pref_Id := Entity (P);
else
while Present (CS) and then CS /= Standard_Standard loop
if Chars (CS) = Name_uPostconditions then
exit;
else
CS := Scope (CS);
end if;
end loop;
-- Emit a warning when the prefix is a constant. Note that the use
-- of Error_Attr would reset the type of N to Any_Type even though
-- this is a warning. Use Error_Msg_XXX instead.
if Chars (CS) /= Name_uPostconditions then
Error_Attr ("% attribute can only appear in postcondition", P);
if Is_Constant_Object (Pref_Id) then
Error_Msg_Name_1 := Name_Old;
Error_Msg_N
("??atribute % applied to constant has no effect", P);
end if;
end if;
-- If the attribute reference is generated for a Requires clause,
-- then no expressions follow. Otherwise it is a primary, in which
-- case, if expressions follow, the attribute reference must be an
-- indexable object, so rewrite the node accordingly.
-- Otherwise the prefix is not a simple name
if Present (E1) then
Rewrite (N,
Make_Indexed_Component (Loc,
Prefix =>
Make_Attribute_Reference (Loc,
Prefix => Relocate_Node (Prefix (N)),
Attribute_Name => Name_Old),
Expressions => Expressions (N)));
else
-- Ensure that the prefix of attribute 'Old is an entity when it
-- is potentially unevaluated (6.1.1 (27/3)).
Analyze (N);
return;
end if;
if Is_Potentially_Unevaluated (N) then
Uneval_Old_Msg;
Check_E0;
-- Detect a possible infinite recursion when the prefix denotes
-- the related function.
-- Prefix has not been analyzed yet, and its full analysis will take
-- place during expansion (see below).
-- function Func (...) return ...
-- with Post => Func'Old ...;
Preanalyze_And_Resolve (P);
Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
elsif Nkind (P) = N_Function_Call then
Pref_Id := Entity (Name (P));
if Is_Limited_Type (P_Type) then
Error_Attr ("attribute % cannot apply to limited objects", P);
end if;
if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
and then Pref_Id = Spec_Id
then
Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!possible infinite recursion<<", P);
Error_Msg_N ("\!??Storage_Error ]<<", P);
end if;
end if;
if Is_Entity_Name (P)
and then Is_Constant_Object (Entity (P))
then
Error_Msg_N
("??attribute Old applied to constant has no effect", P);
end if;
-- The prefix of attribute 'Old may refer to a component of a
-- formal parameter. In this case its expansion may generate
-- actual subtypes that are referenced in an inner context and
-- that must be elaborated within the subprogram itself. If the
-- prefix includes a function call, it may involve finalization
-- actions that should be inserted when the attribute has been
-- rewritten as a declaration. Create a declaration for the prefix
-- and insert it at the start of the enclosing subprogram. This is
-- an expansion activity that has to be performed now to prevent
-- out-of-order issues.
-- Check that the prefix of 'Old is an entity when it may be
-- potentially unevaluated (6.1.1 (27/3)).
-- This expansion is both harmful and not needed in SPARK mode,
-- since the formal verification backend relies on the types of
-- nodes (hence is not robust w.r.t. a change to base type here),
-- and does not suffer from the out-of-order issue described
-- above. Thus, this expansion is skipped in SPARK mode.
if Present (Prag)
and then Is_Potentially_Unevaluated (N)
and then not Is_Entity_Name (P)
then
Uneval_Old_Msg;
end if;
if not GNATprove_Mode then
Pref_Typ := Base_Type (Pref_Typ);
Set_Etype (N, Pref_Typ);
Set_Etype (P, Pref_Typ);
-- The attribute appears within a pre/postcondition, but refers to
-- an entity in the enclosing subprogram. If it is a component of
-- a formal its expansion might generate actual subtypes that may
-- be referenced in an inner context, and which must be elaborated
-- within the subprogram itself. If the prefix includes a function
-- call it may involve finalization actions that should only be
-- inserted when the attribute has been rewritten as a declarations.
-- As a result, if the prefix is not a simple name we create
-- a declaration for it now, and insert it at the start of the
-- enclosing subprogram. This is properly an expansion activity
-- but it has to be performed now to prevent out-of-order issues.
-- This expansion is both harmful and not needed in SPARK mode, since
-- the formal verification backend relies on the types of nodes
-- (hence is not robust w.r.t. a change to base type here), and does
-- not suffer from the out-of-order issue described above. Thus, this
-- expansion is skipped in SPARK mode.
if not Is_Entity_Name (P) and then not GNATprove_Mode then
P_Type := Base_Type (P_Type);
Set_Etype (N, P_Type);
Set_Etype (P, P_Type);
Analyze_Dimension (N);
Expand (N);
Analyze_Dimension (N);
Expand (N);
end if;
end if;
end Old;
......@@ -4985,105 +5057,12 @@ package body Sem_Attr is
------------
when Attribute_Result => Result : declare
procedure Check_Placement_In_Check (Prag : Node_Id);
-- Verify that attribute 'Result appears within pragma Check that
-- emulates a postcondition.
procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
-- Verify that attribute 'Result appears within a consequence of
-- pragma Contract_Cases.
procedure Check_Placement_In_Test_Case (Prag : Node_Id);
-- Verify that attribute 'Result appears within the Ensures argument
-- of pragma Test_Case.
function Denote_Same_Function
(Pref_Id : Entity_Id;
Spec_Id : Entity_Id) return Boolean;
-- Determine whether the entity of the prefix Pref_Id denotes the
-- same entity as that of the related subprogram Spec_Id.
function Is_Within
(Nod : Node_Id;
Encl_Nod : Node_Id) return Boolean;
-- Subsidiary to Check_Placemenet_In_XXX_Case. Determine whether
-- arbitrary node Nod is within enclosing node Encl_Nod.
------------------------------
-- Check_Placement_In_Check --
------------------------------
procedure Check_Placement_In_Check (Prag : Node_Id) is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
Nam : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
begin
-- The "Name" argument of pragma Check denotes a postcondition
if Nam_In (Nam, Name_Post,
Name_Postcondition,
Name_Refined_Post)
then
null;
-- Otherwise the placement of attribute 'Result is illegal
else
Error_Attr
("% attribute can only appear in postcondition of function",
P);
end if;
end Check_Placement_In_Check;
---------------------------------------
-- Check_Placement_In_Contract_Cases --
---------------------------------------
procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
Cases : constant Node_Id := Get_Pragma_Arg (First (Args));
CCase : Node_Id;
begin
if Present (Component_Associations (Cases)) then
CCase := First (Component_Associations (Cases));
while Present (CCase) loop
-- Guard against a malformed contract case. Detect whether
-- attribute 'Result appears within the consequence of the
-- current contract case.
if Nkind (CCase) = N_Component_Association
and then Is_Within (N, Expression (CCase))
then
return;
end if;
Next (CCase);
end loop;
end if;
-- Otherwise pragma Contract_Cases is either malformed in some
-- way or attribute 'Result does not appear within a consequence
-- expression.
Error_Attr ("% attribute misplaced inside contract cases", P);
end Check_Placement_In_Contract_Cases;
----------------------------------
-- Check_Placement_In_Test_Case --
----------------------------------
procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
begin
-- Detect whether attribute 'Result appears within the "Ensures"
-- expression of pragma Test_Case.
if not Is_Within (N, Test_Case_Arg (Prag, Name_Ensures)) then
Error_Attr ("% attribute misplaced inside test case", P);
end if;
end Check_Placement_In_Test_Case;
--------------------------
-- Denote_Same_Function --
--------------------------
......@@ -5135,41 +5114,11 @@ package body Sem_Attr is
end if;
end Denote_Same_Function;
---------------
-- Is_Within --
---------------
function Is_Within
(Nod : Node_Id;
Encl_Nod : Node_Id) return Boolean
is
Par : Node_Id;
begin
Par := Nod;
while Present (Par) loop
if Par = Encl_Nod then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end Is_Within;
-- Local variables
Prag : Node_Id;
Prag_Id : Pragma_Id;
Pref_Id : Entity_Id;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
Legal : Boolean;
Pref_Id : Entity_Id;
Spec_Id : Entity_Id;
-- Start of processing for Result
......@@ -5190,91 +5139,17 @@ package body Sem_Attr is
return;
end if;
-- Traverse the parent chain to find the aspect or pragma where
-- attribute 'Result resides.
Prag := N;
while Present (Prag) loop
if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
exit;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Prag) then
exit;
end if;
Prag := Parent (Prag);
end loop;
-- Do not emit an error when preanalyzing an aspect for ASIS. If the
-- placement of attribute 'Result is illegal, the error is reported
-- when analyzing the corresponding pragma.
if ASIS_Mode and then Nkind (Prag) = N_Aspect_Specification then
null;
-- Attribute 'Result is allowed to appear only in postcondition-like
-- pragmas.
elsif Nkind (Prag) = N_Pragma then
Prag_Id := Get_Pragma_Id (Prag);
if Prag_Id = Pragma_Check then
Check_Placement_In_Check (Prag);
elsif Prag_Id = Pragma_Contract_Cases then
Check_Placement_In_Contract_Cases (Prag);
elsif Prag_Id = Pragma_Postcondition
or else Prag_Id = Pragma_Refined_Post
then
null;
elsif Prag_Id = Pragma_Test_Case then
Check_Placement_In_Test_Case (Prag);
else
Error_Attr
("% attribute can only appear in postcondition of function",
P);
return;
end if;
-- Otherwise the placement of the attribute is illegal
else
Error_Attr
("% attribute can only appear in postcondition of function", P);
return;
end if;
-- Attribute 'Result appears within a postcondition-like pragma. Find
-- the related subprogram subject to the pragma.
Analyze_Attribute_Old_Result (Legal, Spec_Id);
if Nkind (Prag) = N_Aspect_Specification then
Subp_Decl := Parent (Prag);
else
Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
end if;
-- The pragma where attribute 'Result resides should be associated
-- with a subprogram declaration or a body. If this is not the case,
-- then the pragma is illegal. Return as analysis cannot be carried
-- out.
-- The aspect or pragma where attribute 'Result resides should be
-- associated with a subprogram declaration or a body. If this is not
-- the case, then the aspect or pragma is illegal. Return as analysis
-- cannot be carried out.
if not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
N_Entry_Declaration,
N_Generic_Subprogram_Declaration,
N_Subprogram_Body,
N_Subprogram_Body_Stub,
N_Subprogram_Declaration)
then
if not Legal then
return;
end if;
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- Attribute 'Result is part of a _Postconditions procedure. There is
-- no need to perform the semantic checks below as they were already
-- verified when the attribute was analyzed in its original context.
......@@ -5309,7 +5184,7 @@ package body Sem_Attr is
else
Error_Msg_Name_2 := Chars (Spec_Id);
Error_Attr
("incorrect prefix for % attribute, expected %", P);
("incorrect prefix for attribute %, expected %", P);
end if;
-- Otherwise the prefix denotes some other form of subprogram
......@@ -5317,7 +5192,7 @@ package body Sem_Attr is
else
Error_Attr
("% attribute can only appear in postcondition of "
("attribute % can only appear in postcondition of "
& "function", P);
end if;
......@@ -5325,7 +5200,7 @@ package body Sem_Attr is
else
Error_Msg_Name_2 := Chars (Spec_Id);
Error_Attr ("incorrect prefix for % attribute, expected %", P);
Error_Attr ("incorrect prefix for attribute %, expected %", P);
end if;
end if;
end Result;
......
gcc/ada/sem_warn.adb
......@@ -723,28 +723,33 @@ package body Sem_Warn is
----------------------------
procedure Check_Low_Bound_Tested (Expr : Node_Id) is
procedure Check_Low_Bound_Tested_For (Opnd : Node_Id);
-- Determine whether operand Opnd denotes attribute 'First whose prefix
-- is a formal parameter. If this is the case, mark the entity of the
-- prefix as having its low bound tested.
--------------------------------
-- Check_Low_Bound_Tested_For --
--------------------------------
procedure Check_Low_Bound_Tested_For (Opnd : Node_Id) is
begin
if Nkind (Opnd) = N_Attribute_Reference
and then Attribute_Name (Opnd) = Name_First
and then Is_Entity_Name (Prefix (Opnd))
and then Present (Entity (Prefix (Opnd)))
and then Is_Formal (Entity (Prefix (Opnd)))
then
Set_Low_Bound_Tested (Entity (Prefix (Opnd)));
end if;
end Check_Low_Bound_Tested_For;
-- Start of processing for Check_Low_Bound_Tested
begin
if Comes_From_Source (Expr) then
declare
L : constant Node_Id := Left_Opnd (Expr);
R : constant Node_Id := Right_Opnd (Expr);
begin
if Nkind (L) = N_Attribute_Reference
and then Attribute_Name (L) = Name_First
and then Is_Entity_Name (Prefix (L))
and then Is_Formal (Entity (Prefix (L)))
then
Set_Low_Bound_Tested (Entity (Prefix (L)));
end if;
if Nkind (R) = N_Attribute_Reference
and then Attribute_Name (R) = Name_First
and then Is_Entity_Name (Prefix (R))
and then Is_Formal (Entity (Prefix (R)))
then
Set_Low_Bound_Tested (Entity (Prefix (R)));
end if;
end;
Check_Low_Bound_Tested_For (Left_Opnd (Expr));
Check_Low_Bound_Tested_For (Right_Opnd (Expr));
end if;
end Check_Low_Bound_Tested;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment