[multiple changes]
2014-07-30 Robert Dewar <dewar@adacore.com> * sem_res.adb, sem_ch6.adb: Minor code reorganization. * inline.adb: Minor reformatting. 2014-07-30 Javier Miranda <miranda@adacore.com> * a-tags.ads: Add comments. From-SVN: r213272
This commit is contained in:
Arnaud Charlet
parent
2178830b04
commit
eb1ee7570a
5 changed files with 48 additions and 31 deletions
|
|
@ -1,3 +1,12 @@
|
|||
2014-07-30 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_res.adb, sem_ch6.adb: Minor code reorganization.
|
||||
* inline.adb: Minor reformatting.
|
||||
|
||||
2014-07-30 Javier Miranda <miranda@adacore.com>
|
||||
|
||||
* a-tags.ads: Add comments.
|
||||
|
||||
2014-07-30 Pat Rogers <rogers@adacore.com>
|
||||
|
||||
* gnat_rm.texi: Minor word error.
|
||||
|
|
|
|||
|
|
@ -33,11 +33,12 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
-- The operations in this package provide the guarantee that all dispatching
|
||||
-- calls on primitive operations of tagged types and interfaces take constant
|
||||
-- time (in terms of source lines executed), that is to say, the cost of these
|
||||
-- calls is independent of the number of primitives of the type or interface,
|
||||
-- and independent of the number of ancestors or interface progenitors that a
|
||||
-- For performance analysis, take into account that the operations in this
|
||||
-- package provide the guarantee that all dispatching calls on primitive
|
||||
-- operations of tagged types and interfaces take constant time (in terms
|
||||
-- of source lines executed), that is to say, the cost of these calls is
|
||||
-- independent of the number of primitives of the type or interface, and
|
||||
-- independent of the number of ancestors or interface progenitors that a
|
||||
-- tagged type may have.
|
||||
|
||||
-- The following subprograms of the public part of this package take constant
|
||||
|
|
@ -51,9 +52,17 @@
|
|||
-- The following subprograms of the public part of this package take non
|
||||
-- constant time (in terms of sources line executed):
|
||||
|
||||
-- Descendant_Tag (when used with a locally defined tagged type)
|
||||
-- Internal_Tag (when used with a locally defined tagged type)
|
||||
-- Interface_Ancestor_Tags
|
||||
-- Internal_Tag (when used with a locally defined tagged type), because in
|
||||
-- such case this routine processes the external tag, extract from it an
|
||||
-- address available there, and convert it into the tag value returned by
|
||||
-- this function. The number of instructions executed is not constant since
|
||||
-- it depends on the length of the external tag string.
|
||||
|
||||
-- Descendant_Tag (when used with a locally defined tagged type), because
|
||||
-- it relies on the subprogram Internal_Tag() to provide its functionality.
|
||||
|
||||
-- Interface_Ancestor_Tags, because this function returns a table whose
|
||||
-- length depends on the number of interfaces covered by a tagged type.
|
||||
|
||||
with System.Storage_Elements;
|
||||
|
||||
|
|
|
|||
|
|
@ -1697,9 +1697,9 @@ package body Inline is
|
|||
-- is analyzed, as this is where a pragma SPARK_Mode might be inserted.
|
||||
|
||||
elsif Present (Spec_Id)
|
||||
and then (No (SPARK_Pragma (Spec_Id))
|
||||
or else
|
||||
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
|
||||
and then
|
||||
(No (SPARK_Pragma (Spec_Id))
|
||||
or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
|
||||
then
|
||||
return False;
|
||||
|
||||
|
|
@ -1709,8 +1709,7 @@ package body Inline is
|
|||
elsif Instantiation_Location (Sloc (Id)) /= No_Location then
|
||||
return False;
|
||||
|
||||
-- Predicate functions are treated specially by GNATprove. Do not inline
|
||||
-- them.
|
||||
-- Don't inline predicate functions (treated specially by GNATprove)
|
||||
|
||||
elsif Is_Predicate_Function (Id) then
|
||||
return False;
|
||||
|
|
|
|||
|
|
@ -3070,12 +3070,13 @@ package body Sem_Ch6 is
|
|||
declare
|
||||
Body_Spec : constant Node_Id :=
|
||||
Copy_Separate_Tree (Specification (N));
|
||||
New_Decl : constant Node_Id :=
|
||||
Make_Subprogram_Declaration (Loc,
|
||||
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;
|
||||
Aspects : List_Id;
|
||||
Prag, Aspect : Node_Id;
|
||||
|
||||
begin
|
||||
Insert_Before (N, New_Decl);
|
||||
|
|
@ -3093,8 +3094,7 @@ package body Sem_Ch6 is
|
|||
Analyze (New_Decl);
|
||||
|
||||
-- The analysis of the generated subprogram declaration
|
||||
-- may have introduced pragmas, which need to be
|
||||
-- analyzed.
|
||||
-- may have introduced pragmas that need to be analyzed.
|
||||
|
||||
Prag := Next (New_Decl);
|
||||
while Prag /= N loop
|
||||
|
|
@ -3113,8 +3113,7 @@ package body Sem_Ch6 is
|
|||
SPARK_Mode_Aspect :=
|
||||
New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode));
|
||||
Set_Analyzed (SPARK_Mode_Aspect, False);
|
||||
Aspects := New_List;
|
||||
Append (SPARK_Mode_Aspect, Aspects);
|
||||
Aspects := New_List (SPARK_Mode_Aspect);
|
||||
Set_Aspect_Specifications (N, Aspects);
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -6216,15 +6216,16 @@ package body Sem_Res is
|
|||
-- being inlined.
|
||||
|
||||
declare
|
||||
Nam_Alias : constant Entity_Id := Ultimate_Alias (Nam);
|
||||
Decl : constant Node_Id := Unit_Declaration_Node (Nam_Alias);
|
||||
Nam_UA : constant Entity_Id := Ultimate_Alias (Nam);
|
||||
Decl : constant Node_Id := Unit_Declaration_Node (Nam_UA);
|
||||
|
||||
begin
|
||||
-- If the subprogram is not eligible for inlining in GNATprove
|
||||
-- mode, do nothing.
|
||||
|
||||
if not Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
|
||||
or else Nkind (Decl) /= N_Subprogram_Declaration
|
||||
or else not Is_Inlined_Always (Nam_Alias)
|
||||
if Nkind (Decl) /= N_Subprogram_Declaration
|
||||
or else not Is_Inlined_Always (Nam_UA)
|
||||
or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Empty)
|
||||
then
|
||||
null;
|
||||
|
||||
|
|
@ -6234,7 +6235,7 @@ package body Sem_Res is
|
|||
elsif In_Assertion_Expr /= 0 then
|
||||
Error_Msg_NE ("?cannot inline call to &", N, Nam);
|
||||
Error_Msg_N ("\call appears in assertion expression", N);
|
||||
Set_Is_Inlined_Always (Nam_Alias, False);
|
||||
Set_Is_Inlined_Always (Nam_UA, False);
|
||||
|
||||
-- Inlining should not be performed during pre-analysis
|
||||
|
||||
|
|
@ -6246,7 +6247,7 @@ package body Sem_Res is
|
|||
if No (Corresponding_Body (Decl)) then
|
||||
Error_Msg_NE
|
||||
("?cannot inline call to & (body not seen yet)", N, Nam);
|
||||
Set_Is_Inlined_Always (Nam_Alias, False);
|
||||
Set_Is_Inlined_Always (Nam_UA, False);
|
||||
|
||||
-- Nothing to do if there is no body to inline, indicating that
|
||||
-- the subprogram is not suitable for inlining in GNATprove
|
||||
|
|
@ -6263,12 +6264,12 @@ package body Sem_Res is
|
|||
Error_Msg_NE ("?cannot inline call to &", N, Nam);
|
||||
Error_Msg_N
|
||||
("\call appears in potentially unevaluated context", N);
|
||||
Set_Is_Inlined_Always (Nam_Alias, False);
|
||||
Set_Is_Inlined_Always (Nam_UA, False);
|
||||
|
||||
-- Otherwise, inline the call
|
||||
|
||||
else
|
||||
Expand_Inlined_Call (N, Nam_Alias, Nam);
|
||||
Expand_Inlined_Call (N, Nam_UA, Nam);
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue