+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.
-- --
------------------------------------------------------------------------------
--- 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
-- 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;
-- 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;
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;
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);
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
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;
-- 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;
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
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
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;