Commit 7c76aa3f by Hristian Kirtchev Committed by Arnaud Charlet

sem_attr.adb (Analyze_Attribute): Factor out heavily indented code in Denote_Same_Function.

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

	* sem_attr.adb (Analyze_Attribute): Factor out heavily indented
	code in Denote_Same_Function.  Do not analyze attribute 'Result
	when it is inside procedure _Postconditions.  Remove a misplaced
	warning diagnostic. Code cleanup.
	(Denote_Same_Function): New routine.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Code
	cleanup. Warn on pre/postconditions on an inlined subprogram.
	(Analyze_Pragma, Refined_Post case): Warn on pre/postconditions on
	an inlined subprogram.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Code cleanup. Warn on
	pre/post condition on an inlined subprogram.
	(Analyze_Test_Case_In_Decl_Part): Code cleanup. Warn on
	pre/postconditions on an inlined subprogram.
	(Check_Postcondition_Use_In_Inlined_Subprogram): New routine.

From-SVN: r221112
parent aaeb3b3a
2015-03-02 Hristian Kirtchev <kirtchev@adacore.com> 2015-03-02 Hristian Kirtchev <kirtchev@adacore.com>
* sem_attr.adb (Analyze_Attribute): Factor out heavily indented
code in Denote_Same_Function. Do not analyze attribute 'Result
when it is inside procedure _Postconditions. Remove a misplaced
warning diagnostic. Code cleanup.
(Denote_Same_Function): New routine.
* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Code
cleanup. Warn on pre/postconditions on an inlined subprogram.
(Analyze_Pragma, Refined_Post case): Warn on pre/postconditions on
an inlined subprogram.
(Analyze_Pre_Post_Condition_In_Decl_Part): Code cleanup. Warn on
pre/post condition on an inlined subprogram.
(Analyze_Test_Case_In_Decl_Part): Code cleanup. Warn on
pre/postconditions on an inlined subprogram.
(Check_Postcondition_Use_In_Inlined_Subprogram): New routine.
2015-03-02 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Ensure_Aggregate_Form): * sem_prag.adb (Ensure_Aggregate_Form):
Ensure that the name denoted by the Chars of a pragma argument Ensure that the name denoted by the Chars of a pragma argument
association has the proper Sloc when converted into an aggregate. association has the proper Sloc when converted into an aggregate.
......
...@@ -4997,6 +4997,12 @@ package body Sem_Attr is ...@@ -4997,6 +4997,12 @@ package body Sem_Attr is
-- Verify that attribute 'Result appears within the Ensures argument -- Verify that attribute 'Result appears within the Ensures argument
-- of pragma Test_Case. -- 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 function Is_Within
(Nod : Node_Id; (Nod : Node_Id;
Encl_Nod : Node_Id) return Boolean; Encl_Nod : Node_Id) return Boolean;
...@@ -5078,6 +5084,57 @@ package body Sem_Attr is ...@@ -5078,6 +5084,57 @@ package body Sem_Attr is
end if; end if;
end Check_Placement_In_Test_Case; end Check_Placement_In_Test_Case;
--------------------------
-- Denote_Same_Function --
--------------------------
function Denote_Same_Function
(Pref_Id : Entity_Id;
Spec_Id : Entity_Id) return Boolean
is
Subp_Spec : constant Node_Id := Parent (Spec_Id);
begin
-- The prefix denotes the related subprogram
if Pref_Id = Spec_Id then
return True;
-- Account for a special case when attribute 'Result appears in
-- the postcondition of a generic function.
-- generic
-- function Gen_Func return ...
-- with Post => Gen_Func'Result ...;
-- When the generic function is instantiated, the Chars field of
-- the instantiated prefix still denotes the name of the generic
-- function. Note that any preemptive transformation is impossible
-- without a proper analysis. The structure of the wrapper package
-- is as follows:
-- package Anon_Gen_Pack is
-- <subtypes and renamings>
-- function Subp_Decl return ...; -- (!)
-- pragma Postcondition (Gen_Func'Result ...); -- (!)
-- function Gen_Func ... renames Subp_Decl;
-- end Anon_Gen_Pack;
elsif Nkind (Subp_Spec) = N_Function_Specification
and then Present (Generic_Parent (Subp_Spec))
and then Ekind (Pref_Id) = E_Function
and then Present (Alias (Pref_Id))
and then Alias (Pref_Id) = Spec_Id
then
return True;
-- Otherwise the prefix does not denote the related subprogram
else
return False;
end if;
end Denote_Same_Function;
--------------- ---------------
-- Is_Within -- -- Is_Within --
--------------- ---------------
...@@ -5108,14 +5165,11 @@ package body Sem_Attr is ...@@ -5108,14 +5165,11 @@ package body Sem_Attr is
-- Local variables -- Local variables
In_Post : Boolean := False;
Prag : Node_Id; Prag : Node_Id;
Prag_Id : Pragma_Id; Prag_Id : Pragma_Id;
Pref_Id : Entity_Id; Pref_Id : Entity_Id;
Spec_Id : Entity_Id; Spec_Id : Entity_Id;
Subp_Decl : Node_Id; Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
Subp_Spec : Node_Id;
-- Start of processing for Result -- Start of processing for Result
...@@ -5204,128 +5258,62 @@ package body Sem_Attr is ...@@ -5204,128 +5258,62 @@ package body Sem_Attr is
Subp_Decl := Find_Related_Subprogram_Or_Body (Prag); Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
end if; end if;
-- The pragma where attribute 'Result appears is associated with a -- The pragma where attribute 'Result resides should be associated
-- subprogram declaration or a body. -- 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.
if Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration, if not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
N_Entry_Declaration, N_Entry_Declaration,
N_Generic_Subprogram_Declaration, N_Generic_Subprogram_Declaration,
N_Subprogram_Body, N_Subprogram_Body,
N_Subprogram_Body_Stub, N_Subprogram_Body_Stub,
N_Subprogram_Declaration) N_Subprogram_Declaration)
then then
Subp_Id := Defining_Entity (Subp_Decl); return;
-- Attribute 'Result is part of the _Postconditions procedure of
-- the related subprogram. Retrieve the related subprogram.
if Chars (Subp_Id) = Name_uPostconditions then
In_Post := True;
Subp_Decl := Parent (Subp_Decl);
Subp_Id := Scope (Subp_Id);
end if; end if;
-- Retrieve the entity of the spec (if any) Spec_Id := Corresponding_Spec_Of (Subp_Decl);
if Nkind (Subp_Decl) = N_Subprogram_Body -- Attribute 'Result is part of a _Postconditions procedure. There is
and then Present (Corresponding_Spec (Subp_Decl)) -- no need to perform the semantic checks below as they were already
then -- verified when the attribute was analyzed in its original context.
Spec_Id := Corresponding_Spec (Subp_Decl); -- Instead, rewrite the attribute as a reference to formal parameter
-- _Result of the _Postconditions procedure.
elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub if Chars (Spec_Id) = Name_uPostconditions then
and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) Rewrite (N, Make_Identifier (Loc, Name_uResult));
then
Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
else -- The type of formal parameter _Result is that of the function
Spec_Id := Subp_Id; -- encapsulating the _Postconditions procedure. Resolution must
end if; -- be carried out against the function return type.
-- When the subprogram is always inlined, the postcondition will Analyze_And_Resolve (N, Etype (Scope (Spec_Id)));
-- not be propagated to the expanded body.
if Warn_On_Redundant_Constructs -- Otherwise attribute 'Result appears in its original context and
and then Has_Pragma_Inline_Always (Spec_Id) -- all semantic checks should be carried out.
then
Error_Msg_N
("postconditions on inlined functions not enforced?r?", P);
end if;
-- Ensure that the prefix of attribute 'Result denotes the related else
-- subprogram. -- Verify the legality of the prefix. It must denotes the entity
-- of the related [generic] function.
if Is_Entity_Name (P) then if Is_Entity_Name (P) then
Pref_Id := Entity (P); Pref_Id := Entity (P);
-- When a subprogram with contract assertions is imported, it
-- is encapsulated in a wrapper. In this case the scope of the
-- wrapper denotes the original imported subprogram.
if Is_Imported (Pref_Id) then
Pref_Id := Scope (Pref_Id);
end if;
if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then
if Denote_Same_Function (Pref_Id, Spec_Id) then
Set_Etype (N, Etype (Spec_Id));
-- The prefix of attribute 'Result denotes the entity of -- Otherwise the prefix denotes some unrelated function
-- some other unrelated function.
if Pref_Id /= Spec_Id then
Subp_Spec := Parent (Spec_Id);
-- Attribute 'Result appears in a postcondition of a
-- generic function that acts as a compilation unit:
-- generic
-- function Gen_Func return ...
-- with Post => Gen_Func'Result ...;
-- When the function is instantiated, the Chars field of
-- attribute 'Result's prefix still denotes the generic
-- function. Note that any preemptive transformation is
-- impossible without a proper analysis. The structure of
-- the anonymous wrapper package is as follows:
-- package Anon_Gen_Pack is
-- <subtypes and renamings>
-- function Subp_Decl return ...;
-- pragma Postcondition (Gen_Func'Result ...);
-- function Gen_Func ... renames Subp_Decl;
-- end Anon_Gen_Pack;
-- Recognize this case and do not flag it as illegal
if Nkind (Subp_Spec) = N_Function_Specification
and then Present (Generic_Parent (Subp_Spec))
then
if Generic_Parent (Subp_Spec) = Pref_Id then
null;
elsif Ekind (Pref_Id) = E_Function
and then Present (Alias (Pref_Id))
and then Alias (Pref_Id) = Spec_Id
then
null;
else
Error_Msg_Name_2 := Chars (Spec_Id);
Error_Attr
("incorrect prefix for % attribute, expected %",
P);
end if;
-- Otherwise the context is not a function instantiation
-- and the prefix is illegal
else else
Error_Msg_Name_2 := Chars (Spec_Id); Error_Msg_Name_2 := Chars (Spec_Id);
Error_Attr Error_Attr
("incorrect prefix for % attribute, expected %", P); ("incorrect prefix for % attribute, expected %", P);
end if; end if;
end if;
-- Otherwise the attribute's prefix denotes some other form of -- Otherwise the prefix denotes some other form of subprogram
-- a non-function subprogram. -- entity.
else else
Error_Attr Error_Attr
...@@ -5339,20 +5327,6 @@ package body Sem_Attr is ...@@ -5339,20 +5327,6 @@ package body Sem_Attr is
Error_Msg_Name_2 := Chars (Spec_Id); 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;
-- Attribute 'Result is part of the _Postconditions procedure of
-- the related subprogram. Rewrite the attribute as a reference to
-- the _Result formal parameter of _Postconditions.
if In_Post then
Rewrite (N, Make_Identifier (Loc, Name_uResult));
Analyze_And_Resolve (N, Etype (Subp_Id));
-- Otherwise decorate the attribute
else
Set_Etype (N, Etype (Subp_Id));
end if;
end if; end if;
end Result; end Result;
......
...@@ -202,6 +202,13 @@ package body Sem_Prag is ...@@ -202,6 +202,13 @@ package body Sem_Prag is
-- _Post, _Invariant, or _Type_Invariant, which are special names used -- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references. -- in identifiers to represent these attribute references.
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Subp_Id : Entity_Id);
-- Subsidiary to the analysis of pragmas Contract_Cases, Postcondition,
-- Precondition, Refined_Post and Test_Case. Emit a warning when pragma
-- Prag is associated with subprogram Subp_Id subject to Inline_Always.
procedure Check_State_And_Constituent_Use procedure Check_State_And_Constituent_Use
(States : Elist_Id; (States : Elist_Id;
Constits : Elist_Id; Constits : Elist_Id;
...@@ -427,6 +434,7 @@ package body Sem_Prag is ...@@ -427,6 +434,7 @@ package body Sem_Prag is
All_Cases : Node_Id; All_Cases : Node_Id;
CCase : Node_Id; CCase : Node_Id;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id; Subp_Decl : Node_Id;
Subp_Id : Entity_Id; Subp_Id : Entity_Id;
...@@ -439,6 +447,7 @@ package body Sem_Prag is ...@@ -439,6 +447,7 @@ package body Sem_Prag is
Set_Analyzed (N); Set_Analyzed (N);
Subp_Decl := Find_Related_Subprogram_Or_Body (N); Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
Subp_Id := Defining_Entity (Subp_Decl); Subp_Id := Defining_Entity (Subp_Decl);
All_Cases := Expression (Get_Argument (N, Subp_Id)); All_Cases := Expression (Get_Argument (N, Subp_Id));
...@@ -455,14 +464,14 @@ package body Sem_Prag is ...@@ -455,14 +464,14 @@ package body Sem_Prag is
-- to subprogram declarations. Skip the installation for subprogram -- to subprogram declarations. Skip the installation for subprogram
-- bodies because the formals are already visible. -- bodies because the formals are already visible.
if not In_Open_Scopes (Subp_Id) then if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True; Restore_Scope := True;
Push_Scope (Subp_Id); Push_Scope (Spec_Id);
if Is_Generic_Subprogram (Subp_Id) then if Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Subp_Id); Install_Generic_Formals (Spec_Id);
else else
Install_Formals (Subp_Id); Install_Formals (Spec_Id);
end if; end if;
end if; end if;
...@@ -472,6 +481,11 @@ package body Sem_Prag is ...@@ -472,6 +481,11 @@ package body Sem_Prag is
Next (CCase); Next (CCase);
end loop; end loop;
-- Currently it is not possible to inline pre/postconditions on a
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
if Restore_Scope then if Restore_Scope then
End_Scope; End_Scope;
end if; end if;
...@@ -18465,6 +18479,11 @@ package body Sem_Prag is ...@@ -18465,6 +18479,11 @@ package body Sem_Prag is
if Legal then if Legal then
Analyze_Pre_Post_Condition_In_Decl_Part (N); Analyze_Pre_Post_Condition_In_Decl_Part (N);
-- Currently it is not possible to inline pre/postconditions on
-- a subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-- Chain the pragma on the contract for easy retrieval -- Chain the pragma on the contract for easy retrieval
Add_Contract_Item (N, Body_Id); Add_Contract_Item (N, Body_Id);
...@@ -21513,6 +21532,11 @@ package body Sem_Prag is ...@@ -21513,6 +21532,11 @@ package body Sem_Prag is
Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl); Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl);
end if; end if;
-- Currently it is not possible to inline pre/postconditions on a
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-- Remove the subprogram from the scope stack now that the pre-analysis -- Remove the subprogram from the scope stack now that the pre-analysis
-- of the precondition/postcondition is done. -- of the precondition/postcondition is done.
...@@ -24151,10 +24175,10 @@ package body Sem_Prag is ...@@ -24151,10 +24175,10 @@ package body Sem_Prag is
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
procedure Preanalyze_Test_Case_Arg procedure Preanalyze_Test_Case_Arg
(Arg_Nam : Name_Id; (Arg_Nam : Name_Id;
Subp_Id : Entity_Id); Spec_Id : Entity_Id);
-- Preanalyze one of the optional arguments "Requires" or "Ensures" -- Preanalyze one of the optional arguments "Requires" or "Ensures"
-- denoted by Arg_Nam. Subp_Id is the entity of the subprogram subject -- denoted by Arg_Nam. Spec_Id is the entity of the subprogram spec
-- to pragma Test_Case. -- subject to pragma Test_Case.
------------------------------ ------------------------------
-- Preanalyze_Test_Case_Arg -- -- Preanalyze_Test_Case_Arg --
...@@ -24162,7 +24186,7 @@ package body Sem_Prag is ...@@ -24162,7 +24186,7 @@ package body Sem_Prag is
procedure Preanalyze_Test_Case_Arg procedure Preanalyze_Test_Case_Arg
(Arg_Nam : Name_Id; (Arg_Nam : Name_Id;
Subp_Id : Entity_Id) Spec_Id : Entity_Id)
is is
Arg : Node_Id; Arg : Node_Id;
...@@ -24170,7 +24194,7 @@ package body Sem_Prag is ...@@ -24170,7 +24194,7 @@ package body Sem_Prag is
-- Preanalyze the original aspect argument for ASIS or for a generic -- Preanalyze the original aspect argument for ASIS or for a generic
-- subprogram to properly capture global references. -- subprogram to properly capture global references.
if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then if ASIS_Mode or else Is_Generic_Subprogram (Spec_Id) then
Arg := Arg :=
Test_Case_Arg Test_Case_Arg
(Prag => N, (Prag => N,
...@@ -24192,8 +24216,8 @@ package body Sem_Prag is ...@@ -24192,8 +24216,8 @@ package body Sem_Prag is
-- Local variables -- Local variables
Spec_Id : Entity_Id;
Subp_Decl : Node_Id; Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
Restore_Scope : Boolean := False; Restore_Scope : Boolean := False;
-- Gets set True if we do a Push_Scope needing a Pop_Scope on exit -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
...@@ -24202,25 +24226,30 @@ package body Sem_Prag is ...@@ -24202,25 +24226,30 @@ package body Sem_Prag is
begin begin
Subp_Decl := Find_Related_Subprogram_Or_Body (N); Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl); Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- Ensure that the formal parameters are visible when analyzing all -- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining -- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations. -- to subprogram declarations.
if not In_Open_Scopes (Subp_Id) then if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True; Restore_Scope := True;
Push_Scope (Subp_Id); Push_Scope (Spec_Id);
if Is_Generic_Subprogram (Subp_Id) then if Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Subp_Id); Install_Generic_Formals (Spec_Id);
else else
Install_Formals (Subp_Id); Install_Formals (Spec_Id);
end if; end if;
end if; end if;
Preanalyze_Test_Case_Arg (Name_Requires, Subp_Id); Preanalyze_Test_Case_Arg (Name_Requires, Spec_Id);
Preanalyze_Test_Case_Arg (Name_Ensures, Subp_Id); Preanalyze_Test_Case_Arg (Name_Ensures, Spec_Id);
-- Currently it is not possible to inline pre/postconditions on a
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
if Restore_Scope then if Restore_Scope then
End_Scope; End_Scope;
...@@ -24604,6 +24633,32 @@ package body Sem_Prag is ...@@ -24604,6 +24633,32 @@ package body Sem_Prag is
end if; end if;
end Check_Missing_Part_Of; end Check_Missing_Part_Of;
---------------------------------------------------
-- Check_Postcondition_Use_In_Inlined_Subprogram --
---------------------------------------------------
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Subp_Id : Entity_Id)
is
begin
if Warn_On_Redundant_Constructs
and then Has_Pragma_Inline_Always (Subp_Id)
then
Error_Msg_Name_1 := Original_Aspect_Pragma_Name (Prag);
if From_Aspect_Specification (Prag) then
Error_Msg_NE
("aspect % not enforced on inlined subprogram &?r?",
Corresponding_Aspect (Prag), Subp_Id);
else
Error_Msg_NE
("pragma % not enforced on inlined subprogram &?r?",
Prag, Subp_Id);
end if;
end if;
end Check_Postcondition_Use_In_Inlined_Subprogram;
------------------------------------- -------------------------------------
-- Check_State_And_Constituent_Use -- -- Check_State_And_Constituent_Use --
------------------------------------- -------------------------------------
......
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