[multiple changes]
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com> * aspects.adb Add an entry for entry bodies in table Has_Aspect_Specifications_Flag. (Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain aspects. * contracts.adb (Add_Contract_Items): Code cleanup. Add processing for entry bodies, entry declarations and task units. (Analyze_Subprogram_Body_Contract): Renamed to Analyze_Entry_Or_Subprogram_Body_Contract. Do not analyze the contract of an entry body unless annotating the original tree. (Analyze_Subprogram_Contract): Renamed to Analyze_Entry_Or_Subprogram_Contract. Do not analyze the contract of an entry declaration unless annotating the original tree. (Analyze_Task_Contract): New routine. * contracts.ads (Add_Contract_Item): Update the comment on usage. (Analyze_Package_Body_Contract): Update comment on usage. (Analyze_Package_Contract): Update the comment on usage. (Analyze_Subprogram_Body_Contract): Renamed to Analyze_Entry_Or_Subprogram_Body_Contract. (Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage. (Analyze_Subprogram_Contract): Renamed to Analyze_Entry_Or_Subprogram_Contract. (Analyze_Task_Contract): New routine. * einfo.adb (Contract): Restructure the assertion to include entries and task units. (SPARK_Pragma): This attribute now applies to operators. (SPARK_Pragma_Inherited): This flag now applies to operators. (Set_Contract): Restructure the assertion to include entries and task units. (Set_SPARK_Pragma): This attribute now applies to operators. (Set_SPARK_Pragma_Inherited): This flag now applies to operators. (Write_Field34_Name): Write out all Ekinds that have a contract. (Write_Field40_Name): SPARK_Pragma now applies to operators. * einfo.ads: Update the documentation of attribute Contract along with usage in nodes. Update the documentation of attributes SPARK_Pragma and SPARK_Pragma_Inherited. * exp_ch6.adb (Freeze_Subprogram): Update the call to Analyze_Subprogram_Contract. * par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it is not part of the entry barrier production. (P_Entry_Body): Parse the optional aspect specifications. Diagnose misplaced aspects. * sem_attr.adb (Analyze_Attribute_Old_Result): Update the call to Find_Related_Subprogram_Or_Body. * sem_aux.adb (Unit_Declaration_Node) Add an entry for entry declarations and bodies. * sem_ch3.adb (Analyze_Declarations): Analyze the contracts of entry declarations, entry bodies and task units. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Update the call to Analyze_Subprogram_Body_Contract. (Analyze_Subprogram_Body_Helper): Update the call to Analyze_Subprogram_Body_Contract. * sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect specifications and the contract. * sem_ch10.adb (Analyze_Compilation_Unit): Update the call to Analyze_Subprogram_Contract. * sem_ch12.adb (Save_References_In_Pragma): Update the call to Find_Related_Subprogram_Or_Body. * sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use Unique_Defining_Entity rather than rummaging around in nodes. (Diagnose_Misplaced_Aspects): Update comment on usage. Update the error messages to accomondate the increasing number of contexts. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Analyze_Depends_Global): Update the call to Find_Related_Subprogram_Or_Body. Add processing for entry declarations. (Analyze_Depends_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Task units have no formal parameters to install. (Analyze_Global_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Task units have no formal parameters to install. (Analyze_Global_Item): Use Fix_Msg to handle the increasing number of contexts. (Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body. Perform full analysis when various pragmas appear in an entry body. (Analyze_Pre_Post_Condition): Update the call to Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma appears in an entry body. (Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Analyze_Refined_Depends_Global_Post): Update the call to Find_Related_Subprogram_Or_Body. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Refined_Depends_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain the entity of the spec. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Refined_Global_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain the entity of the spec. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Test_Case_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Check_Dependency_Clause): Use Fix_Msg to handle the increasing number of contexts. (Check_Mode_Restriction_In_Enclosing_Context): Use Fix_Msg to handle the increasing number of contexts. (Collect_Subprogram_Inputs_Outputs): Use the refined versions of the pragmas when the context is an entry body or a task body. (Find_Related_Subprogram_Or_Body): Renamed to Find_Related_Declaration_Or_Body. Add processing for entries and task units. (Fix_Msg): New routine. (Role_Error): Use Fix_Msg to handle the increasing number of contexts. * sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to Find_Related_Declaration_Or_Body. Update the comment on usage. * sem_util.adb (Is_Entry_Body): New routine. (Is_Entry_Declaration): New routine. * sem_util.ads (Is_Entry_Body): New routine. (Is_Entry_Declaration): New routine. 2015-10-26 Ed Schonberg <schonberg@adacore.com> * inline.adb (Has_Excluded_Declaration): A subtype declaration with a predicate aspect generates a subprogram, and therefore prevents the inlining of the enclosing subprogram. * osint.ads: Fix typo. From-SVN: r229333
This commit is contained in:
Arnaud Charlet
parent
1f145d79e9
commit
f99ff327e1
|
|
@ -1,3 +1,126 @@
|
|||
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* aspects.adb Add an entry for entry bodies in table
|
||||
Has_Aspect_Specifications_Flag.
|
||||
(Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain
|
||||
aspects.
|
||||
* contracts.adb (Add_Contract_Items): Code cleanup. Add
|
||||
processing for entry bodies, entry declarations and task units.
|
||||
(Analyze_Subprogram_Body_Contract): Renamed
|
||||
to Analyze_Entry_Or_Subprogram_Body_Contract. Do not
|
||||
analyze the contract of an entry body unless annotating the
|
||||
original tree.
|
||||
(Analyze_Subprogram_Contract): Renamed to
|
||||
Analyze_Entry_Or_Subprogram_Contract. Do not analyze the contract
|
||||
of an entry declaration unless annotating the original tree.
|
||||
(Analyze_Task_Contract): New routine.
|
||||
* contracts.ads (Add_Contract_Item): Update the comment on usage.
|
||||
(Analyze_Package_Body_Contract): Update comment on usage.
|
||||
(Analyze_Package_Contract): Update the comment on usage.
|
||||
(Analyze_Subprogram_Body_Contract): Renamed to
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract.
|
||||
(Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage.
|
||||
(Analyze_Subprogram_Contract): Renamed to
|
||||
Analyze_Entry_Or_Subprogram_Contract.
|
||||
(Analyze_Task_Contract): New routine.
|
||||
* einfo.adb (Contract): Restructure the assertion to include
|
||||
entries and task units.
|
||||
(SPARK_Pragma): This attribute now applies to operators.
|
||||
(SPARK_Pragma_Inherited): This flag now applies to operators.
|
||||
(Set_Contract): Restructure the assertion to include entries and task
|
||||
units.
|
||||
(Set_SPARK_Pragma): This attribute now applies to operators.
|
||||
(Set_SPARK_Pragma_Inherited): This flag now applies to operators.
|
||||
(Write_Field34_Name): Write out all Ekinds that have a contract.
|
||||
(Write_Field40_Name): SPARK_Pragma now applies to operators.
|
||||
* einfo.ads: Update the documentation of attribute Contract along
|
||||
with usage in nodes. Update the documentation of attributes
|
||||
SPARK_Pragma and SPARK_Pragma_Inherited.
|
||||
* exp_ch6.adb (Freeze_Subprogram): Update the call to
|
||||
Analyze_Subprogram_Contract.
|
||||
* par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it
|
||||
is not part of the entry barrier production.
|
||||
(P_Entry_Body): Parse the optional aspect specifications. Diagnose
|
||||
misplaced aspects.
|
||||
* sem_attr.adb (Analyze_Attribute_Old_Result): Update the call
|
||||
to Find_Related_Subprogram_Or_Body.
|
||||
* sem_aux.adb (Unit_Declaration_Node) Add an entry for entry
|
||||
declarations and bodies.
|
||||
* sem_ch3.adb (Analyze_Declarations): Analyze the contracts of
|
||||
entry declarations, entry bodies and task units.
|
||||
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
|
||||
Update the call to Analyze_Subprogram_Body_Contract.
|
||||
(Analyze_Subprogram_Body_Helper): Update the call to
|
||||
Analyze_Subprogram_Body_Contract.
|
||||
* sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect
|
||||
specifications and the contract.
|
||||
* sem_ch10.adb (Analyze_Compilation_Unit): Update the call to
|
||||
Analyze_Subprogram_Contract.
|
||||
* sem_ch12.adb (Save_References_In_Pragma): Update the call to
|
||||
Find_Related_Subprogram_Or_Body.
|
||||
* sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use
|
||||
Unique_Defining_Entity rather than rummaging around in nodes.
|
||||
(Diagnose_Misplaced_Aspects): Update comment on usage. Update the
|
||||
error messages to accomondate the increasing number of contexts.
|
||||
* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
|
||||
Update the call to Find_Related_Subprogram_Or_Body.
|
||||
(Analyze_Depends_Global): Update the call to
|
||||
Find_Related_Subprogram_Or_Body. Add processing for entry
|
||||
declarations.
|
||||
(Analyze_Depends_In_Decl_Part): Update the call
|
||||
to Find_Related_Subprogram_Or_Body. Task units have no formal
|
||||
parameters to install. (Analyze_Global_In_Decl_Part): Update
|
||||
the call to Find_Related_Subprogram_Or_Body. Task units have no
|
||||
formal parameters to install.
|
||||
(Analyze_Global_Item): Use Fix_Msg to handle the increasing number of
|
||||
contexts.
|
||||
(Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body.
|
||||
Perform full analysis when various pragmas appear in an entry body.
|
||||
(Analyze_Pre_Post_Condition): Update the call to
|
||||
Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma
|
||||
appears in an entry body.
|
||||
(Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to
|
||||
Find_Related_Subprogram_Or_Body.
|
||||
(Analyze_Refined_Depends_Global_Post): Update
|
||||
the call to Find_Related_Subprogram_Or_Body. Use
|
||||
Fix_Msg to handle the increasing number of contexts.
|
||||
(Analyze_Refined_Depends_In_Decl_Part): Update
|
||||
the call to Find_Related_Subprogram_Or_Body. Use
|
||||
Unique_Defining_Entity to obtain the entity of the
|
||||
spec. Use Fix_Msg to handle the increasing number of contexts.
|
||||
(Analyze_Refined_Global_In_Decl_Part): Update the call to
|
||||
Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain
|
||||
the entity of the spec. Use Fix_Msg to handle the increasing number of
|
||||
contexts.
|
||||
(Analyze_Test_Case_In_Decl_Part): Update the call to
|
||||
Find_Related_Subprogram_Or_Body.
|
||||
(Check_Dependency_Clause): Use Fix_Msg to handle the increasing number
|
||||
of contexts.
|
||||
(Check_Mode_Restriction_In_Enclosing_Context): Use
|
||||
Fix_Msg to handle the increasing number of contexts.
|
||||
(Collect_Subprogram_Inputs_Outputs): Use the refined
|
||||
versions of the pragmas when the context is an entry body or
|
||||
a task body.
|
||||
(Find_Related_Subprogram_Or_Body): Renamed to
|
||||
Find_Related_Declaration_Or_Body. Add processing for entries
|
||||
and task units.
|
||||
(Fix_Msg): New routine.
|
||||
(Role_Error): Use Fix_Msg to handle the increasing number of contexts.
|
||||
* sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to
|
||||
Find_Related_Declaration_Or_Body. Update the comment on usage.
|
||||
* sem_util.adb (Is_Entry_Body): New routine.
|
||||
(Is_Entry_Declaration): New routine.
|
||||
* sem_util.ads (Is_Entry_Body): New routine.
|
||||
(Is_Entry_Declaration): New routine.
|
||||
|
||||
2015-10-26 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* inline.adb (Has_Excluded_Declaration): A subtype declaration
|
||||
with a predicate aspect generates a subprogram, and therefore
|
||||
prevents the inlining of the enclosing subprogram.
|
||||
* osint.ads: Fix typo.
|
||||
|
||||
|
||||
2015-10-26 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_case.adb (Check_Choice_Set): Choose initial choice range
|
||||
|
|
|
|||
|
|
@ -154,7 +154,8 @@ package body Aspects is
|
|||
|
||||
pragma Assert (Has_Aspects (N));
|
||||
pragma Assert (Nkind (N) in N_Body_Stub
|
||||
or else Nkind_In (N, N_Package_Body,
|
||||
or else Nkind_In (N, N_Entry_Body,
|
||||
N_Package_Body,
|
||||
N_Protected_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Task_Body));
|
||||
|
|
@ -427,6 +428,7 @@ package body Aspects is
|
|||
Has_Aspect_Specifications_Flag : constant array (Node_Kind) of Boolean :=
|
||||
(N_Abstract_Subprogram_Declaration => True,
|
||||
N_Component_Declaration => True,
|
||||
N_Entry_Body => True,
|
||||
N_Entry_Declaration => True,
|
||||
N_Exception_Declaration => True,
|
||||
N_Exception_Renaming_Declaration => True,
|
||||
|
|
|
|||
|
|
@ -121,7 +121,7 @@ package body Contracts is
|
|||
Set_Contract (Id, Items);
|
||||
end if;
|
||||
|
||||
-- Contract items related to constants. Applicable pragmas are:
|
||||
-- Constants, the applicable pragmas are:
|
||||
-- Part_Of
|
||||
|
||||
if Ekind (Id) = E_Constant then
|
||||
|
|
@ -134,24 +134,17 @@ package body Contracts is
|
|||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to [generic] packages or instantiations. The
|
||||
-- applicable pragmas are:
|
||||
-- Abstract_States
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of (instantiation only)
|
||||
-- Entry bodies, the applicable pragmas are:
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
|
||||
elsif Ekind_In (Id, E_Generic_Package, E_Package) then
|
||||
if Nam_In (Prag_Nam, Name_Abstract_State,
|
||||
Name_Initial_Condition,
|
||||
Name_Initializes)
|
||||
then
|
||||
elsif Is_Entry_Body (Id) then
|
||||
if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
|
||||
Add_Classification;
|
||||
|
||||
-- Indicator Part_Of must be associated with a package instantiation
|
||||
|
||||
elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
|
||||
Add_Classification;
|
||||
elsif Prag_Nam = Name_Refined_Post then
|
||||
Add_Pre_Post_Condition;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
|
|
@ -159,21 +152,7 @@ package body Contracts is
|
|||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to package bodies. The applicable pragmas are:
|
||||
-- Refined_States
|
||||
|
||||
elsif Ekind (Id) = E_Package_Body then
|
||||
if Prag_Nam = Name_Refined_State then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to subprogram or entry declarations. The
|
||||
-- applicable pragmas are:
|
||||
-- Entry or subprogram declarations, the applicable pragmas are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Extensions_Visible
|
||||
|
|
@ -183,9 +162,11 @@ package body Contracts is
|
|||
-- Test_Case
|
||||
-- Volatile_Function
|
||||
|
||||
elsif Ekind_In (Id, E_Entry, E_Entry_Family)
|
||||
or else Is_Generic_Subprogram (Id)
|
||||
or else Is_Subprogram (Id)
|
||||
elsif Is_Entry_Declaration (Id)
|
||||
or else Ekind_In (Id, E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Procedure)
|
||||
then
|
||||
if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
|
||||
Add_Pre_Post_Condition;
|
||||
|
|
@ -210,7 +191,44 @@ package body Contracts is
|
|||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to subprogram bodies. Applicable pragmas are:
|
||||
-- Packages or instantiations, the applicable pragmas are:
|
||||
-- Abstract_States
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of (instantiation only)
|
||||
|
||||
elsif Ekind_In (Id, E_Generic_Package, E_Package) then
|
||||
if Nam_In (Prag_Nam, Name_Abstract_State,
|
||||
Name_Initial_Condition,
|
||||
Name_Initializes)
|
||||
then
|
||||
Add_Classification;
|
||||
|
||||
-- Indicator Part_Of must be associated with a package instantiation
|
||||
|
||||
elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Package bodies, the applicable pragmas are:
|
||||
-- Refined_States
|
||||
|
||||
elsif Ekind (Id) = E_Package_Body then
|
||||
if Prag_Nam = Name_Refined_State then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Subprogram bodies, the applicable pragmas are:
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
|
|
@ -233,7 +251,35 @@ package body Contracts is
|
|||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to variables. Applicable pragmas are:
|
||||
-- Task bodies, the applicable pragmas are:
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
|
||||
elsif Ekind (Id) = E_Task_Body then
|
||||
if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Task units, the applicable pragmas are:
|
||||
-- Depends
|
||||
-- Global
|
||||
|
||||
elsif Ekind (Id) = E_Task_Type then
|
||||
if Nam_In (Prag_Nam, Name_Depends, Name_Global) then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Variables, the applicable pragmas are:
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
-- Constant_After_Elaboration
|
||||
|
|
@ -284,6 +330,231 @@ package body Contracts is
|
|||
end loop;
|
||||
end Analyze_Enclosing_Package_Body_Contract;
|
||||
|
||||
-----------------------------------------------
|
||||
-- Analyze_Entry_Or_Subprogram_Body_Contract --
|
||||
-----------------------------------------------
|
||||
|
||||
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
|
||||
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
|
||||
Items : constant Node_Id := Contract (Body_Id);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
|
||||
Mode : SPARK_Mode_Type;
|
||||
|
||||
begin
|
||||
-- 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.
|
||||
|
||||
if Ekind (Body_Id) = E_Void then
|
||||
return;
|
||||
|
||||
-- Do not analyze the contract of an entry body unless annotating the
|
||||
-- original tree. It is preferable to analyze the contract after the
|
||||
-- entry body has been transformed into a subprogram body to properly
|
||||
-- handle references to unpacked formals.
|
||||
|
||||
elsif Ekind_In (Body_Id, E_Entry, E_Entry_Family)
|
||||
and then not ASIS_Mode
|
||||
and then not GNATprove_Mode
|
||||
then
|
||||
return;
|
||||
|
||||
-- Do not analyze a contract multiple times
|
||||
|
||||
elsif Present (Items) then
|
||||
if Analyzed (Items) then
|
||||
return;
|
||||
else
|
||||
Set_Analyzed (Items);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result or
|
||||
-- define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Body_Id);
|
||||
|
||||
-- A stand-alone nonvolatile function body cannot have an effectively
|
||||
-- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
|
||||
-- check is relevant only when SPARK_Mode is on, as it is not a standard
|
||||
-- legality rule. The check is performed here because Volatile_Function
|
||||
-- is processed after the analysis of the related subprogram body.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Body_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Body_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
|
||||
-- Capture all global references in a generic subprogram body now that
|
||||
-- the contract has been analyzed.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Body_Decl) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Body_Decl),
|
||||
Gen_Id => Spec_Id);
|
||||
end if;
|
||||
|
||||
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
|
||||
-- invariants and predicates associated with body and its spec. Do not
|
||||
-- expand the contract of subprogram body stubs.
|
||||
|
||||
if Nkind (Body_Decl) = N_Subprogram_Body then
|
||||
Expand_Subprogram_Contract (Body_Id);
|
||||
end if;
|
||||
end Analyze_Entry_Or_Subprogram_Body_Contract;
|
||||
|
||||
------------------------------------------
|
||||
-- Analyze_Entry_Or_Subprogram_Contract --
|
||||
------------------------------------------
|
||||
|
||||
procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Subp_Id);
|
||||
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
||||
Depends : Node_Id := Empty;
|
||||
Global : Node_Id := Empty;
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
Prag_Nam : Name_Id;
|
||||
|
||||
begin
|
||||
-- Do not analyze the contract of an entry declaration unless annotating
|
||||
-- the original tree. It is preferable to analyze the contract after the
|
||||
-- entry declaration has been transformed into a subprogram declaration
|
||||
-- to properly handle references to unpacked formals.
|
||||
|
||||
if Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
|
||||
and then not ASIS_Mode
|
||||
and then not GNATprove_Mode
|
||||
then
|
||||
return;
|
||||
|
||||
-- Do not analyze a contract multiple times
|
||||
|
||||
elsif Present (Items) then
|
||||
if Analyzed (Items) then
|
||||
return;
|
||||
else
|
||||
Set_Analyzed (Items);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Subp_Id, Mode);
|
||||
|
||||
-- All subprograms carry a contract, but for some it is not significant
|
||||
-- and should not be processed.
|
||||
|
||||
if not Has_Significant_Contract (Subp_Id) then
|
||||
null;
|
||||
|
||||
elsif Present (Items) then
|
||||
|
||||
-- Analyze pre- and postconditions
|
||||
|
||||
Prag := Pre_Post_Conditions (Items);
|
||||
while Present (Prag) loop
|
||||
Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze contract-cases and test-cases
|
||||
|
||||
Prag := Contract_Test_Cases (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Contract_Cases then
|
||||
Analyze_Contract_Cases_In_Decl_Part (Prag);
|
||||
else
|
||||
pragma Assert (Prag_Nam = Name_Test_Case);
|
||||
Analyze_Test_Case_In_Decl_Part (Prag);
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze classification pragmas
|
||||
|
||||
Prag := Classifications (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Depends then
|
||||
Depends := Prag;
|
||||
|
||||
elsif Prag_Nam = Name_Global then
|
||||
Global := Prag;
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze Global first, as Depends may mention items classified in
|
||||
-- the global categorization.
|
||||
|
||||
if Present (Global) then
|
||||
Analyze_Global_In_Decl_Part (Global);
|
||||
end if;
|
||||
|
||||
-- Depends must be analyzed after Global in order to see the modes of
|
||||
-- all global items.
|
||||
|
||||
if Present (Depends) then
|
||||
Analyze_Depends_In_Decl_Part (Depends);
|
||||
end if;
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result
|
||||
-- or define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- A nonvolatile function cannot have an effectively volatile formal
|
||||
-- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
|
||||
-- only when SPARK_Mode is on, as it is not a standard legality rule.
|
||||
-- The check is performed here because pragma Volatile_Function is
|
||||
-- processed after the analysis of the related subprogram declaration.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Subp_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
|
||||
-- Capture all global references in a generic subprogram now that the
|
||||
-- contract has been analyzed.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Subp_Decl) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Subp_Decl),
|
||||
Gen_Id => Subp_Id);
|
||||
end if;
|
||||
end Analyze_Entry_Or_Subprogram_Contract;
|
||||
|
||||
-----------------------------
|
||||
-- Analyze_Object_Contract --
|
||||
-----------------------------
|
||||
|
|
@ -617,209 +888,6 @@ package body Contracts is
|
|||
end if;
|
||||
end Analyze_Package_Contract;
|
||||
|
||||
--------------------------------------
|
||||
-- Analyze_Subprogram_Body_Contract --
|
||||
--------------------------------------
|
||||
|
||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
|
||||
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
|
||||
Items : constant Node_Id := Contract (Body_Id);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
|
||||
Mode : SPARK_Mode_Type;
|
||||
|
||||
begin
|
||||
-- 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.
|
||||
|
||||
if Ekind (Body_Id) = E_Void then
|
||||
return;
|
||||
|
||||
-- Do not analyze a contract multiple times
|
||||
|
||||
elsif Present (Items) then
|
||||
if Analyzed (Items) then
|
||||
return;
|
||||
else
|
||||
Set_Analyzed (Items);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result or
|
||||
-- define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Body_Id);
|
||||
|
||||
-- A stand-alone nonvolatile function body cannot have an effectively
|
||||
-- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
|
||||
-- check is relevant only when SPARK_Mode is on, as it is not a standard
|
||||
-- legality rule. The check is performed here because Volatile_Function
|
||||
-- is processed after the analysis of the related subprogram body.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Body_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Body_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
|
||||
-- Capture all global references in a generic subprogram body now that
|
||||
-- the contract has been analyzed.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Body_Decl) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Body_Decl),
|
||||
Gen_Id => Spec_Id);
|
||||
end if;
|
||||
|
||||
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
|
||||
-- invariants and predicates associated with body and its spec. Do not
|
||||
-- expand the contract of subprogram body stubs.
|
||||
|
||||
if Nkind (Body_Decl) = N_Subprogram_Body then
|
||||
Expand_Subprogram_Contract (Body_Id);
|
||||
end if;
|
||||
end Analyze_Subprogram_Body_Contract;
|
||||
|
||||
---------------------------------
|
||||
-- Analyze_Subprogram_Contract --
|
||||
---------------------------------
|
||||
|
||||
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Subp_Id);
|
||||
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
||||
Depends : Node_Id := Empty;
|
||||
Global : Node_Id := Empty;
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
Prag_Nam : Name_Id;
|
||||
|
||||
begin
|
||||
-- Do not analyze a contract multiple times
|
||||
|
||||
if Present (Items) then
|
||||
if Analyzed (Items) then
|
||||
return;
|
||||
else
|
||||
Set_Analyzed (Items);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Subp_Id, Mode);
|
||||
|
||||
-- All subprograms carry a contract, but for some it is not significant
|
||||
-- and should not be processed.
|
||||
|
||||
if not Has_Significant_Contract (Subp_Id) then
|
||||
null;
|
||||
|
||||
elsif Present (Items) then
|
||||
|
||||
-- Analyze pre- and postconditions
|
||||
|
||||
Prag := Pre_Post_Conditions (Items);
|
||||
while Present (Prag) loop
|
||||
Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze contract-cases and test-cases
|
||||
|
||||
Prag := Contract_Test_Cases (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Contract_Cases then
|
||||
Analyze_Contract_Cases_In_Decl_Part (Prag);
|
||||
else
|
||||
pragma Assert (Prag_Nam = Name_Test_Case);
|
||||
Analyze_Test_Case_In_Decl_Part (Prag);
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze classification pragmas
|
||||
|
||||
Prag := Classifications (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Depends then
|
||||
Depends := Prag;
|
||||
|
||||
elsif Prag_Nam = Name_Global then
|
||||
Global := Prag;
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze Global first, as Depends may mention items classified in
|
||||
-- the global categorization.
|
||||
|
||||
if Present (Global) then
|
||||
Analyze_Global_In_Decl_Part (Global);
|
||||
end if;
|
||||
|
||||
-- Depends must be analyzed after Global in order to see the modes of
|
||||
-- all global items.
|
||||
|
||||
if Present (Depends) then
|
||||
Analyze_Depends_In_Decl_Part (Depends);
|
||||
end if;
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result
|
||||
-- or define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- A nonvolatile function cannot have an effectively volatile formal
|
||||
-- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
|
||||
-- only when SPARK_Mode is on, as it is not a standard legality rule.
|
||||
-- The check is performed here because pragma Volatile_Function is
|
||||
-- processed after the analysis of the related subprogram declaration.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Subp_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
|
||||
-- Capture all global references in a generic subprogram now that the
|
||||
-- contract has been analyzed.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Subp_Decl) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Subp_Decl),
|
||||
Gen_Id => Subp_Id);
|
||||
end if;
|
||||
end Analyze_Subprogram_Contract;
|
||||
|
||||
-------------------------------------------
|
||||
-- Analyze_Subprogram_Body_Stub_Contract --
|
||||
-------------------------------------------
|
||||
|
|
@ -838,7 +906,7 @@ package body Contracts is
|
|||
-- Refined_Global
|
||||
|
||||
if Present (Spec_Id) then
|
||||
Analyze_Subprogram_Body_Contract (Stub_Id);
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
|
||||
|
||||
-- The stub acts as its own spec, the applicable pragmas are:
|
||||
-- Contract_Cases
|
||||
|
|
@ -849,10 +917,61 @@ package body Contracts is
|
|||
-- Test_Case
|
||||
|
||||
else
|
||||
Analyze_Subprogram_Contract (Stub_Id);
|
||||
Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
|
||||
end if;
|
||||
end Analyze_Subprogram_Body_Stub_Contract;
|
||||
|
||||
---------------------------
|
||||
-- Analyze_Task_Contract --
|
||||
---------------------------
|
||||
|
||||
procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Task_Id);
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
|
||||
begin
|
||||
-- Do not analyze a contract multiple times
|
||||
|
||||
if Present (Items) then
|
||||
if Analyzed (Items) then
|
||||
return;
|
||||
else
|
||||
Set_Analyzed (Items);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Task_Id, Mode);
|
||||
|
||||
-- Analyze Global first, as Depends may mention items classified in the
|
||||
-- global categorization.
|
||||
|
||||
Prag := Get_Pragma (Task_Id, Pragma_Global);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_Global_In_Decl_Part (Prag);
|
||||
end if;
|
||||
|
||||
-- Depends must be analyzed after Global in order to see the modes of
|
||||
-- all global items.
|
||||
|
||||
Prag := Get_Pragma (Task_Id, Pragma_Depends);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_Depends_In_Decl_Part (Prag);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
end Analyze_Task_Contract;
|
||||
|
||||
-----------------------------
|
||||
-- Create_Generic_Contract --
|
||||
-----------------------------
|
||||
|
|
|
|||
|
|
@ -31,9 +31,9 @@ with Types; use Types;
|
|||
package Contracts is
|
||||
|
||||
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
|
||||
-- Add pragma Prag to the contract of a constant, entry, package [body],
|
||||
-- subprogram [body], or variable denoted by Id. The following are valid
|
||||
-- pragmas:
|
||||
-- Add pragma Prag to the contract of a constant, entry, entry family,
|
||||
-- [generic] package, package body, [generic] subprogram, subprogram body,
|
||||
-- variable or task unit denoted by Id. The following are valid pragmas:
|
||||
-- Abstract_State
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
|
|
@ -60,6 +60,31 @@ package Contracts is
|
|||
-- Analyze the contract of the nearest package body (if any) enclosing
|
||||
-- package or subprogram body Body_Decl.
|
||||
|
||||
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
|
||||
-- Analyze all delayed pragmas chained on the contract of entry or
|
||||
-- subprogram body Body_Id as if they appeared at the end of a declarative
|
||||
-- region. Pragmas in question are:
|
||||
-- Contract_Cases (stand alone subprogram body)
|
||||
-- Depends (stand alone subprogram body)
|
||||
-- Global (stand alone subprogram body)
|
||||
-- Postcondition (stand alone subprogram body)
|
||||
-- Precondition (stand alone subprogram body)
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case (stand alone subprogram body)
|
||||
|
||||
procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id);
|
||||
-- Analyze all delayed pragmas chained on the contract of entry or
|
||||
-- subprogram Subp_Id as if they appeared at the end of a declarative
|
||||
-- region. The pragmas in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
|
||||
procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
|
||||
-- Analyze all delayed pragmas chained on the contract of object Obj_Id as
|
||||
-- if they appeared at the end of the declarative region. The pragmas to be
|
||||
|
|
@ -73,51 +98,26 @@ package Contracts is
|
|||
procedure Analyze_Package_Body_Contract
|
||||
(Body_Id : Entity_Id;
|
||||
Freeze_Id : Entity_Id := Empty);
|
||||
-- Analyze all delayed aspects chained on the contract of package body
|
||||
-- Analyze all delayed pragmas chained on the contract of package body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects that are considered are:
|
||||
-- pragmas that are considered are:
|
||||
-- Refined_State
|
||||
--
|
||||
-- Freeze_Id is the entity of a [generic] package body or a [generic]
|
||||
-- subprogram body which "freezes" the contract of Body_Id.
|
||||
|
||||
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of package Pack_Id
|
||||
-- as if they appeared at the end of a declarative region. The aspects
|
||||
-- Analyze all delayed pragmas chained on the contract of package Pack_Id
|
||||
-- as if they appeared at the end of a declarative region. The pragmas
|
||||
-- that are considered are:
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of
|
||||
|
||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. Aspects
|
||||
-- in question are:
|
||||
-- Contract_Cases (stand alone body)
|
||||
-- Depends (stand alone body)
|
||||
-- Global (stand alone body)
|
||||
-- Postcondition (stand alone body)
|
||||
-- Precondition (stand alone body)
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case (stand alone body)
|
||||
|
||||
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram
|
||||
-- Subp_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
|
||||
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of a subprogram body
|
||||
-- Analyze all delayed pragmas chained on the contract of a subprogram body
|
||||
-- stub Stub_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- pragmas in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
|
|
@ -128,6 +128,13 @@ package Contracts is
|
|||
-- Refined_Post
|
||||
-- Test_Case
|
||||
|
||||
procedure Analyze_Task_Contract (Task_Id : Entity_Id);
|
||||
-- Analyze all delayed pragmas chained on the contract of a task unit
|
||||
-- Task_Id as if they appeared at the end of a declarative region. The
|
||||
-- pragmas in question are:
|
||||
-- Depends
|
||||
-- Global
|
||||
|
||||
procedure Create_Generic_Contract (Unit : Node_Id);
|
||||
-- Create a contract node for a generic package, generic subprogram, or a
|
||||
-- generic body denoted by Unit by collecting all source contract-related
|
||||
|
|
|
|||
|
|
@ -1205,16 +1205,25 @@ package body Einfo is
|
|||
function Contract (Id : E) return N is
|
||||
begin
|
||||
pragma Assert
|
||||
(Ekind_In (Id, E_Constant,
|
||||
E_Entry,
|
||||
(Ekind_In (Id, E_Constant, -- object variants
|
||||
E_Variable)
|
||||
or else
|
||||
Ekind_In (Id, E_Entry, -- overloadable variants
|
||||
E_Entry_Family,
|
||||
E_Generic_Package,
|
||||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
Ekind_In (Id, E_Generic_Package, -- package variants
|
||||
E_Package,
|
||||
E_Package_Body,
|
||||
E_Subprogram_Body,
|
||||
E_Variable,
|
||||
E_Void)
|
||||
or else Is_Subprogram_Or_Generic_Subprogram (Id));
|
||||
E_Package_Body)
|
||||
or else
|
||||
Ekind_In (Id, E_Task_Body, -- synchronized variants
|
||||
E_Task_Type,
|
||||
E_Void)); -- special purpose
|
||||
return Node34 (Id);
|
||||
end Contract;
|
||||
|
||||
|
|
@ -3139,6 +3148,7 @@ package body Einfo is
|
|||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
|
|
@ -3161,6 +3171,7 @@ package body Einfo is
|
|||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
|
|
@ -3834,16 +3845,25 @@ package body Einfo is
|
|||
procedure Set_Contract (Id : E; V : N) is
|
||||
begin
|
||||
pragma Assert
|
||||
(Ekind_In (Id, E_Constant,
|
||||
E_Entry,
|
||||
(Ekind_In (Id, E_Constant, -- object variants
|
||||
E_Variable)
|
||||
or else
|
||||
Ekind_In (Id, E_Entry, -- overloadable variants
|
||||
E_Entry_Family,
|
||||
E_Generic_Package,
|
||||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
Ekind_In (Id, E_Generic_Package, -- package variants
|
||||
E_Package,
|
||||
E_Package_Body,
|
||||
E_Subprogram_Body,
|
||||
E_Variable,
|
||||
E_Void)
|
||||
or else Is_Subprogram_Or_Generic_Subprogram (Id));
|
||||
E_Package_Body)
|
||||
or else
|
||||
Ekind_In (Id, E_Task_Body, -- synchronized variants
|
||||
E_Task_Type,
|
||||
E_Void)); -- special purpose
|
||||
Set_Node34 (Id, V);
|
||||
end Set_Contract;
|
||||
|
||||
|
|
@ -6170,6 +6190,7 @@ package body Einfo is
|
|||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
|
|
@ -6192,6 +6213,7 @@ package body Einfo is
|
|||
E_Function,
|
||||
E_Generic_Function,
|
||||
E_Generic_Procedure,
|
||||
E_Operator,
|
||||
E_Procedure,
|
||||
E_Subprogram_Body)
|
||||
or else
|
||||
|
|
@ -10212,14 +10234,19 @@ package body Einfo is
|
|||
when E_Constant |
|
||||
E_Entry |
|
||||
E_Entry_Family |
|
||||
E_Function |
|
||||
E_Generic_Function |
|
||||
E_Generic_Package |
|
||||
E_Generic_Procedure |
|
||||
E_Operator |
|
||||
E_Package |
|
||||
E_Package_Body |
|
||||
E_Procedure |
|
||||
E_Subprogram_Body |
|
||||
E_Task_Body |
|
||||
E_Task_Type |
|
||||
E_Variable |
|
||||
E_Void |
|
||||
Generic_Subprogram_Kind |
|
||||
Subprogram_Kind =>
|
||||
E_Void =>
|
||||
Write_Str ("Contract");
|
||||
|
||||
when others =>
|
||||
|
|
@ -10317,6 +10344,7 @@ package body Einfo is
|
|||
E_Generic_Function |
|
||||
E_Generic_Package |
|
||||
E_Generic_Procedure |
|
||||
E_Operator |
|
||||
E_Package |
|
||||
E_Package_Body |
|
||||
E_Procedure |
|
||||
|
|
|
|||
|
|
@ -705,10 +705,10 @@ package Einfo is
|
|||
-- of declaration, procedure call, assignment statement or pragma.
|
||||
|
||||
-- Contract (Node34)
|
||||
-- Defined in constant, entry, entry family, [generic] package, package
|
||||
-- body, [generic] subprogram, subprogram body, and variable entities.
|
||||
-- Points to the contract of the entity, holding various assertion items
|
||||
-- and data classifiers.
|
||||
-- Defined in constant, entry, entry family, operator, [generic] package,
|
||||
-- package body, [generic] subprogram, subprogram body, variable and task
|
||||
-- type entities. Points to the contract of the entity, holding various
|
||||
-- assertion items and data classifiers.
|
||||
|
||||
-- Corresponding_Concurrent_Type (Node18)
|
||||
-- Defined in record types that are constructed by the expander to
|
||||
|
|
@ -4087,19 +4087,20 @@ package Einfo is
|
|||
-- inherited, rather than a local one.
|
||||
|
||||
-- SPARK_Pragma (Node40)
|
||||
-- Present in entries, [generic] package specs, package bodies, [generic]
|
||||
-- subprogram specs, subprogram bodies and synchronized types. Points to
|
||||
-- the N_Pragma node that applies to the spec or body. This is either set
|
||||
-- by a local SPARK_Mode pragma or is inherited from the context (from an
|
||||
-- outer scope for the spec case or from the spec for the body case). In
|
||||
-- the case where it is inherited the flag SPARK_Pragma_Inherited is set.
|
||||
-- Empty if no SPARK_Mode pragma is applicable.
|
||||
-- Present in entries, operators, [generic] packages, package bodies,
|
||||
-- [generic] subprograms, subprogram bodies and synchronized types.
|
||||
-- Points to the N_Pragma node that applies to the spec or body. This
|
||||
-- is either set by a local SPARK_Mode pragma or is inherited from the
|
||||
-- context (from an outer scope for the spec case or from the spec for
|
||||
-- the body case). In the case where it is inherited the flag
|
||||
-- SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is
|
||||
-- applicable.
|
||||
|
||||
-- SPARK_Pragma_Inherited (Flag265)
|
||||
-- Present in entries, [generic] package specs, package bodies, [generic]
|
||||
-- subprogram specs, subprogram bodies and synchronized types. Set if the
|
||||
-- SPARK_Pragma attribute points to a pragma that is inherited, rather
|
||||
-- than a local one.
|
||||
-- Present in entries, operators, [generic] packages, package bodies,
|
||||
-- [generic] subprograms, subprogram bodies and synchronized types. Set
|
||||
-- if the SPARK_Pragma attribute points to a pragma that is inherited,
|
||||
-- rather than a local one.
|
||||
|
||||
-- Spec_Entity (Node19)
|
||||
-- Defined in package body entities. Points to corresponding package
|
||||
|
|
@ -6041,13 +6042,15 @@ package Einfo is
|
|||
-- Linker_Section_Pragma (Node33)
|
||||
-- Contract (Node34)
|
||||
-- Import_Pragma (Node35)
|
||||
-- SPARK_Pragma (Node40)
|
||||
-- Default_Expressions_Processed (Flag108)
|
||||
-- Has_Invariants (Flag232)
|
||||
-- Has_Nested_Subprogram (Flag282)
|
||||
-- Is_Machine_Code_Subprogram (Flag137)
|
||||
-- Is_Pure (Flag44)
|
||||
-- Is_Intrinsic_Subprogram (Flag64)
|
||||
-- Is_Machine_Code_Subprogram (Flag137)
|
||||
-- Is_Primitive (Flag218)
|
||||
-- Default_Expressions_Processed (Flag108)
|
||||
-- Is_Pure (Flag44)
|
||||
-- SPARK_Pragma_Inherited (Flag265)
|
||||
-- Aren't there more flags and fields? seems like this list should be
|
||||
-- more similar to the E_Function list, which is much longer ???
|
||||
|
||||
|
|
@ -6378,6 +6381,7 @@ package Einfo is
|
|||
-- (plus type attributes)
|
||||
|
||||
-- E_Task_Body
|
||||
-- Contract (Node34)
|
||||
-- SPARK_Pragma (Node40)
|
||||
-- SPARK_Pragma_Inherited (Flag265)
|
||||
-- (any others??? First/Last Entity, Scope_Depth???)
|
||||
|
|
@ -6396,6 +6400,7 @@ package Einfo is
|
|||
-- Task_Body_Procedure (Node25)
|
||||
-- Storage_Size_Variable (Node26) (base type only)
|
||||
-- Relative_Deadline_Variable (Node28) (base type only)
|
||||
-- Contract (Node34)
|
||||
-- SPARK_Pragma (Node40)
|
||||
-- SPARK_Aux_Pragma (Node41)
|
||||
-- Delay_Cleanups (Flag114)
|
||||
|
|
|
|||
|
|
@ -7105,7 +7105,7 @@ package body Exp_Ch6 is
|
|||
if Nkind (Parent (Subp)) = N_Procedure_Specification
|
||||
and then Null_Present (Parent (Subp))
|
||||
then
|
||||
Analyze_Subprogram_Contract (Subp);
|
||||
Analyze_Entry_Or_Subprogram_Contract (Subp);
|
||||
end if;
|
||||
end Freeze_Subprogram;
|
||||
|
||||
|
|
|
|||
|
|
@ -3513,6 +3513,37 @@ package body Inline is
|
|||
("cannot inline & (nested procedure instantiation)?",
|
||||
D, Subp);
|
||||
return True;
|
||||
|
||||
-- Subtype declarations with predicates will generate predicate
|
||||
-- functions, i.e. nested subprogram bodies, so inlining is not
|
||||
-- possible.
|
||||
|
||||
elsif Nkind (D) = N_Subtype_Declaration
|
||||
and then Present (Aspect_Specifications (D))
|
||||
then
|
||||
declare
|
||||
A : Node_Id;
|
||||
A_Id : Aspect_Id;
|
||||
|
||||
begin
|
||||
A := First (Aspect_Specifications (D));
|
||||
while Present (A) loop
|
||||
A_Id := Get_Aspect_Id (Chars (Identifier (A)));
|
||||
|
||||
if A_Id = Aspect_Predicate
|
||||
or else A_Id = Aspect_Static_Predicate
|
||||
or else A_Id = Aspect_Dynamic_Predicate
|
||||
then
|
||||
Cannot_Inline
|
||||
("cannot inline & "
|
||||
& "(subtype declaration with predicate)?",
|
||||
D, Subp);
|
||||
return True;
|
||||
end if;
|
||||
|
||||
Next (A);
|
||||
end loop;
|
||||
end;
|
||||
end if;
|
||||
|
||||
Next (D);
|
||||
|
|
|
|||
|
|
@ -760,7 +760,7 @@ private
|
|||
-- for this file. This routine merely constructs the name.
|
||||
|
||||
procedure Write_Info (Info : String);
|
||||
-- Implement Write_Binder_Info, Write_Debug_Info, and Write_Library_Info
|
||||
-- Implements Write_Binder_Info, Write_Debug_Info, and Write_Library_Info
|
||||
|
||||
procedure Write_With_Check (A : Address; N : Integer);
|
||||
-- Writes N bytes from buffer starting at address A to file whose FD is
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2015, 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- --
|
||||
|
|
@ -1089,7 +1089,6 @@ package body Ch9 is
|
|||
Resync_Past_Semicolon;
|
||||
Pop_Scope_Stack; -- discard unused entry
|
||||
return Error;
|
||||
|
||||
end P_Accept_Statement;
|
||||
|
||||
------------------------
|
||||
|
|
@ -1098,12 +1097,45 @@ package body Ch9 is
|
|||
|
||||
-- Parsed by P_Expression (4.4)
|
||||
|
||||
--------------------------
|
||||
-- 9.5.2 Entry Barrier --
|
||||
--------------------------
|
||||
|
||||
-- ENTRY_BARRIER ::= when CONDITION
|
||||
|
||||
-- Error_Recovery: cannot raise Error_Resync
|
||||
|
||||
function P_Entry_Barrier return Node_Id is
|
||||
Bnode : Node_Id;
|
||||
|
||||
begin
|
||||
if Token = Tok_When then
|
||||
Scan; -- past WHEN;
|
||||
Bnode := P_Expression_No_Right_Paren;
|
||||
|
||||
if Token = Tok_Colon_Equal then
|
||||
Error_Msg_SC -- CODEFIX
|
||||
("|"":="" should be ""=""");
|
||||
Scan;
|
||||
Bnode := P_Expression_No_Right_Paren;
|
||||
end if;
|
||||
|
||||
else
|
||||
T_When; -- to give error message
|
||||
Bnode := Error;
|
||||
end if;
|
||||
|
||||
return Bnode;
|
||||
end P_Entry_Barrier;
|
||||
|
||||
-----------------------
|
||||
-- 9.5.2 Entry Body --
|
||||
-----------------------
|
||||
|
||||
-- ENTRY_BODY ::=
|
||||
-- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART ENTRY_BARRIER is
|
||||
-- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART
|
||||
-- [ASPECT_SPECIFICATIONS] ENTRY_BARRIER
|
||||
-- is
|
||||
-- DECLARATIVE_PART
|
||||
-- begin
|
||||
-- HANDLED_SEQUENCE_OF_STATEMENTS
|
||||
|
|
@ -1114,6 +1146,7 @@ package body Ch9 is
|
|||
-- Error_Recovery: cannot raise Error_Resync
|
||||
|
||||
function P_Entry_Body return Node_Id is
|
||||
Dummy_Node : Node_Id;
|
||||
Entry_Node : Node_Id;
|
||||
Formal_Part_Node : Node_Id;
|
||||
Name_Node : Node_Id;
|
||||
|
|
@ -1135,8 +1168,34 @@ package body Ch9 is
|
|||
Formal_Part_Node := P_Entry_Body_Formal_Part;
|
||||
Set_Entry_Body_Formal_Part (Entry_Node, Formal_Part_Node);
|
||||
|
||||
-- Ada 2012 (AI12-0169): Aspect specifications may appear on an entry
|
||||
-- body immediately after the formal part. Do not parse the aspect
|
||||
-- specifications directly because the "when" of the entry barrier may
|
||||
-- be interpreted as a misused "with".
|
||||
|
||||
if Token = Tok_With then
|
||||
P_Aspect_Specifications (Entry_Node, Semicolon => False);
|
||||
end if;
|
||||
|
||||
Set_Condition (Formal_Part_Node, P_Entry_Barrier);
|
||||
|
||||
-- Detect an illegal placement of aspect specifications following the
|
||||
-- entry barrier.
|
||||
|
||||
-- entry E ... when Barrier with Aspect is
|
||||
|
||||
if Token = Tok_With then
|
||||
Error_Msg_SC ("aspect specifications must come before entry barrier");
|
||||
|
||||
-- Consume the illegal aspects to allow for parsing to continue
|
||||
|
||||
Dummy_Node := New_Node (N_Entry_Body, Sloc (Entry_Node));
|
||||
P_Aspect_Specifications (Dummy_Node, Semicolon => False);
|
||||
end if;
|
||||
|
||||
TF_Is;
|
||||
Parse_Decls_Begin_End (Entry_Node);
|
||||
|
||||
return Entry_Node;
|
||||
end P_Entry_Body;
|
||||
|
||||
|
|
@ -1185,38 +1244,6 @@ package body Ch9 is
|
|||
return Fpart_Node;
|
||||
end P_Entry_Body_Formal_Part;
|
||||
|
||||
--------------------------
|
||||
-- 9.5.2 Entry Barrier --
|
||||
--------------------------
|
||||
|
||||
-- ENTRY_BARRIER ::= when CONDITION
|
||||
|
||||
-- Error_Recovery: cannot raise Error_Resync
|
||||
|
||||
function P_Entry_Barrier return Node_Id is
|
||||
Bnode : Node_Id;
|
||||
|
||||
begin
|
||||
if Token = Tok_When then
|
||||
Scan; -- past WHEN;
|
||||
Bnode := P_Expression_No_Right_Paren;
|
||||
|
||||
if Token = Tok_Colon_Equal then
|
||||
Error_Msg_SC -- CODEFIX
|
||||
("|"":="" should be ""=""");
|
||||
Scan;
|
||||
Bnode := P_Expression_No_Right_Paren;
|
||||
end if;
|
||||
|
||||
else
|
||||
T_When; -- to give error message
|
||||
Bnode := Error;
|
||||
end if;
|
||||
|
||||
TF_Is;
|
||||
return Bnode;
|
||||
end P_Entry_Barrier;
|
||||
|
||||
--------------------------------------
|
||||
-- 9.5.2 Entry Index Specification --
|
||||
--------------------------------------
|
||||
|
|
|
|||
|
|
@ -1330,7 +1330,7 @@ package body Sem_Attr is
|
|||
if Nkind (Prag) = N_Aspect_Specification then
|
||||
Subp_Decl := Parent (Prag);
|
||||
else
|
||||
Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
|
||||
Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
|
||||
end if;
|
||||
|
||||
-- The aspect or pragma where the attribute resides should be
|
||||
|
|
|
|||
|
|
@ -819,8 +819,8 @@ package body Sem_Aux is
|
|||
-- Generic subprogram body
|
||||
|
||||
elsif Is_Subprogram (S)
|
||||
and then Nkind (Unit_Declaration_Node (S))
|
||||
= N_Generic_Subprogram_Declaration
|
||||
and then Nkind (Unit_Declaration_Node (S)) =
|
||||
N_Generic_Subprogram_Declaration
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
|
|
@ -1649,6 +1649,8 @@ package body Sem_Aux is
|
|||
-- Isn't there some better way to express the following ???
|
||||
|
||||
while Nkind (N) /= N_Abstract_Subprogram_Declaration
|
||||
and then Nkind (N) /= N_Entry_Body
|
||||
and then Nkind (N) /= N_Entry_Declaration
|
||||
and then Nkind (N) /= N_Formal_Package_Declaration
|
||||
and then Nkind (N) /= N_Function_Instantiation
|
||||
and then Nkind (N) /= N_Generic_Package_Declaration
|
||||
|
|
|
|||
|
|
@ -939,7 +939,7 @@ package body Sem_Ch10 is
|
|||
if Nkind_In (Unit_Node, N_Generic_Subprogram_Declaration,
|
||||
N_Subprogram_Declaration)
|
||||
then
|
||||
Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
|
||||
Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Unit_Node));
|
||||
end if;
|
||||
|
||||
-- Generate distribution stubs if requested and no error
|
||||
|
|
|
|||
|
|
@ -14796,10 +14796,9 @@ package body Sem_Ch12 is
|
|||
elsif Is_Generic_Contract_Pragma (Prag) and then Prag /= Templ then
|
||||
if Is_Package_Contract_Annotation (Prag) then
|
||||
Context := Find_Related_Package_Or_Body (Prag);
|
||||
|
||||
else
|
||||
pragma Assert (Is_Subprogram_Contract_Annotation (Prag));
|
||||
Context := Find_Related_Subprogram_Or_Body (Prag);
|
||||
Context := Find_Related_Declaration_Or_Body (Prag);
|
||||
end if;
|
||||
|
||||
-- The use of Original_Node accounts for the case when the
|
||||
|
|
|
|||
|
|
@ -3474,9 +3474,9 @@ package body Sem_Ch13 is
|
|||
Body_Id : constant Entity_Id := Defining_Entity (N);
|
||||
|
||||
procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id);
|
||||
-- Subprogram body [stub] N has aspects, but they are not properly
|
||||
-- placed. Emit an error message depending on the aspects involved.
|
||||
-- Spec_Id is the entity of the corresponding spec.
|
||||
-- Body [stub] N has aspects, but they are not properly placed. Emit an
|
||||
-- error message depending on the aspects involved. Spec_Id denotes the
|
||||
-- entity of the corresponding spec.
|
||||
|
||||
--------------------------------
|
||||
-- Diagnose_Misplaced_Aspects --
|
||||
|
|
@ -3532,7 +3532,7 @@ package body Sem_Ch13 is
|
|||
|
||||
else
|
||||
Error_Msg_N
|
||||
("aspect specification must appear in subprogram declaration",
|
||||
("aspect specification must appear on initial declaration",
|
||||
Asp);
|
||||
end if;
|
||||
end Misplaced_Aspect_Error;
|
||||
|
|
@ -3574,7 +3574,7 @@ package body Sem_Ch13 is
|
|||
|
||||
else
|
||||
Error_Msg_N
|
||||
("aspect specification must appear in subprogram declaration",
|
||||
("aspect specification must appear on initial declaration",
|
||||
Asp);
|
||||
end if;
|
||||
|
||||
|
|
@ -3584,23 +3584,17 @@ package body Sem_Ch13 is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Spec_Id : Entity_Id;
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (N);
|
||||
|
||||
-- Start of processing for Analyze_Aspects_On_Body_Or_Stub
|
||||
|
||||
begin
|
||||
if Nkind (N) = N_Subprogram_Body_Stub then
|
||||
Spec_Id := Corresponding_Spec_Of_Stub (N);
|
||||
else
|
||||
Spec_Id := Corresponding_Spec (N);
|
||||
end if;
|
||||
|
||||
-- Language-defined aspects cannot be associated with a subprogram body
|
||||
-- [stub] if the subprogram has a spec. Certain implementation defined
|
||||
-- aspects are allowed to break this rule (for all applicable cases, see
|
||||
-- table Aspects.Aspect_On_Body_Or_Stub_OK).
|
||||
|
||||
if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
|
||||
if Spec_Id /= Body_Id and then not Aspects_On_Body_Or_Stub_OK (N) then
|
||||
Diagnose_Misplaced_Aspects (Spec_Id);
|
||||
else
|
||||
Analyze_Aspect_Specifications (N, Body_Id);
|
||||
|
|
|
|||
|
|
@ -2505,16 +2505,23 @@ package body Sem_Ch3 is
|
|||
Analyze_Object_Contract (Defining_Entity (Decl));
|
||||
|
||||
elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
|
||||
N_Entry_Declaration,
|
||||
N_Generic_Subprogram_Declaration,
|
||||
N_Subprogram_Declaration)
|
||||
then
|
||||
Analyze_Subprogram_Contract (Defining_Entity (Decl));
|
||||
Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
|
||||
|
||||
elsif Nkind (Decl) = N_Subprogram_Body then
|
||||
Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
|
||||
elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract
|
||||
(Defining_Entity (Decl));
|
||||
|
||||
elsif Nkind (Decl) = N_Subprogram_Body_Stub then
|
||||
Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
|
||||
|
||||
elsif Nkind_In (Decl, N_Single_Task_Declaration,
|
||||
N_Task_Type_Declaration)
|
||||
then
|
||||
Analyze_Task_Contract (Defining_Entity (Decl));
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
|
|
|
|||
|
|
@ -1385,7 +1385,7 @@ package body Sem_Ch6 is
|
|||
-- have been analyzed. This ensures that any contract-related pragmas
|
||||
-- are available through the N_Contract node of the body.
|
||||
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
|
||||
|
||||
Analyze (Handled_Statement_Sequence (N));
|
||||
Save_Global_References (Original_Node (N));
|
||||
|
|
@ -3789,7 +3789,7 @@ package body Sem_Ch6 is
|
|||
-- after the declarations of the body have been processed as pragmas
|
||||
-- are now chained on the contract of the subprogram body.
|
||||
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
|
||||
|
||||
-- If SPARK_Mode for body is not On, disable frontend inlining for this
|
||||
-- subprogram in GNATprove mode, as its body should not be analyzed.
|
||||
|
|
|
|||
|
|
@ -1213,8 +1213,8 @@ package body Sem_Ch9 is
|
|||
Set_Ekind (Id, E_Entry);
|
||||
end if;
|
||||
|
||||
Set_Scope (Id, Current_Scope);
|
||||
Set_Etype (Id, Standard_Void_Type);
|
||||
Set_Scope (Id, Current_Scope);
|
||||
Set_Accept_Address (Id, New_Elmt_List);
|
||||
|
||||
-- Set the SPARK_Mode from the current context (may be overwritten later
|
||||
|
|
@ -1223,6 +1223,12 @@ package body Sem_Ch9 is
|
|||
Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
|
||||
Set_SPARK_Pragma_Inherited (Id);
|
||||
|
||||
-- Analyze any aspect specifications that appear on the entry body
|
||||
|
||||
if Has_Aspects (N) then
|
||||
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
|
||||
end if;
|
||||
|
||||
E := First_Entity (P_Type);
|
||||
while Present (E) loop
|
||||
if Chars (E) = Chars (Id)
|
||||
|
|
@ -1352,6 +1358,12 @@ package body Sem_Ch9 is
|
|||
Inspect_Deferred_Constant_Completion (Decls);
|
||||
end if;
|
||||
|
||||
-- Process the contract of the subprogram body after all declarations
|
||||
-- have been analyzed. This ensures that any contract-related pragmas
|
||||
-- are available through the N_Contract node of the body.
|
||||
|
||||
Analyze_Entry_Or_Subprogram_Body_Contract (Id);
|
||||
|
||||
if Present (Stats) then
|
||||
Analyze (Stats);
|
||||
end if;
|
||||
|
|
|
|||
|
|
@ -209,6 +209,12 @@ package body Sem_Prag is
|
|||
-- Do_Checks is set, the routine reports duplicate pragmas. The routine
|
||||
-- returns Empty when reaching the start of the node chain.
|
||||
|
||||
function Fix_Msg (Id : Entity_Id; Msg : String) return String;
|
||||
-- Replace all occurrences of "subprogram" in string Msg with a specific
|
||||
-- word depending on the Ekind of Id as follows:
|
||||
-- * When Id is an entry [family], replace with "entry"
|
||||
-- * When Id is a task type, replace with "task unit"
|
||||
|
||||
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
|
||||
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
|
||||
-- original one, following the renaming chain) is returned. Otherwise the
|
||||
|
|
@ -386,7 +392,7 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
|
||||
|
||||
|
|
@ -465,7 +471,7 @@ package body Sem_Prag is
|
|||
|
||||
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
|
||||
Loc : constant Source_Ptr := Sloc (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
|
||||
All_Inputs_Seen : Elist_Id := No_Elist;
|
||||
|
|
@ -1144,8 +1150,8 @@ package body Sem_Prag is
|
|||
|
||||
Error_Msg_Name_1 := Chars (Spec_Id);
|
||||
SPARK_Msg_NE
|
||||
("\& is not part of the input or output set of subprogram %",
|
||||
Item, Item_Id);
|
||||
(Fix_Msg (Spec_Id, "\& is not part of the input or output "
|
||||
& "set of subprogram %"), Item, Item_Id);
|
||||
|
||||
-- The mode of the item and its role in pragma [Refined_]Depends
|
||||
-- are in conflict. Construct a detailed message explaining the
|
||||
|
|
@ -1638,7 +1644,9 @@ package body Sem_Prag is
|
|||
Restore_Scope := True;
|
||||
Push_Scope (Spec_Id);
|
||||
|
||||
if Is_Generic_Subprogram (Spec_Id) then
|
||||
if Ekind (Spec_Id) = E_Task_Type then
|
||||
null;
|
||||
elsif Is_Generic_Subprogram (Spec_Id) then
|
||||
Install_Generic_Formals (Spec_Id);
|
||||
else
|
||||
Install_Formals (Spec_Id);
|
||||
|
|
@ -1772,7 +1780,7 @@ package body Sem_Prag is
|
|||
---------------------------------
|
||||
|
||||
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
|
||||
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl);
|
||||
|
||||
|
|
@ -1876,8 +1884,8 @@ package body Sem_Prag is
|
|||
if Is_Formal (Item_Id) then
|
||||
if Scope (Item_Id) = Spec_Id then
|
||||
SPARK_Msg_NE
|
||||
("global item cannot reference parameter of "
|
||||
& "subprogram &", Item, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "global item cannot reference "
|
||||
& "parameter of subprogram &"), Item, Spec_Id);
|
||||
return;
|
||||
end if;
|
||||
|
||||
|
|
@ -2096,9 +2104,10 @@ package body Sem_Prag is
|
|||
SPARK_Msg_NE
|
||||
("global item & cannot have mode In_Out or Output",
|
||||
Item, Item_Id);
|
||||
|
||||
SPARK_Msg_NE
|
||||
("\item already appears as input of subprogram &",
|
||||
Item, Context);
|
||||
(Fix_Msg (Subp_Id, "\item already appears as input of "
|
||||
& "subprogram &"), Item, Context);
|
||||
|
||||
-- Stop the traversal once an error has been detected
|
||||
|
||||
|
|
@ -2257,7 +2266,9 @@ package body Sem_Prag is
|
|||
Restore_Scope := True;
|
||||
Push_Scope (Spec_Id);
|
||||
|
||||
if Is_Generic_Subprogram (Spec_Id) then
|
||||
if Ekind (Spec_Id) = E_Task_Type then
|
||||
null;
|
||||
elsif Is_Generic_Subprogram (Spec_Id) then
|
||||
Install_Generic_Formals (Spec_Id);
|
||||
else
|
||||
Install_Formals (Spec_Id);
|
||||
|
|
@ -3351,21 +3362,26 @@ package body Sem_Prag is
|
|||
-- associated with a subprogram declaration or a body that acts as a
|
||||
-- spec.
|
||||
|
||||
Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
|
||||
Subp_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
|
||||
|
||||
-- Entry
|
||||
|
||||
if Nkind (Subp_Decl) = N_Entry_Declaration then
|
||||
null;
|
||||
|
||||
-- Generic subprogram
|
||||
|
||||
if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
|
||||
elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
|
||||
null;
|
||||
|
||||
-- Body acts as spec
|
||||
-- Subprogram body acts as spec
|
||||
|
||||
elsif Nkind (Subp_Decl) = N_Subprogram_Body
|
||||
and then No (Corresponding_Spec (Subp_Decl))
|
||||
then
|
||||
null;
|
||||
|
||||
-- Body stub acts as spec
|
||||
-- Subprogram body stub acts as spec
|
||||
|
||||
elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
|
||||
and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
|
||||
|
|
@ -3377,6 +3393,11 @@ package body Sem_Prag is
|
|||
elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
|
||||
null;
|
||||
|
||||
-- Task unit
|
||||
|
||||
elsif Nkind (Subp_Decl) = N_Task_Type_Declaration then
|
||||
null;
|
||||
|
||||
else
|
||||
Pragma_Misplaced;
|
||||
return;
|
||||
|
|
@ -3387,6 +3408,16 @@ package body Sem_Prag is
|
|||
Legal := True;
|
||||
Spec_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
|
||||
-- When the related context is an entry, it must be a protected entry
|
||||
-- (SPARK RM 6.1.4(6)).
|
||||
|
||||
if Is_Entry_Declaration (Spec_Id)
|
||||
and then Ekind (Scope (Spec_Id)) /= E_Protected_Type
|
||||
then
|
||||
Pragma_Misplaced;
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- A pragma that applies to a Ghost entity becomes Ghost for the
|
||||
-- purposes of legality checks and removal of ignored Ghost code.
|
||||
|
||||
|
|
@ -3686,7 +3717,8 @@ package body Sem_Prag is
|
|||
-- Ensure the proper placement of the pragma
|
||||
|
||||
Subp_Decl :=
|
||||
Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK);
|
||||
Find_Related_Declaration_Or_Body
|
||||
(N, Do_Checks => not Duplicates_OK);
|
||||
|
||||
-- When a pre/postcondition pragma applies to an abstract subprogram,
|
||||
-- its original form must be an aspect with 'Class.
|
||||
|
|
@ -3759,10 +3791,11 @@ package body Sem_Prag is
|
|||
|
||||
Mark_Pragma_As_Ghost (N, Subp_Id);
|
||||
|
||||
-- Fully analyze the pragma when it appears inside a subprogram
|
||||
-- body because it cannot benefit from forward references.
|
||||
-- Fully analyze the pragma when it appears inside an entry or
|
||||
-- subprogram body because it cannot benefit from forward references.
|
||||
|
||||
if Nkind_In (Subp_Decl, N_Subprogram_Body,
|
||||
if Nkind_In (Subp_Decl, N_Entry_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
then
|
||||
-- The legality checks of pragmas Precondition and Postcondition
|
||||
|
|
@ -3801,23 +3834,36 @@ package body Sem_Prag is
|
|||
-- Verify the placement of the pragma and check for duplicates. The
|
||||
-- pragma must apply to a subprogram body [stub].
|
||||
|
||||
Body_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
|
||||
Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
|
||||
|
||||
-- Extract the entities of the spec and body
|
||||
-- Entry body
|
||||
|
||||
if Nkind (Body_Decl) = N_Subprogram_Body then
|
||||
Body_Id := Defining_Entity (Body_Decl);
|
||||
Spec_Id := Corresponding_Spec (Body_Decl);
|
||||
if Nkind (Body_Decl) = N_Entry_Body then
|
||||
null;
|
||||
|
||||
-- Subprogram body
|
||||
|
||||
elsif Nkind (Body_Decl) = N_Subprogram_Body then
|
||||
null;
|
||||
|
||||
-- Subprogram body stub
|
||||
|
||||
elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then
|
||||
Body_Id := Defining_Entity (Body_Decl);
|
||||
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
|
||||
null;
|
||||
|
||||
-- Task body
|
||||
|
||||
elsif Nkind (Body_Decl) = N_Task_Body then
|
||||
null;
|
||||
|
||||
else
|
||||
Pragma_Misplaced;
|
||||
return;
|
||||
end if;
|
||||
|
||||
Body_Id := Defining_Entity (Body_Decl);
|
||||
Spec_Id := Unique_Defining_Entity (Body_Decl);
|
||||
|
||||
-- The pragma must apply to the second declaration of a subprogram.
|
||||
-- In other words, the body [stub] cannot acts as a spec.
|
||||
|
||||
|
|
@ -3839,10 +3885,17 @@ package body Sem_Prag is
|
|||
|
||||
Spec_Decl := Unit_Declaration_Node (Spec_Id);
|
||||
|
||||
-- The proper context of a entry declaration is the declaration of
|
||||
-- the enclosing synchronized type.
|
||||
|
||||
if Nkind (Spec_Decl) = N_Entry_Declaration then
|
||||
Spec_Decl := Parent (Parent (Spec_Decl));
|
||||
end if;
|
||||
|
||||
if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then
|
||||
Error_Pragma
|
||||
("pragma % must apply to the body of a subprogram declared in a "
|
||||
& "package specification");
|
||||
(Fix_Msg (Spec_Id, "pragma % must apply to the body of "
|
||||
& "subprogram declared in a package specification"));
|
||||
return;
|
||||
end if;
|
||||
|
||||
|
|
@ -12275,7 +12328,7 @@ package body Sem_Prag is
|
|||
-- as a spec.
|
||||
|
||||
Subp_Decl :=
|
||||
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
|
||||
Find_Related_Declaration_Or_Body (N, Do_Checks => True);
|
||||
|
||||
-- Generic subprogram
|
||||
|
||||
|
|
@ -12319,10 +12372,12 @@ package body Sem_Prag is
|
|||
Mark_Pragma_As_Ghost (N, Spec_Id);
|
||||
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
|
||||
|
||||
-- Fully analyze the pragma when it appears inside a subprogram
|
||||
-- body because it cannot benefit from forward references.
|
||||
-- Fully analyze the pragma when it appears inside an entry
|
||||
-- or subprogram body because it cannot benefit from forward
|
||||
-- references.
|
||||
|
||||
if Nkind_In (Subp_Decl, N_Subprogram_Body,
|
||||
if Nkind_In (Subp_Decl, N_Entry_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
then
|
||||
-- The legality checks of pragma Contract_Cases are affected by
|
||||
|
|
@ -13046,10 +13101,12 @@ package body Sem_Prag is
|
|||
|
||||
Add_Contract_Item (N, Spec_Id);
|
||||
|
||||
-- Fully analyze the pragma when it appears inside a subprogram
|
||||
-- body because it cannot benefit from forward references.
|
||||
-- Fully analyze the pragma when it appears inside an entry
|
||||
-- or subprogram body because it cannot benefit from forward
|
||||
-- references.
|
||||
|
||||
if Nkind_In (Subp_Decl, N_Subprogram_Body,
|
||||
if Nkind_In (Subp_Decl, N_Entry_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
then
|
||||
-- The legality checks of pragmas Depends and Global are
|
||||
|
|
@ -13993,7 +14050,7 @@ package body Sem_Prag is
|
|||
Check_At_Most_N_Arguments (1);
|
||||
|
||||
Subp_Decl :=
|
||||
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
|
||||
Find_Related_Declaration_Or_Body (N, Do_Checks => True);
|
||||
|
||||
-- Generic subprogram declaration
|
||||
|
||||
|
|
@ -14564,10 +14621,12 @@ package body Sem_Prag is
|
|||
|
||||
Add_Contract_Item (N, Spec_Id);
|
||||
|
||||
-- Fully analyze the pragma when it appears inside a subprogram
|
||||
-- body because it cannot benefit from forward references.
|
||||
-- Fully analyze the pragma when it appears inside an entry
|
||||
-- or subprogram body because it cannot benefit from forward
|
||||
-- references.
|
||||
|
||||
if Nkind_In (Subp_Decl, N_Subprogram_Body,
|
||||
if Nkind_In (Subp_Decl, N_Entry_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
then
|
||||
-- The legality checks of pragmas Depends and Global are
|
||||
|
|
@ -20991,7 +21050,7 @@ package body Sem_Prag is
|
|||
return;
|
||||
end if;
|
||||
|
||||
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl := Find_Related_Declaration_Or_Body (N);
|
||||
|
||||
-- Find the enclosing context
|
||||
|
||||
|
|
@ -21067,10 +21126,12 @@ package body Sem_Prag is
|
|||
|
||||
Check_Distinct_Name (Subp_Id);
|
||||
|
||||
-- Fully analyze the pragma when it appears inside a subprogram
|
||||
-- body because it cannot benefit from forward references.
|
||||
-- Fully analyze the pragma when it appears inside an entry
|
||||
-- or subprogram body because it cannot benefit from forward
|
||||
-- references.
|
||||
|
||||
if Nkind_In (Subp_Decl, N_Subprogram_Body,
|
||||
if Nkind_In (Subp_Decl, N_Entry_Body,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
then
|
||||
-- The legality checks of pragma Test_Case are affected by the
|
||||
|
|
@ -21910,7 +21971,7 @@ package body Sem_Prag is
|
|||
Check_At_Most_N_Arguments (1);
|
||||
|
||||
Subp_Decl :=
|
||||
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
|
||||
Find_Related_Declaration_Or_Body (N, Do_Checks => True);
|
||||
|
||||
-- Generic subprogram
|
||||
|
||||
|
|
@ -22575,7 +22636,7 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
|
||||
|
||||
|
|
@ -22773,9 +22834,9 @@ package body Sem_Prag is
|
|||
|
||||
Item_Id := Available_View (Entity_Of (Item));
|
||||
|
||||
return Ekind (Item_Id) = E_Abstract_State
|
||||
return
|
||||
Ekind (Item_Id) = E_Abstract_State
|
||||
and then Has_Null_Refinement (Item_Id);
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
|
|
@ -23059,8 +23120,8 @@ package body Sem_Prag is
|
|||
|
||||
if not Clause_Matched then
|
||||
SPARK_Msg_NE
|
||||
("dependence clause of subprogram & has no matching refinement "
|
||||
& "in body", Dep_Clause, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "dependence clause of subprogram & has no "
|
||||
& "matching refinement in body"), Dep_Clause, Spec_Id);
|
||||
end if;
|
||||
end Check_Dependency_Clause;
|
||||
|
||||
|
|
@ -23377,7 +23438,7 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
|
||||
Errors : constant Nat := Serious_Errors_Detected;
|
||||
Clause : Node_Id;
|
||||
|
|
@ -23394,12 +23455,7 @@ package body Sem_Prag is
|
|||
return;
|
||||
end if;
|
||||
|
||||
if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
|
||||
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
|
||||
else
|
||||
Spec_Id := Corresponding_Spec (Body_Decl);
|
||||
end if;
|
||||
|
||||
Spec_Id := Unique_Defining_Entity (Body_Decl);
|
||||
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
|
||||
|
||||
-- Subprogram declarations lacks pragma Depends. Refined_Depends is
|
||||
|
|
@ -23407,8 +23463,8 @@ package body Sem_Prag is
|
|||
|
||||
if No (Depends) then
|
||||
SPARK_Msg_NE
|
||||
("useless refinement, declaration of subprogram & lacks aspect or "
|
||||
& "pragma Depends", N, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram "
|
||||
& "& lacks aspect or pragma Depends"), N, Spec_Id);
|
||||
goto Leave;
|
||||
end if;
|
||||
|
||||
|
|
@ -23421,8 +23477,8 @@ package body Sem_Prag is
|
|||
|
||||
if Nkind (Deps) = N_Null then
|
||||
SPARK_Msg_NE
|
||||
("useless refinement, subprogram & does not depend on abstract "
|
||||
& "state with visible refinement", N, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "useless refinement, subprogram & does not "
|
||||
& "depend on abstract state with visible refinement"), N, Spec_Id);
|
||||
goto Leave;
|
||||
end if;
|
||||
|
||||
|
|
@ -24355,7 +24411,7 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Errors : constant Nat := Serious_Errors_Detected;
|
||||
Items : Node_Id;
|
||||
|
||||
|
|
@ -24368,12 +24424,7 @@ package body Sem_Prag is
|
|||
return;
|
||||
end if;
|
||||
|
||||
if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
|
||||
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
|
||||
else
|
||||
Spec_Id := Corresponding_Spec (Body_Decl);
|
||||
end if;
|
||||
|
||||
Spec_Id := Unique_Defining_Entity (Body_Decl);
|
||||
Global := Get_Pragma (Spec_Id, Pragma_Global);
|
||||
Items := Expression (Get_Argument (N, Spec_Id));
|
||||
|
||||
|
|
@ -24382,8 +24433,8 @@ package body Sem_Prag is
|
|||
|
||||
if No (Global) then
|
||||
SPARK_Msg_NE
|
||||
("useless refinement, declaration of subprogram & lacks aspect or "
|
||||
& "pragma Global", N, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram "
|
||||
& "& lacks aspect or pragma Global"), N, Spec_Id);
|
||||
goto Leave;
|
||||
end if;
|
||||
|
||||
|
|
@ -24415,8 +24466,9 @@ package body Sem_Prag is
|
|||
and then not Has_Null_State
|
||||
then
|
||||
SPARK_Msg_NE
|
||||
("useless refinement, subprogram & does not depend on abstract "
|
||||
& "state with visible refinement", N, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "useless refinement, subprogram & does not "
|
||||
& "depend on abstract state with visible refinement"),
|
||||
N, Spec_Id);
|
||||
goto Leave;
|
||||
|
||||
-- The global refinement of inputs and outputs cannot be null when
|
||||
|
|
@ -24432,8 +24484,8 @@ package body Sem_Prag is
|
|||
and then not Has_Null_State
|
||||
then
|
||||
SPARK_Msg_NE
|
||||
("refinement cannot be null, subprogram & has global items",
|
||||
N, Spec_Id);
|
||||
(Fix_Msg (Spec_Id, "refinement cannot be null, subprogram & has "
|
||||
& "global items"), N, Spec_Id);
|
||||
goto Leave;
|
||||
end if;
|
||||
end if;
|
||||
|
|
@ -25292,7 +25344,7 @@ package body Sem_Prag is
|
|||
------------------------------------
|
||||
|
||||
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
|
||||
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
|
||||
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
|
||||
|
||||
procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id);
|
||||
|
|
@ -26326,10 +26378,13 @@ package body Sem_Prag is
|
|||
Next_Entity (Formal);
|
||||
end loop;
|
||||
|
||||
-- When processing a subprogram body, look for pragmas Refined_Depends
|
||||
-- and Refined_Global as they specify the inputs and outputs.
|
||||
-- When processing an entry, subprogram or task body, look for pragmas
|
||||
-- Refined_Depends and Refined_Global as they specify the inputs and
|
||||
-- outputs.
|
||||
|
||||
if Ekind (Subp_Id) = E_Subprogram_Body then
|
||||
if Is_Entry_Body (Subp_Id)
|
||||
or else Ekind_In (Subp_Id, E_Subprogram_Body, E_Task_Body)
|
||||
then
|
||||
Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends);
|
||||
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
|
||||
|
||||
|
|
@ -26469,6 +26524,172 @@ package body Sem_Prag is
|
|||
return Empty;
|
||||
end Find_Related_Context;
|
||||
|
||||
--------------------------------------
|
||||
-- Find_Related_Declaration_Or_Body --
|
||||
--------------------------------------
|
||||
|
||||
function Find_Related_Declaration_Or_Body
|
||||
(Prag : Node_Id;
|
||||
Do_Checks : Boolean := False) return Node_Id
|
||||
is
|
||||
Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
|
||||
|
||||
procedure Expression_Function_Error;
|
||||
-- Emit an error concerning pragma Prag that illegaly applies to an
|
||||
-- expression function.
|
||||
|
||||
-------------------------------
|
||||
-- Expression_Function_Error --
|
||||
-------------------------------
|
||||
|
||||
procedure Expression_Function_Error is
|
||||
begin
|
||||
Error_Msg_Name_1 := Prag_Nam;
|
||||
|
||||
-- Emit a precise message to distinguish between source pragmas and
|
||||
-- pragmas generated from aspects.
|
||||
|
||||
if From_Aspect_Specification (Prag) then
|
||||
Error_Msg_N
|
||||
("aspect % cannot apply to a stand alone expression function",
|
||||
Prag);
|
||||
else
|
||||
Error_Msg_N
|
||||
("pragma % cannot apply to a stand alone expression function",
|
||||
Prag);
|
||||
end if;
|
||||
end Expression_Function_Error;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Context : constant Node_Id := Parent (Prag);
|
||||
Stmt : Node_Id;
|
||||
|
||||
Look_For_Body : constant Boolean :=
|
||||
Nam_In (Prag_Nam, Name_Refined_Depends,
|
||||
Name_Refined_Global,
|
||||
Name_Refined_Post);
|
||||
-- Refinement pragmas must be associated with a subprogram body [stub]
|
||||
|
||||
-- Start of processing for Find_Related_Declaration_Or_Body
|
||||
|
||||
begin
|
||||
Stmt := Prev (Prag);
|
||||
while Present (Stmt) loop
|
||||
|
||||
-- Skip prior pragmas, but check for duplicates. Pragmas produced
|
||||
-- by splitting a complex pre/postcondition are not considered to
|
||||
-- be duplicates.
|
||||
|
||||
if Nkind (Stmt) = N_Pragma then
|
||||
if Do_Checks
|
||||
and then not Split_PPC (Stmt)
|
||||
and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam
|
||||
then
|
||||
Duplication_Error
|
||||
(Prag => Prag,
|
||||
Prev => Stmt);
|
||||
end if;
|
||||
|
||||
-- Emit an error when a refinement pragma appears on an expression
|
||||
-- function without a completion.
|
||||
|
||||
elsif Do_Checks
|
||||
and then Look_For_Body
|
||||
and then Nkind (Stmt) = N_Subprogram_Declaration
|
||||
and then Nkind (Original_Node (Stmt)) = N_Expression_Function
|
||||
and then not Has_Completion (Defining_Entity (Stmt))
|
||||
then
|
||||
Expression_Function_Error;
|
||||
return Empty;
|
||||
|
||||
-- The refinement pragma applies to a subprogram body stub
|
||||
|
||||
elsif Look_For_Body
|
||||
and then Nkind (Stmt) = N_Subprogram_Body_Stub
|
||||
then
|
||||
return Stmt;
|
||||
|
||||
-- Skip internally generated code
|
||||
|
||||
elsif not Comes_From_Source (Stmt) then
|
||||
if Nkind (Stmt) = N_Subprogram_Declaration then
|
||||
|
||||
-- The subprogram declaration is an internally generated spec
|
||||
-- for an expression function.
|
||||
|
||||
if Nkind (Original_Node (Stmt)) = N_Expression_Function then
|
||||
return Stmt;
|
||||
|
||||
-- The subprogram is actually an instance housed within an
|
||||
-- anonymous wrapper package.
|
||||
|
||||
elsif Present (Generic_Parent (Specification (Stmt))) then
|
||||
return Stmt;
|
||||
end if;
|
||||
|
||||
-- The pragma applies to a single task declaration rewritten as a
|
||||
-- task type.
|
||||
|
||||
elsif Nkind (Stmt) = N_Task_Type_Declaration
|
||||
and then Nkind (Original_Node (Stmt)) = N_Single_Task_Declaration
|
||||
then
|
||||
return Stmt;
|
||||
end if;
|
||||
|
||||
-- Return the current construct which is either a subprogram body,
|
||||
-- a subprogram declaration or is illegal.
|
||||
|
||||
else
|
||||
return Stmt;
|
||||
end if;
|
||||
|
||||
Prev (Stmt);
|
||||
end loop;
|
||||
|
||||
-- If we fall through, then the pragma was either the first declaration
|
||||
-- or it was preceded by other pragmas and no source constructs.
|
||||
|
||||
-- The pragma is associated with a library-level subprogram
|
||||
|
||||
if Nkind (Context) = N_Compilation_Unit_Aux then
|
||||
return Unit (Parent (Context));
|
||||
|
||||
-- The pragma appears inside the declarations of an entry body
|
||||
|
||||
elsif Nkind (Context) = N_Entry_Body then
|
||||
return Context;
|
||||
|
||||
-- The pragma appears inside the statements of a subprogram body. This
|
||||
-- placement is the result of subprogram contract expansion.
|
||||
|
||||
elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
|
||||
return Parent (Context);
|
||||
|
||||
-- The pragma appears inside the declarative part of a subprogram body
|
||||
|
||||
elsif Nkind (Context) = N_Subprogram_Body then
|
||||
return Context;
|
||||
|
||||
-- The pragma appears inside the declarative part of a task body
|
||||
|
||||
elsif Nkind (Context) = N_Task_Body then
|
||||
return Context;
|
||||
|
||||
-- The pragma is a byproduct of aspect expansion, return the related
|
||||
-- context of the original aspect. This case has a lower priority as
|
||||
-- the above circuitry pinpoints precisely the related context.
|
||||
|
||||
elsif Present (Corresponding_Aspect (Prag)) then
|
||||
return Parent (Corresponding_Aspect (Prag));
|
||||
|
||||
-- No candidate subprogram [body] found
|
||||
|
||||
else
|
||||
return Empty;
|
||||
end if;
|
||||
end Find_Related_Declaration_Or_Body;
|
||||
|
||||
----------------------------------
|
||||
-- Find_Related_Package_Or_Body --
|
||||
----------------------------------
|
||||
|
|
@ -26557,153 +26778,55 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Find_Related_Package_Or_Body;
|
||||
|
||||
-------------------------------------
|
||||
-- Find_Related_Subprogram_Or_Body --
|
||||
-------------------------------------
|
||||
-------------
|
||||
-- Fix_Msg --
|
||||
-------------
|
||||
|
||||
function Find_Related_Subprogram_Or_Body
|
||||
(Prag : Node_Id;
|
||||
Do_Checks : Boolean := False) return Node_Id
|
||||
is
|
||||
Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
|
||||
|
||||
procedure Expression_Function_Error;
|
||||
-- Emit an error concerning pragma Prag that illegaly applies to an
|
||||
-- expression function.
|
||||
|
||||
-------------------------------
|
||||
-- Expression_Function_Error --
|
||||
-------------------------------
|
||||
|
||||
procedure Expression_Function_Error is
|
||||
begin
|
||||
Error_Msg_Name_1 := Prag_Nam;
|
||||
|
||||
-- Emit a precise message to distinguish between source pragmas and
|
||||
-- pragmas generated from aspects.
|
||||
|
||||
if From_Aspect_Specification (Prag) then
|
||||
Error_Msg_N
|
||||
("aspect % cannot apply to a stand alone expression function",
|
||||
Prag);
|
||||
else
|
||||
Error_Msg_N
|
||||
("pragma % cannot apply to a stand alone expression function",
|
||||
Prag);
|
||||
end if;
|
||||
end Expression_Function_Error;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Context : constant Node_Id := Parent (Prag);
|
||||
Stmt : Node_Id;
|
||||
|
||||
Look_For_Body : constant Boolean :=
|
||||
Nam_In (Prag_Nam, Name_Refined_Depends,
|
||||
Name_Refined_Global,
|
||||
Name_Refined_Post);
|
||||
-- Refinement pragmas must be associated with a subprogram body [stub]
|
||||
|
||||
-- Start of processing for Find_Related_Subprogram_Or_Body
|
||||
function Fix_Msg (Id : Entity_Id; Msg : String) return String is
|
||||
Msg_Last : constant Natural := Msg'Last;
|
||||
Msg_Index : Natural;
|
||||
Res : String (Msg'Range) := (others => ' ');
|
||||
Res_Index : Natural;
|
||||
|
||||
begin
|
||||
Stmt := Prev (Prag);
|
||||
while Present (Stmt) loop
|
||||
-- Copy all characters from the input message Msg to result Res with
|
||||
-- suitable replacements.
|
||||
|
||||
-- Skip prior pragmas, but check for duplicates. Pragmas produced
|
||||
-- by splitting a complex pre/postcondition are not considered to
|
||||
-- be duplicates.
|
||||
Msg_Index := Msg'First;
|
||||
Res_Index := Res'First;
|
||||
while Msg_Index <= Msg_Last loop
|
||||
|
||||
if Nkind (Stmt) = N_Pragma then
|
||||
if Do_Checks
|
||||
and then not Split_PPC (Stmt)
|
||||
and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam
|
||||
-- Replace "subprogram" with a different word
|
||||
|
||||
if Msg_Index <= Msg_Last - 10
|
||||
and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram"
|
||||
then
|
||||
Duplication_Error
|
||||
(Prag => Prag,
|
||||
Prev => Stmt);
|
||||
end if;
|
||||
if Ekind_In (Id, E_Entry, E_Entry_Family) then
|
||||
Res (Res_Index .. Res_Index + 4) := "entry";
|
||||
Res_Index := Res_Index + 5;
|
||||
|
||||
-- Emit an error when a refinement pragma appears on an expression
|
||||
-- function without a completion.
|
||||
|
||||
elsif Do_Checks
|
||||
and then Look_For_Body
|
||||
and then Nkind (Stmt) = N_Subprogram_Declaration
|
||||
and then Nkind (Original_Node (Stmt)) = N_Expression_Function
|
||||
and then not Has_Completion (Defining_Entity (Stmt))
|
||||
then
|
||||
Expression_Function_Error;
|
||||
return Empty;
|
||||
|
||||
-- The refinement pragma applies to a subprogram body stub
|
||||
|
||||
elsif Look_For_Body
|
||||
and then Nkind (Stmt) = N_Subprogram_Body_Stub
|
||||
then
|
||||
return Stmt;
|
||||
|
||||
-- Skip internally generated code
|
||||
|
||||
elsif not Comes_From_Source (Stmt) then
|
||||
if Nkind (Stmt) = N_Subprogram_Declaration then
|
||||
|
||||
-- The subprogram declaration is an internally generated spec
|
||||
-- for an expression function.
|
||||
|
||||
if Nkind (Original_Node (Stmt)) = N_Expression_Function then
|
||||
return Stmt;
|
||||
|
||||
-- The subprogram is actually an instance housed within an
|
||||
-- anonymous wrapper package.
|
||||
|
||||
elsif Present (Generic_Parent (Specification (Stmt))) then
|
||||
return Stmt;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Return the current construct which is either a subprogram body,
|
||||
-- a subprogram declaration or is illegal.
|
||||
elsif Ekind_In (Id, E_Task_Body, E_Task_Type) then
|
||||
Res (Res_Index .. Res_Index + 8) := "task unit";
|
||||
Res_Index := Res_Index + 9;
|
||||
|
||||
else
|
||||
return Stmt;
|
||||
Res (Res_Index .. Res_Index + 9) := "subprogram";
|
||||
Res_Index := Res_Index + 10;
|
||||
end if;
|
||||
|
||||
Prev (Stmt);
|
||||
Msg_Index := Msg_Index + 10;
|
||||
|
||||
-- Otherwise copy the character
|
||||
|
||||
else
|
||||
Res (Res_Index) := Msg (Msg_Index);
|
||||
Msg_Index := Msg_Index + 1;
|
||||
Res_Index := Res_Index + 1;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
-- If we fall through, then the pragma was either the first declaration
|
||||
-- or it was preceded by other pragmas and no source constructs.
|
||||
|
||||
-- The pragma is associated with a library-level subprogram
|
||||
|
||||
if Nkind (Context) = N_Compilation_Unit_Aux then
|
||||
return Unit (Parent (Context));
|
||||
|
||||
-- The pragma appears inside the statements of a subprogram body. This
|
||||
-- placement is the result of subprogram contract expansion.
|
||||
|
||||
elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
|
||||
return Parent (Context);
|
||||
|
||||
-- The pragma appears inside the declarative part of a subprogram body
|
||||
|
||||
elsif Nkind (Context) = N_Subprogram_Body then
|
||||
return Context;
|
||||
|
||||
-- The pragma is a byproduct of aspect expansion, return the related
|
||||
-- context of the original aspect. This case has a lower priority as
|
||||
-- the above circuitry pinpoints precisely the related context.
|
||||
|
||||
elsif Present (Corresponding_Aspect (Prag)) then
|
||||
return Parent (Corresponding_Aspect (Prag));
|
||||
|
||||
-- No candidate subprogram [body] found
|
||||
|
||||
else
|
||||
return Empty;
|
||||
end if;
|
||||
end Find_Related_Subprogram_Or_Body;
|
||||
return Res (Res'First .. Res_Index - 1);
|
||||
end Fix_Msg;
|
||||
|
||||
------------------
|
||||
-- Get_Argument --
|
||||
|
|
|
|||
|
|
@ -327,22 +327,29 @@ package Sem_Prag is
|
|||
-- the pragma is illegal. If flag Do_Checks is set, the routine reports
|
||||
-- duplicate pragmas.
|
||||
|
||||
function Find_Related_Subprogram_Or_Body
|
||||
function Find_Related_Declaration_Or_Body
|
||||
(Prag : Node_Id;
|
||||
Do_Checks : Boolean := False) return Node_Id;
|
||||
-- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
|
||||
-- Refined_Depends, Refined_Global and Refined_Post and attribute 'Result.
|
||||
-- Find the declaration of the related subprogram [body or stub] subject
|
||||
-- to pragma Prag. If flag Do_Checks is set, the routine reports duplicate
|
||||
-- pragmas and detects improper use of refinement pragmas in stand alone
|
||||
-- expression functions. The returned value depends on the related pragma
|
||||
-- as follows:
|
||||
-- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding
|
||||
-- N_Subprogram_Declaration node or if the pragma applies to a stand
|
||||
-- alone body, the N_Subprogram_Body node or Empty if illegal.
|
||||
-- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
|
||||
-- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
|
||||
-- illegal.
|
||||
-- Subsidiary to the analysis of pragmas
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Extensions_Visible
|
||||
-- Global
|
||||
-- Post
|
||||
-- Post_Class
|
||||
-- Postcondition
|
||||
-- Pre
|
||||
-- Pre_Class
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case
|
||||
-- as well as attributes 'Old and 'Result. Find the declaration of the
|
||||
-- related entry, subprogram or task type [body] subject to pragma Prag.
|
||||
-- If flag Do_Checks is set, the routine reports duplicate pragmas and
|
||||
-- detects improper use of refinement pragmas in stand alone expression
|
||||
-- functions.
|
||||
|
||||
function Get_Argument
|
||||
(Prag : Node_Id;
|
||||
|
|
|
|||
|
|
@ -11444,6 +11444,28 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Is_Effectively_Volatile_Object;
|
||||
|
||||
-------------------
|
||||
-- Is_Entry_Body --
|
||||
-------------------
|
||||
|
||||
function Is_Entry_Body (Id : Entity_Id) return Boolean is
|
||||
begin
|
||||
return
|
||||
Ekind_In (Id, E_Entry, E_Entry_Family)
|
||||
and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Body;
|
||||
end Is_Entry_Body;
|
||||
|
||||
--------------------------
|
||||
-- Is_Entry_Declaration --
|
||||
--------------------------
|
||||
|
||||
function Is_Entry_Declaration (Id : Entity_Id) return Boolean is
|
||||
begin
|
||||
return
|
||||
Ekind_In (Id, E_Entry, E_Entry_Family)
|
||||
and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Declaration;
|
||||
end Is_Entry_Declaration;
|
||||
|
||||
----------------------------
|
||||
-- Is_Expression_Function --
|
||||
----------------------------
|
||||
|
|
|
|||
|
|
@ -1283,6 +1283,12 @@ package Sem_Util is
|
|||
-- Determine whether an arbitrary node denotes an effectively volatile
|
||||
-- object (SPARK RM 7.1.2).
|
||||
|
||||
function Is_Entry_Body (Id : Entity_Id) return Boolean;
|
||||
-- Determine whether entity Id is the body entity of an entry [family]
|
||||
|
||||
function Is_Entry_Declaration (Id : Entity_Id) return Boolean;
|
||||
-- Determine whether entity Id is the spec entity of an entry [family]
|
||||
|
||||
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
|
||||
-- Predicate to determine whether a scope entity comes from a rewritten
|
||||
-- expression function call, and should be inlined unconditionally. Also
|
||||
|
|
|
|||
Loading…
Reference in New Issue