[multiple changes]
2015-05-12 Ed Schonberg <schonberg@adacore.com> * sem_ch3.adb (Add_Internal_Interface_Entities): Do no generate freeze nodes for these in ASIS mode, because they lead to elaoration order issues in gigi. 2015-05-12 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch6.adb (Analyze_Expression_Function): Code cleanup. Use Copy_Subprogram_Spec to create a proper spec. (Analyze_Subprogram_Body_Helper): Code cleanup. Do not prepare a stand alone body for inlining in GNATprove mode when inside a generic. (Body_Has_Contract): Reimplemented. (Build_Subprogram_Declaration): New routine. * sem_ch10.adb (Analyze_Compilation_Unit): Capture global references within generic bodies by loading them. * sem_util.adb (Copy_Parameter_List): Code cleanup. (Copy_Subprogram_Spec): New routine. (Is_Contract_Annotation): New routine. * sem_util.ads (Copy_Subprogram_Spec): New routine. (Is_Contract_Annotation): New routine. 2015-05-12 Hristian Kirtchev <kirtchev@adacore.com> * sem_attr.adb (Resolve_Attribute): Do not analyze the generated body of an expression function when the prefix of attribute 'Access is the body. From-SVN: r223048
This commit is contained in:
parent
cb2e147086
commit
8d1fe980a2
|
@ -1,3 +1,31 @@
|
||||||
|
2015-05-12 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
|
* sem_ch3.adb (Add_Internal_Interface_Entities): Do no generate
|
||||||
|
freeze nodes for these in ASIS mode, because they lead to
|
||||||
|
elaoration order issues in gigi.
|
||||||
|
|
||||||
|
2015-05-12 Hristian Kirtchev <kirtchev@adacore.com>
|
||||||
|
|
||||||
|
* sem_ch6.adb (Analyze_Expression_Function): Code
|
||||||
|
cleanup. Use Copy_Subprogram_Spec to create a proper spec.
|
||||||
|
(Analyze_Subprogram_Body_Helper): Code cleanup. Do not
|
||||||
|
prepare a stand alone body for inlining in GNATprove mode
|
||||||
|
when inside a generic. (Body_Has_Contract): Reimplemented.
|
||||||
|
(Build_Subprogram_Declaration): New routine.
|
||||||
|
* sem_ch10.adb (Analyze_Compilation_Unit): Capture global
|
||||||
|
references within generic bodies by loading them.
|
||||||
|
* sem_util.adb (Copy_Parameter_List): Code cleanup.
|
||||||
|
(Copy_Subprogram_Spec): New routine.
|
||||||
|
(Is_Contract_Annotation): New routine.
|
||||||
|
* sem_util.ads (Copy_Subprogram_Spec): New routine.
|
||||||
|
(Is_Contract_Annotation): New routine.
|
||||||
|
|
||||||
|
2015-05-12 Hristian Kirtchev <kirtchev@adacore.com>
|
||||||
|
|
||||||
|
* sem_attr.adb (Resolve_Attribute): Do not analyze the generated
|
||||||
|
body of an expression function when the prefix of attribute
|
||||||
|
'Access is the body.
|
||||||
|
|
||||||
2015-05-12 Ed Schonberg <schonberg@adacore.com>
|
2015-05-12 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
* sem_ch3.adb (Build_Derived_Enumeration_Type): The anonymous base
|
* sem_ch3.adb (Build_Derived_Enumeration_Type): The anonymous base
|
||||||
|
|
|
@ -10675,13 +10675,31 @@ package body Sem_Attr is
|
||||||
Subp_Body :=
|
Subp_Body :=
|
||||||
Unit_Declaration_Node (Corresponding_Body (Subp_Decl));
|
Unit_Declaration_Node (Corresponding_Body (Subp_Decl));
|
||||||
|
|
||||||
-- Analyze the body of the expression function to freeze
|
-- The body has already been analyzed when the expression
|
||||||
-- the expression. This takes care of the case where the
|
-- function acts as a completion.
|
||||||
-- 'Access is part of dispatch table initialization and
|
|
||||||
-- the generated body of the expression function has not
|
|
||||||
-- been analyzed yet.
|
|
||||||
|
|
||||||
if not Analyzed (Subp_Body) then
|
if Analyzed (Subp_Body) then
|
||||||
|
null;
|
||||||
|
|
||||||
|
-- Attribute 'Access may appear within the generated body
|
||||||
|
-- of the expression function subject to the attribute:
|
||||||
|
|
||||||
|
-- function F is (... F'Access ...);
|
||||||
|
|
||||||
|
-- If the expression function is on the scope stack, then
|
||||||
|
-- the body is currently being analyzed. Do not reanalyze
|
||||||
|
-- it because this will lead to infinite recursion.
|
||||||
|
|
||||||
|
elsif In_Open_Scopes (Subp_Id) then
|
||||||
|
null;
|
||||||
|
|
||||||
|
-- Analyze the body of the expression function to freeze
|
||||||
|
-- the expression. This takes care of the case where the
|
||||||
|
-- 'Access is part of dispatch table initialization and
|
||||||
|
-- the generated body of the expression function has not
|
||||||
|
-- been analyzed yet.
|
||||||
|
|
||||||
|
else
|
||||||
Analyze (Subp_Body);
|
Analyze (Subp_Body);
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
|
@ -1020,16 +1020,18 @@ package body Sem_Ch10 is
|
||||||
|
|
||||||
Remove_Context (N);
|
Remove_Context (N);
|
||||||
|
|
||||||
-- If this is the main unit and we are generating code, we must check
|
-- When generating code for a non-generic main unit, check that withed
|
||||||
-- that all generic units in the context have a body if they need it,
|
-- generic units have a body if they need it, even if the units have not
|
||||||
-- even if they have not been instantiated. In the absence of .ali files
|
-- been instantiated. Force the load of the bodies to produce the proper
|
||||||
-- for generic units, we must force the load of the body, just to
|
-- error if the body is absent. The same applies to GNATprove mode, with
|
||||||
-- produce the proper error if the body is absent. We skip this
|
-- the added benefit of capturing global references within the generic.
|
||||||
-- verification if the main unit itself is generic.
|
-- This in turn allows for proper inlining of subprogram bodies without
|
||||||
|
-- a previous declaration.
|
||||||
|
|
||||||
if Get_Cunit_Unit_Number (N) = Main_Unit
|
if Get_Cunit_Unit_Number (N) = Main_Unit
|
||||||
and then Operating_Mode = Generate_Code
|
and then ((Operating_Mode = Generate_Code and then Expander_Active)
|
||||||
and then Expander_Active
|
or else
|
||||||
|
(Operating_Mode = Check_Semantics and then GNATprove_Mode))
|
||||||
then
|
then
|
||||||
-- Check whether the source for the body of the unit must be included
|
-- Check whether the source for the body of the unit must be included
|
||||||
-- in a standalone library.
|
-- in a standalone library.
|
||||||
|
@ -1066,7 +1068,7 @@ package body Sem_Ch10 is
|
||||||
then
|
then
|
||||||
Nam := Entity (Name (Item));
|
Nam := Entity (Name (Item));
|
||||||
|
|
||||||
-- Compile generic subprogram, unless it is intrinsic or
|
-- Compile the generic subprogram, unless it is intrinsic or
|
||||||
-- imported so no body is required, or generic package body
|
-- imported so no body is required, or generic package body
|
||||||
-- if the package spec requires a body.
|
-- if the package spec requires a body.
|
||||||
|
|
||||||
|
@ -1080,20 +1082,21 @@ package body Sem_Ch10 is
|
||||||
|
|
||||||
if Present (Renamed_Object (Nam)) then
|
if Present (Renamed_Object (Nam)) then
|
||||||
Un :=
|
Un :=
|
||||||
Load_Unit
|
Load_Unit
|
||||||
(Load_Name => Get_Body_Name
|
(Load_Name =>
|
||||||
(Get_Unit_Name
|
Get_Body_Name
|
||||||
(Unit_Declaration_Node
|
(Get_Unit_Name
|
||||||
(Renamed_Object (Nam)))),
|
(Unit_Declaration_Node
|
||||||
Required => False,
|
(Renamed_Object (Nam)))),
|
||||||
Subunit => False,
|
Required => False,
|
||||||
Error_Node => N,
|
Subunit => False,
|
||||||
Renamings => True);
|
Error_Node => N,
|
||||||
|
Renamings => True);
|
||||||
else
|
else
|
||||||
Un :=
|
Un :=
|
||||||
Load_Unit
|
Load_Unit
|
||||||
(Load_Name => Get_Body_Name
|
(Load_Name =>
|
||||||
(Get_Unit_Name (Item)),
|
Get_Body_Name (Get_Unit_Name (Item)),
|
||||||
Required => False,
|
Required => False,
|
||||||
Subunit => False,
|
Subunit => False,
|
||||||
Error_Node => N,
|
Error_Node => N,
|
||||||
|
|
|
@ -1772,9 +1772,13 @@ package body Sem_Ch3 is
|
||||||
-- locally defined tagged types (or compiling with static
|
-- locally defined tagged types (or compiling with static
|
||||||
-- dispatch tables generation disabled) the corresponding
|
-- dispatch tables generation disabled) the corresponding
|
||||||
-- entry of the secondary dispatch table is filled when
|
-- entry of the secondary dispatch table is filled when
|
||||||
-- such an entity is frozen.
|
-- such an entity is frozen. This is an expansion activity
|
||||||
|
-- that must be suppressed for ASIS because it leads to
|
||||||
|
-- gigi elaboration issues in annotate mode.
|
||||||
|
|
||||||
Set_Has_Delayed_Freeze (New_Subp);
|
if not ASIS_Mode then
|
||||||
|
Set_Has_Delayed_Freeze (New_Subp);
|
||||||
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
<<Continue>>
|
<<Continue>>
|
||||||
|
@ -1794,7 +1798,7 @@ package body Sem_Ch3 is
|
||||||
-----------------------------------
|
-----------------------------------
|
||||||
|
|
||||||
procedure Analyze_Component_Declaration (N : Node_Id) is
|
procedure Analyze_Component_Declaration (N : Node_Id) is
|
||||||
Loc : constant Source_Ptr := Sloc (N);
|
Loc : constant Source_Ptr := Sloc (Component_Definition (N));
|
||||||
Id : constant Entity_Id := Defining_Identifier (N);
|
Id : constant Entity_Id := Defining_Identifier (N);
|
||||||
E : constant Node_Id := Expression (N);
|
E : constant Node_Id := Expression (N);
|
||||||
Typ : constant Node_Id :=
|
Typ : constant Node_Id :=
|
||||||
|
@ -2137,9 +2141,14 @@ package body Sem_Ch3 is
|
||||||
then
|
then
|
||||||
declare
|
declare
|
||||||
Act_T : constant Entity_Id := Build_Default_Subtype (T, N);
|
Act_T : constant Entity_Id := Build_Default_Subtype (T, N);
|
||||||
|
|
||||||
begin
|
begin
|
||||||
Set_Etype (Id, Act_T);
|
Set_Etype (Id, Act_T);
|
||||||
Set_Component_Definition (N,
|
|
||||||
|
-- Rewrite the component definition to use the constrained
|
||||||
|
-- subtype.
|
||||||
|
|
||||||
|
Rewrite (Component_Definition (N),
|
||||||
Make_Component_Definition (Loc,
|
Make_Component_Definition (Loc,
|
||||||
Subtype_Indication => New_Occurrence_Of (Act_T, Loc)));
|
Subtype_Indication => New_Occurrence_Of (Act_T, Loc)));
|
||||||
end;
|
end;
|
||||||
|
|
|
@ -268,10 +268,10 @@ package body Sem_Ch6 is
|
||||||
---------------------------------
|
---------------------------------
|
||||||
|
|
||||||
procedure Analyze_Expression_Function (N : Node_Id) is
|
procedure Analyze_Expression_Function (N : Node_Id) is
|
||||||
Loc : constant Source_Ptr := Sloc (N);
|
Expr : constant Node_Id := Expression (N);
|
||||||
LocX : constant Source_Ptr := Sloc (Expression (N));
|
Loc : constant Source_Ptr := Sloc (N);
|
||||||
Expr : constant Node_Id := Expression (N);
|
LocX : constant Source_Ptr := Sloc (Expr);
|
||||||
Spec : constant Node_Id := Specification (N);
|
Spec : constant Node_Id := Specification (N);
|
||||||
|
|
||||||
Def_Id : Entity_Id;
|
Def_Id : Entity_Id;
|
||||||
|
|
||||||
|
@ -293,36 +293,11 @@ package body Sem_Ch6 is
|
||||||
|
|
||||||
Inline_Processing_Required := True;
|
Inline_Processing_Required := True;
|
||||||
|
|
||||||
-- Create a specification for the generated body. Types and defauts in
|
-- Create a specification for the generated body. This must be done
|
||||||
-- the profile are copies of the spec, but new entities must be created
|
-- prior to the analysis of the initial declaration.
|
||||||
-- for the unit name and the formals.
|
|
||||||
|
|
||||||
New_Spec := New_Copy_Tree (Spec);
|
New_Spec := Copy_Subprogram_Spec (Spec);
|
||||||
Set_Defining_Unit_Name (New_Spec,
|
Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
|
||||||
Make_Defining_Identifier (Sloc (Defining_Unit_Name (Spec)),
|
|
||||||
Chars (Defining_Unit_Name (Spec))));
|
|
||||||
|
|
||||||
if Present (Parameter_Specifications (New_Spec)) then
|
|
||||||
declare
|
|
||||||
Formal_Spec : Node_Id;
|
|
||||||
Def : Entity_Id;
|
|
||||||
|
|
||||||
begin
|
|
||||||
Formal_Spec := First (Parameter_Specifications (New_Spec));
|
|
||||||
|
|
||||||
-- Create a new formal parameter at the same source position
|
|
||||||
|
|
||||||
while Present (Formal_Spec) loop
|
|
||||||
Def := Defining_Identifier (Formal_Spec);
|
|
||||||
Set_Defining_Identifier (Formal_Spec,
|
|
||||||
Make_Defining_Identifier (Sloc (Def),
|
|
||||||
Chars => Chars (Def)));
|
|
||||||
Next (Formal_Spec);
|
|
||||||
end loop;
|
|
||||||
end;
|
|
||||||
end if;
|
|
||||||
|
|
||||||
Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
|
|
||||||
|
|
||||||
-- If there are previous overloadable entities with the same name,
|
-- If there are previous overloadable entities with the same name,
|
||||||
-- check whether any of them is completed by the expression function.
|
-- check whether any of them is completed by the expression function.
|
||||||
|
@ -2272,7 +2247,7 @@ package body Sem_Ch6 is
|
||||||
|
|
||||||
procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
|
procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
|
||||||
Loc : constant Source_Ptr := Sloc (N);
|
Loc : constant Source_Ptr := Sloc (N);
|
||||||
Body_Spec : constant Node_Id := Specification (N);
|
Body_Spec : Node_Id := Specification (N);
|
||||||
Body_Id : Entity_Id := Defining_Entity (Body_Spec);
|
Body_Id : Entity_Id := Defining_Entity (Body_Spec);
|
||||||
Prev_Id : constant Entity_Id := Current_Entity_In_Scope (Body_Id);
|
Prev_Id : constant Entity_Id := Current_Entity_In_Scope (Body_Id);
|
||||||
Conformant : Boolean;
|
Conformant : Boolean;
|
||||||
|
@ -2309,6 +2284,9 @@ package body Sem_Ch6 is
|
||||||
-- Check whether unanalyzed body has an aspect or pragma that may
|
-- Check whether unanalyzed body has an aspect or pragma that may
|
||||||
-- generate a SPARK contract.
|
-- generate a SPARK contract.
|
||||||
|
|
||||||
|
procedure Build_Subprogram_Declaration;
|
||||||
|
-- Create a matching subprogram declaration for subprogram body N
|
||||||
|
|
||||||
procedure Check_Anonymous_Return;
|
procedure Check_Anonymous_Return;
|
||||||
-- Ada 2005: if a function returns an access type that denotes a task,
|
-- Ada 2005: if a function returns an access type that denotes a task,
|
||||||
-- or a type that contains tasks, we must create a master entity for
|
-- or a type that contains tasks, we must create a master entity for
|
||||||
|
@ -2486,63 +2464,114 @@ package body Sem_Ch6 is
|
||||||
-----------------------
|
-----------------------
|
||||||
|
|
||||||
function Body_Has_Contract return Boolean is
|
function Body_Has_Contract return Boolean is
|
||||||
Decls : constant List_Id := Declarations (N);
|
Decls : constant List_Id := Declarations (N);
|
||||||
A_Spec : Node_Id;
|
Item : Node_Id;
|
||||||
A : Aspect_Id;
|
|
||||||
Decl : Node_Id;
|
|
||||||
P_Id : Pragma_Id;
|
|
||||||
|
|
||||||
begin
|
begin
|
||||||
-- Check for unanalyzed aspects in the body that will
|
-- Check for unanalyzed aspects in the body that will generate a
|
||||||
-- generate a contract.
|
-- contract.
|
||||||
|
|
||||||
if Present (Aspect_Specifications (N)) then
|
if Present (Aspect_Specifications (N)) then
|
||||||
A_Spec := First (Aspect_Specifications (N));
|
Item := First (Aspect_Specifications (N));
|
||||||
while Present (A_Spec) loop
|
while Present (Item) loop
|
||||||
A := Get_Aspect_Id (Chars (Identifier (A_Spec)));
|
if Is_Contract_Annotation (Item) then
|
||||||
|
|
||||||
if A = Aspect_Contract_Cases or else
|
|
||||||
A = Aspect_Depends or else
|
|
||||||
A = Aspect_Global or else
|
|
||||||
A = Aspect_Pre or else
|
|
||||||
A = Aspect_Precondition or else
|
|
||||||
A = Aspect_Post or else
|
|
||||||
A = Aspect_Postcondition
|
|
||||||
then
|
|
||||||
return True;
|
return True;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
Next (A_Spec);
|
Next (Item);
|
||||||
end loop;
|
end loop;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
-- Check for pragmas that may generate a contract
|
-- Check for pragmas that may generate a contract
|
||||||
|
|
||||||
if Present (Decls) then
|
if Present (Decls) then
|
||||||
Decl := First (Decls);
|
Item := First (Decls);
|
||||||
while Present (Decl) loop
|
while Present (Item) loop
|
||||||
if Nkind (Decl) = N_Pragma then
|
if Nkind (Item) = N_Pragma
|
||||||
P_Id := Get_Pragma_Id (Pragma_Name (Decl));
|
and then Is_Contract_Annotation (Item)
|
||||||
|
then
|
||||||
if P_Id = Pragma_Contract_Cases or else
|
return True;
|
||||||
P_Id = Pragma_Depends or else
|
|
||||||
P_Id = Pragma_Global or else
|
|
||||||
P_Id = Pragma_Pre or else
|
|
||||||
P_Id = Pragma_Precondition or else
|
|
||||||
P_Id = Pragma_Post or else
|
|
||||||
P_Id = Pragma_Postcondition
|
|
||||||
then
|
|
||||||
return True;
|
|
||||||
end if;
|
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
Next (Decl);
|
Next (Item);
|
||||||
end loop;
|
end loop;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
return False;
|
return False;
|
||||||
end Body_Has_Contract;
|
end Body_Has_Contract;
|
||||||
|
|
||||||
|
----------------------------------
|
||||||
|
-- Build_Subprogram_Declaration --
|
||||||
|
----------------------------------
|
||||||
|
|
||||||
|
procedure Build_Subprogram_Declaration is
|
||||||
|
Asp : Node_Id;
|
||||||
|
Decl : Node_Id;
|
||||||
|
Subp_Decl : Node_Id;
|
||||||
|
|
||||||
|
begin
|
||||||
|
-- Create a matching subprogram spec using the profile of the body.
|
||||||
|
-- The structure of the tree is identical, but has new entities for
|
||||||
|
-- the defining unit name and formal parameters.
|
||||||
|
|
||||||
|
Subp_Decl :=
|
||||||
|
Make_Subprogram_Declaration (Loc,
|
||||||
|
Specification => Copy_Subprogram_Spec (Body_Spec));
|
||||||
|
|
||||||
|
-- Relocate the aspects of the subprogram body to the new subprogram
|
||||||
|
-- spec because it acts as the initial declaration.
|
||||||
|
-- ??? what about pragmas
|
||||||
|
|
||||||
|
Move_Aspects (N, To => Subp_Decl);
|
||||||
|
Insert_Before_And_Analyze (N, Subp_Decl);
|
||||||
|
|
||||||
|
-- The analysis of the subprogram spec aspects may introduce pragmas
|
||||||
|
-- that need to be analyzed.
|
||||||
|
|
||||||
|
Decl := Next (Subp_Decl);
|
||||||
|
while Present (Decl) loop
|
||||||
|
|
||||||
|
-- Stop the search for pragmas once the body has been reached as
|
||||||
|
-- this terminates the region where pragmas may appear.
|
||||||
|
|
||||||
|
if Decl = N then
|
||||||
|
exit;
|
||||||
|
|
||||||
|
elsif Nkind (Decl) = N_Pragma then
|
||||||
|
Analyze (Decl);
|
||||||
|
end if;
|
||||||
|
|
||||||
|
Next (Decl);
|
||||||
|
end loop;
|
||||||
|
|
||||||
|
Spec_Id := Defining_Entity (Subp_Decl);
|
||||||
|
Set_Corresponding_Spec (N, Spec_Id);
|
||||||
|
|
||||||
|
-- Mark the generated spec as a source construct to ensure that all
|
||||||
|
-- calls to it are properly registered in ALI files for GNATprove.
|
||||||
|
|
||||||
|
Set_Comes_From_Source (Spec_Id, True);
|
||||||
|
|
||||||
|
-- If aspect SPARK_Mode was specified on the body, it needs to be
|
||||||
|
-- repeated both on the generated spec and the body.
|
||||||
|
|
||||||
|
Asp := Find_Aspect (Spec_Id, Aspect_SPARK_Mode);
|
||||||
|
|
||||||
|
if Present (Asp) then
|
||||||
|
Asp := New_Copy_Tree (Asp);
|
||||||
|
Set_Analyzed (Asp, False);
|
||||||
|
Set_Aspect_Specifications (N, New_List (Asp));
|
||||||
|
end if;
|
||||||
|
|
||||||
|
-- Ensure that the specs of the subprogram declaration and its body
|
||||||
|
-- are identical, otherwise they will appear non-conformant due to
|
||||||
|
-- rewritings in the default values of formal parameters.
|
||||||
|
|
||||||
|
Body_Spec := Copy_Subprogram_Spec (Body_Spec);
|
||||||
|
Set_Specification (N, Body_Spec);
|
||||||
|
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
|
||||||
|
end Build_Subprogram_Declaration;
|
||||||
|
|
||||||
----------------------------
|
----------------------------
|
||||||
-- Check_Anonymous_Return --
|
-- Check_Anonymous_Return --
|
||||||
----------------------------
|
----------------------------
|
||||||
|
@ -3221,68 +3250,9 @@ package body Sem_Ch6 is
|
||||||
-- to the spec, leading to legality errors.
|
-- to the spec, leading to legality errors.
|
||||||
|
|
||||||
and then not Body_Has_Contract
|
and then not Body_Has_Contract
|
||||||
|
and then not Inside_A_Generic
|
||||||
then
|
then
|
||||||
declare
|
Build_Subprogram_Declaration;
|
||||||
Body_Spec : constant Node_Id :=
|
|
||||||
Copy_Separate_Tree (Specification (N));
|
|
||||||
New_Decl : constant Node_Id :=
|
|
||||||
Make_Subprogram_Declaration (Loc,
|
|
||||||
Copy_Separate_Tree (Specification (N)));
|
|
||||||
|
|
||||||
SPARK_Mode_Aspect : Node_Id;
|
|
||||||
Aspects : List_Id;
|
|
||||||
Prag, Aspect : Node_Id;
|
|
||||||
|
|
||||||
begin
|
|
||||||
Insert_Before (N, New_Decl);
|
|
||||||
Move_Aspects (From => N, To => New_Decl);
|
|
||||||
|
|
||||||
-- Mark the newly moved aspects as not analyzed, so that
|
|
||||||
-- their effect on New_Decl is properly analyzed.
|
|
||||||
|
|
||||||
Aspect := First (Aspect_Specifications (New_Decl));
|
|
||||||
while Present (Aspect) loop
|
|
||||||
Set_Analyzed (Aspect, False);
|
|
||||||
Next (Aspect);
|
|
||||||
end loop;
|
|
||||||
|
|
||||||
Analyze (New_Decl);
|
|
||||||
|
|
||||||
-- The analysis of the generated subprogram declaration
|
|
||||||
-- may have introduced pragmas that need to be analyzed.
|
|
||||||
|
|
||||||
Prag := Next (New_Decl);
|
|
||||||
while Prag /= N loop
|
|
||||||
Analyze (Prag);
|
|
||||||
Next (Prag);
|
|
||||||
end loop;
|
|
||||||
|
|
||||||
Spec_Id := Defining_Entity (New_Decl);
|
|
||||||
|
|
||||||
-- As Body_Id originally comes from source, mark the new
|
|
||||||
-- Spec_Id as such, which is required so that calls to
|
|
||||||
-- this subprogram are registered in the local effects
|
|
||||||
-- stored in ALI files for GNATprove.
|
|
||||||
|
|
||||||
Set_Comes_From_Source (Spec_Id, True);
|
|
||||||
|
|
||||||
-- If aspect SPARK_Mode was specified on the body, it
|
|
||||||
-- needs to be repeated on the generated decl and the
|
|
||||||
-- body. Since the original aspect was moved to the
|
|
||||||
-- generated decl, copy it for the body.
|
|
||||||
|
|
||||||
if Has_Aspect (Spec_Id, Aspect_SPARK_Mode) then
|
|
||||||
SPARK_Mode_Aspect :=
|
|
||||||
New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode));
|
|
||||||
Set_Analyzed (SPARK_Mode_Aspect, False);
|
|
||||||
Aspects := New_List (SPARK_Mode_Aspect);
|
|
||||||
Set_Aspect_Specifications (N, Aspects);
|
|
||||||
end if;
|
|
||||||
|
|
||||||
Set_Specification (N, Body_Spec);
|
|
||||||
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
|
|
||||||
Set_Corresponding_Spec (N, Spec_Id);
|
|
||||||
end;
|
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
@ -3777,7 +3747,8 @@ package body Sem_Ch6 is
|
||||||
and then Full_Analysis
|
and then Full_Analysis
|
||||||
and then not Inside_A_Generic
|
and then not Inside_A_Generic
|
||||||
and then Present (Spec_Id)
|
and then Present (Spec_Id)
|
||||||
and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
|
and then Nkind (Unit_Declaration_Node (Spec_Id)) =
|
||||||
|
N_Subprogram_Declaration
|
||||||
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
|
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
|
||||||
and then not Body_Has_Contract
|
and then not Body_Has_Contract
|
||||||
then
|
then
|
||||||
|
|
|
@ -4412,21 +4412,19 @@ package body Sem_Util is
|
||||||
if No (First_Formal (Subp_Id)) then
|
if No (First_Formal (Subp_Id)) then
|
||||||
return No_List;
|
return No_List;
|
||||||
else
|
else
|
||||||
Plist := New_List;
|
Plist := New_List;
|
||||||
Formal := First_Formal (Subp_Id);
|
Formal := First_Formal (Subp_Id);
|
||||||
while Present (Formal) loop
|
while Present (Formal) loop
|
||||||
Append
|
Append_To (Plist,
|
||||||
(Make_Parameter_Specification (Loc,
|
Make_Parameter_Specification (Loc,
|
||||||
Defining_Identifier =>
|
Defining_Identifier =>
|
||||||
Make_Defining_Identifier (Sloc (Formal),
|
Make_Defining_Identifier (Sloc (Formal), Chars (Formal)),
|
||||||
Chars => Chars (Formal)),
|
In_Present => In_Present (Parent (Formal)),
|
||||||
In_Present => In_Present (Parent (Formal)),
|
Out_Present => Out_Present (Parent (Formal)),
|
||||||
Out_Present => Out_Present (Parent (Formal)),
|
Parameter_Type =>
|
||||||
Parameter_Type =>
|
|
||||||
New_Occurrence_Of (Etype (Formal), Loc),
|
New_Occurrence_Of (Etype (Formal), Loc),
|
||||||
Expression =>
|
Expression =>
|
||||||
New_Copy_Tree (Expression (Parent (Formal)))),
|
New_Copy_Tree (Expression (Parent (Formal)))));
|
||||||
Plist);
|
|
||||||
|
|
||||||
Next_Formal (Formal);
|
Next_Formal (Formal);
|
||||||
end loop;
|
end loop;
|
||||||
|
@ -4435,6 +4433,43 @@ package body Sem_Util is
|
||||||
return Plist;
|
return Plist;
|
||||||
end Copy_Parameter_List;
|
end Copy_Parameter_List;
|
||||||
|
|
||||||
|
--------------------------
|
||||||
|
-- Copy_Subprogram_Spec --
|
||||||
|
--------------------------
|
||||||
|
|
||||||
|
function Copy_Subprogram_Spec (Spec : Node_Id) return Node_Id is
|
||||||
|
Def_Id : Node_Id;
|
||||||
|
Formal_Spec : Node_Id;
|
||||||
|
Result : Node_Id;
|
||||||
|
|
||||||
|
begin
|
||||||
|
-- The structure of the original tree must be replicated without any
|
||||||
|
-- alterations. Use New_Copy_Tree for this purpose.
|
||||||
|
|
||||||
|
Result := New_Copy_Tree (Spec);
|
||||||
|
|
||||||
|
-- Create a new entity for the defining unit name
|
||||||
|
|
||||||
|
Def_Id := Defining_Unit_Name (Result);
|
||||||
|
Set_Defining_Unit_Name (Result,
|
||||||
|
Make_Defining_Identifier (Sloc (Def_Id), Chars (Def_Id)));
|
||||||
|
|
||||||
|
-- Create new entities for the formal parameters
|
||||||
|
|
||||||
|
if Present (Parameter_Specifications (Result)) then
|
||||||
|
Formal_Spec := First (Parameter_Specifications (Result));
|
||||||
|
while Present (Formal_Spec) loop
|
||||||
|
Def_Id := Defining_Identifier (Formal_Spec);
|
||||||
|
Set_Defining_Identifier (Formal_Spec,
|
||||||
|
Make_Defining_Identifier (Sloc (Def_Id), Chars (Def_Id)));
|
||||||
|
|
||||||
|
Next (Formal_Spec);
|
||||||
|
end loop;
|
||||||
|
end if;
|
||||||
|
|
||||||
|
return Result;
|
||||||
|
end Copy_Subprogram_Spec;
|
||||||
|
|
||||||
--------------------------------
|
--------------------------------
|
||||||
-- Corresponding_Generic_Type --
|
-- Corresponding_Generic_Type --
|
||||||
--------------------------------
|
--------------------------------
|
||||||
|
@ -10299,6 +10334,29 @@ package body Sem_Util is
|
||||||
or else Is_Task_Interface (T));
|
or else Is_Task_Interface (T));
|
||||||
end Is_Concurrent_Interface;
|
end Is_Concurrent_Interface;
|
||||||
|
|
||||||
|
-----------------------
|
||||||
|
-- Is_Constant_Bound --
|
||||||
|
-----------------------
|
||||||
|
|
||||||
|
function Is_Constant_Bound (Exp : Node_Id) return Boolean is
|
||||||
|
begin
|
||||||
|
if Compile_Time_Known_Value (Exp) then
|
||||||
|
return True;
|
||||||
|
|
||||||
|
elsif Is_Entity_Name (Exp) and then Present (Entity (Exp)) then
|
||||||
|
return Is_Constant_Object (Entity (Exp))
|
||||||
|
or else Ekind (Entity (Exp)) = E_Enumeration_Literal;
|
||||||
|
|
||||||
|
elsif Nkind (Exp) in N_Binary_Op then
|
||||||
|
return Is_Constant_Bound (Left_Opnd (Exp))
|
||||||
|
and then Is_Constant_Bound (Right_Opnd (Exp))
|
||||||
|
and then Scope (Entity (Exp)) = Standard_Standard;
|
||||||
|
|
||||||
|
else
|
||||||
|
return False;
|
||||||
|
end if;
|
||||||
|
end Is_Constant_Bound;
|
||||||
|
|
||||||
---------------------------
|
---------------------------
|
||||||
-- Is_Container_Element --
|
-- Is_Container_Element --
|
||||||
---------------------------
|
---------------------------
|
||||||
|
@ -10478,28 +10536,40 @@ package body Sem_Util is
|
||||||
end;
|
end;
|
||||||
end Is_Container_Element;
|
end Is_Container_Element;
|
||||||
|
|
||||||
-----------------------
|
----------------------------
|
||||||
-- Is_Constant_Bound --
|
-- Is_Contract_Annotation --
|
||||||
-----------------------
|
----------------------------
|
||||||
|
|
||||||
|
function Is_Contract_Annotation (Item : Node_Id) return Boolean is
|
||||||
|
Nam : Name_Id;
|
||||||
|
|
||||||
function Is_Constant_Bound (Exp : Node_Id) return Boolean is
|
|
||||||
begin
|
begin
|
||||||
if Compile_Time_Known_Value (Exp) then
|
if Nkind (Item) = N_Aspect_Specification then
|
||||||
return True;
|
Nam := Chars (Identifier (Item));
|
||||||
|
|
||||||
elsif Is_Entity_Name (Exp) and then Present (Entity (Exp)) then
|
else pragma Assert (Nkind (Item) = N_Pragma);
|
||||||
return Is_Constant_Object (Entity (Exp))
|
Nam := Pragma_Name (Item);
|
||||||
or else Ekind (Entity (Exp)) = E_Enumeration_Literal;
|
|
||||||
|
|
||||||
elsif Nkind (Exp) in N_Binary_Op then
|
|
||||||
return Is_Constant_Bound (Left_Opnd (Exp))
|
|
||||||
and then Is_Constant_Bound (Right_Opnd (Exp))
|
|
||||||
and then Scope (Entity (Exp)) = Standard_Standard;
|
|
||||||
|
|
||||||
else
|
|
||||||
return False;
|
|
||||||
end if;
|
end if;
|
||||||
end Is_Constant_Bound;
|
|
||||||
|
return
|
||||||
|
Nam = Name_Abstract_State
|
||||||
|
or else Nam = Name_Contract_Cases
|
||||||
|
or else Nam = Name_Depends
|
||||||
|
or else Nam = Name_Extensions_Visible
|
||||||
|
or else Nam = Name_Global
|
||||||
|
or else Nam = Name_Initial_Condition
|
||||||
|
or else Nam = Name_Initializes
|
||||||
|
or else Nam = Name_Post
|
||||||
|
or else Nam = Name_Post_Class
|
||||||
|
or else Nam = Name_Postcondition
|
||||||
|
or else Nam = Name_Pre
|
||||||
|
or else Nam = Name_Pre_Class
|
||||||
|
or else Nam = Name_Precondition
|
||||||
|
or else Nam = Name_Refined_Depends
|
||||||
|
or else Nam = Name_Refined_Global
|
||||||
|
or else Nam = Name_Refined_State
|
||||||
|
or else Nam = Name_Test_Case;
|
||||||
|
end Is_Contract_Annotation;
|
||||||
|
|
||||||
--------------------------------------
|
--------------------------------------
|
||||||
-- Is_Controlling_Limited_Procedure --
|
-- Is_Controlling_Limited_Procedure --
|
||||||
|
|
|
@ -397,12 +397,6 @@ package Sem_Util is
|
||||||
-- Depends
|
-- Depends
|
||||||
-- Global
|
-- Global
|
||||||
|
|
||||||
function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
|
|
||||||
-- Utility to create a parameter profile for a new subprogram spec, when
|
|
||||||
-- the subprogram has a body that acts as spec. This is done for some cases
|
|
||||||
-- of inlining, and for private protected ops. Also used to create bodies
|
|
||||||
-- for stubbed subprograms.
|
|
||||||
|
|
||||||
function Copy_Component_List
|
function Copy_Component_List
|
||||||
(R_Typ : Entity_Id;
|
(R_Typ : Entity_Id;
|
||||||
Loc : Source_Ptr) return List_Id;
|
Loc : Source_Ptr) return List_Id;
|
||||||
|
@ -410,6 +404,17 @@ package Sem_Util is
|
||||||
-- create a new compatible record type. Loc is the source location assigned
|
-- create a new compatible record type. Loc is the source location assigned
|
||||||
-- to the created nodes.
|
-- to the created nodes.
|
||||||
|
|
||||||
|
function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
|
||||||
|
-- Utility to create a parameter profile for a new subprogram spec, when
|
||||||
|
-- the subprogram has a body that acts as spec. This is done for some cases
|
||||||
|
-- of inlining, and for private protected ops. Also used to create bodies
|
||||||
|
-- for stubbed subprograms.
|
||||||
|
|
||||||
|
function Copy_Subprogram_Spec (Spec : Node_Id) return Node_Id;
|
||||||
|
-- Replicate a function or a procedure specification denoted by Spec. The
|
||||||
|
-- resulting tree is an exact duplicate of the original tree. New entities
|
||||||
|
-- are created for the unit name and the formal parameters.
|
||||||
|
|
||||||
function Corresponding_Generic_Type (T : Entity_Id) return Entity_Id;
|
function Corresponding_Generic_Type (T : Entity_Id) return Entity_Id;
|
||||||
-- If a type is a generic actual type, return the corresponding formal in
|
-- If a type is a generic actual type, return the corresponding formal in
|
||||||
-- the generic parent unit. There is no direct link in the tree for this
|
-- the generic parent unit. There is no direct link in the tree for this
|
||||||
|
@ -1186,6 +1191,10 @@ package Sem_Util is
|
||||||
-- explicit dereference. The transformation applies when it has the form
|
-- explicit dereference. The transformation applies when it has the form
|
||||||
-- F (X).Discr.all.
|
-- F (X).Discr.all.
|
||||||
|
|
||||||
|
function Is_Contract_Annotation (Item : Node_Id) return Boolean;
|
||||||
|
-- Determine whether aspect specification or pragma Item is a contract
|
||||||
|
-- annotation.
|
||||||
|
|
||||||
function Is_Controlling_Limited_Procedure
|
function Is_Controlling_Limited_Procedure
|
||||||
(Proc_Nam : Entity_Id) return Boolean;
|
(Proc_Nam : Entity_Id) return Boolean;
|
||||||
-- Ada 2005 (AI-345): Determine whether Proc_Nam is a primitive procedure
|
-- Ada 2005 (AI-345): Determine whether Proc_Nam is a primitive procedure
|
||||||
|
|
Loading…
Reference in New Issue