-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, 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- --
-- body. Early instantiations can also appear if generic, instance and
-- body are all in the declarative part of a subprogram or entry. Entities
-- of packages that are early instantiations are delayed, and their freeze
- -- node appears after the generic body.
+ -- node appears after the generic body. This rather complex machinery is
+ -- needed when nested instantiations are present, because the source does
+ -- not carry any indication of where the corresponding instance bodies must
+ -- be installed and frozen.
procedure Install_Formal_Packages (Par : Entity_Id);
-- Install the visible part of any formal of the parent that is a formal
F_Copy : List_Id) return List_Id
is
Actuals_To_Freeze : constant Elist_Id := New_Elmt_List;
- Assoc : constant List_Id := New_List;
+ Assoc_List : constant List_Id := New_List;
Default_Actuals : constant List_Id := New_List;
Gen_Unit : constant Entity_Id :=
Defining_Entity (Parent (F_Copy));
-- In Ada 2005, indicates partial parameterization of a formal
-- package. As usual an other association must be last in the list.
+ procedure Check_Fixed_Point_Actual (Actual : Node_Id);
+ -- Warn if an actual fixed-point type has user-defined arithmetic
+ -- operations, but there is no corresponding formal in the generic,
+ -- in which case the predefined operations will be used. This merits
+ -- a warning because of the special semantics of fixed point ops.
+
procedure Check_Overloaded_Formal_Subprogram (Formal : Entity_Id);
-- Apply RM 12.3(9): if a formal subprogram is overloaded, the instance
-- cannot have a named association for it. AI05-0025 extends this rule
end loop;
end Check_Overloaded_Formal_Subprogram;
+ -------------------------------
+ -- Check_Fixed_Point_Actual --
+ -------------------------------
+
+ procedure Check_Fixed_Point_Actual (Actual : Node_Id) is
+ Typ : constant Entity_Id := Entity (Actual);
+ Prims : constant Elist_Id := Collect_Primitive_Operations (Typ);
+ Elem : Elmt_Id;
+ Formal : Node_Id;
+ Op : Entity_Id;
+
+ begin
+ -- Locate primitive operations of the type that are arithmetic
+ -- operations.
+
+ Elem := First_Elmt (Prims);
+ while Present (Elem) loop
+ if Nkind (Node (Elem)) = N_Defining_Operator_Symbol then
+
+ -- Check whether the generic unit has a formal subprogram of
+ -- the same name. This does not check types but is good enough
+ -- to justify a warning.
+
+ Formal := First_Non_Pragma (Formals);
+ Op := Alias (Node (Elem));
+
+ while Present (Formal) loop
+ if Nkind (Formal) = N_Formal_Concrete_Subprogram_Declaration
+ and then Chars (Defining_Entity (Formal)) =
+ Chars (Node (Elem))
+ then
+ exit;
+
+ elsif Nkind (Formal) = N_Formal_Package_Declaration then
+ declare
+ Assoc : Node_Id;
+ Ent : Entity_Id;
+
+ begin
+ -- Locate corresponding actual, and check whether it
+ -- includes a fixed-point type.
+
+ Assoc := First (Assoc_List);
+ while Present (Assoc) loop
+ exit when
+ Nkind (Assoc) = N_Package_Renaming_Declaration
+ and then Chars (Defining_Unit_Name (Assoc)) =
+ Chars (Defining_Identifier (Formal));
+
+ Next (Assoc);
+ end loop;
+
+ if Present (Assoc) then
+
+ -- If formal package declares a fixed-point type,
+ -- and the user-defined operator is derived from
+ -- a generic instance package, the fixed-point type
+ -- does not use the corresponding predefined op.
+
+ Ent := First_Entity (Entity (Name (Assoc)));
+ while Present (Ent) loop
+ if Is_Fixed_Point_Type (Ent)
+ and then Present (Op)
+ and then Is_Generic_Instance (Scope (Op))
+ then
+ return;
+ end if;
+
+ Next_Entity (Ent);
+ end loop;
+ end if;
+ end;
+ end if;
+
+ Next (Formal);
+ end loop;
+
+ if No (Formal) then
+ Error_Msg_Sloc := Sloc (Node (Elem));
+ Error_Msg_NE
+ ("?instance does not use primitive operation&#",
+ Actual, Node (Elem));
+ end if;
+ end if;
+
+ Next_Elmt (Elem);
+ end loop;
+ end Check_Fixed_Point_Actual;
+
-------------------------------
-- Has_Fully_Defined_Profile --
-------------------------------
Set_Defining_Identifier (Decl, Id);
end if;
- Append (Decl, Assoc);
+ Append (Decl, Assoc_List);
if No (Found_Assoc) then
Default :=
Kind := Nkind (Analyzed_Formal);
case Nkind (Formal) is
-
when N_Formal_Subprogram_Declaration =>
exit when Kind in N_Formal_Subprogram_Declaration
and then
N_Generic_Package_Declaration,
N_Package_Declaration);
- when N_Use_Package_Clause | N_Use_Type_Clause => exit;
+ when N_Use_Package_Clause
+ | N_Use_Type_Clause
+ =>
+ exit;
when others =>
else
Append_List
(Instantiate_Object (Formal, Match, Analyzed_Formal),
- Assoc);
+ Assoc_List);
-- For a defaulted in_parameter, create an entry in the
-- the list of defaulted actuals, for GNATProve use. Do
Analyze (Match);
Append_List
(Instantiate_Type
- (Formal, Match, Analyzed_Formal, Assoc),
- Assoc);
+ (Formal, Match, Analyzed_Formal, Assoc_List),
+ Assoc_List);
+
+ if Is_Fixed_Point_Type (Entity (Match)) then
+ Check_Fixed_Point_Actual (Match);
+ end if;
-- An instantiation is a freeze point for the actuals,
-- unless this is a rewritten formal package, or the
end if;
else
- Append_To (Assoc,
+ Append_To (Assoc_List,
Instantiate_Formal_Subprogram
(Formal, Match, Analyzed_Formal));
if No (Match) and then Box_Present (Formal) then
declare
Subp : constant Entity_Id :=
- Defining_Unit_Name (Specification (Last (Assoc)));
+ Defining_Unit_Name
+ (Specification (Last (Assoc_List)));
begin
Append_To (Default_Actuals,
Append_List
(Instantiate_Formal_Package
(Formal, Match, Analyzed_Formal),
- Assoc);
+ Assoc_List);
+
+ -- Determine whether the actual package needs an explicit
+ -- freeze node. This is only the case if the actual is
+ -- declared in the same unit and has a body. Normally
+ -- packages do not have explicit freeze nodes, and gigi
+ -- only uses them to elaborate entities in a package
+ -- body.
+
+ declare
+ Actual : constant Entity_Id := Entity (Match);
+
+ Needs_Freezing : Boolean;
+ S : Entity_Id;
+
+ begin
+ if not Expander_Active
+ or else not Has_Completion (Actual)
+ or else not In_Same_Source_Unit (I_Node, Actual)
+ or else
+ (Present (Renamed_Entity (Actual))
+ and then not
+ In_Same_Source_Unit
+ (I_Node, (Renamed_Entity (Actual))))
+ then
+ null;
+
+ else
+ -- Finally we want to exclude such freeze nodes
+ -- from statement sequences, which freeze
+ -- everything before them.
+ -- Is this strictly necessary ???
+
+ Needs_Freezing := True;
+
+ S := Current_Scope;
+ while Present (S) loop
+ if Ekind_In (S, E_Block,
+ E_Function,
+ E_Loop,
+ E_Procedure)
+ then
+ Needs_Freezing := False;
+ exit;
+ end if;
+
+ S := Scope (S);
+ end loop;
+
+ if Needs_Freezing then
+ Set_Has_Delayed_Freeze (Actual);
+ Append_Elmt (Actual, Actuals_To_Freeze);
+ end if;
+ end if;
+ end;
end if;
-- For use type and use package appearing in the generic part,
-- they belong (we mustn't recopy them since this would mess up
-- the Sloc values).
- when N_Use_Package_Clause |
- N_Use_Type_Clause =>
+ when N_Use_Package_Clause
+ | N_Use_Type_Clause
+ =>
if Nkind (Original_Node (I_Node)) =
N_Formal_Package_Declaration
then
- Append (New_Copy_Tree (Formal), Assoc);
+ Append (New_Copy_Tree (Formal), Assoc_List);
else
Remove (Formal);
- Append (Formal, Assoc);
+ Append (Formal, Assoc_List);
end if;
when others =>
raise Program_Error;
-
end case;
Formal := Saved_Formal;
Append_List (Default_Formals, Formals);
end if;
- return Assoc;
+ return Assoc_List;
end Analyze_Associations;
-------------------------------
(Generic_Formal_Declarations (Original_Node (Gen_Decl)));
while Present (Formal_Decl) loop
Append_To
- (Decls, Copy_Generic_Node (Formal_Decl, Empty, True));
+ (Decls,
+ Copy_Generic_Node
+ (Formal_Decl, Empty, Instantiating => True));
Next (Formal_Decl);
end loop;
end;
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Associations : Boolean := True;
New_N : Node_Id;
-- continue analysis to minimize cascaded errors.
Error_Msg_N
- ("generic parent cannot be used as formal package "
- & "of a child unit", Gen_Id);
+ ("generic parent cannot be used as formal package of a child "
+ & "unit", Gen_Id);
else
Error_Msg_N
- ("generic package cannot be used as a formal package "
- & "within itself", Gen_Id);
+ ("generic package cannot be used as a formal package within "
+ & "itself", Gen_Id);
Restore_Env;
goto Leave;
end if;
-- all SPARK_Mode pragmas within the generic_package_name.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the formal spec in case the body is instantiated at a later
+ -- pass. This preserves the original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Formal);
end if;
Analyze (Specification (N));
Analyze_Aspect_Specifications (N, Pack_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
end Analyze_Formal_Package_Declaration;
---------------------------------
-- Enter the new name, and branch to specific routine
case Nkind (Def) is
- when N_Formal_Private_Type_Definition =>
+ when N_Formal_Private_Type_Definition =>
Analyze_Formal_Private_Type (N, T, Def);
- when N_Formal_Derived_Type_Definition =>
+ when N_Formal_Derived_Type_Definition =>
Analyze_Formal_Derived_Type (N, T, Def);
- when N_Formal_Incomplete_Type_Definition =>
+ when N_Formal_Incomplete_Type_Definition =>
Analyze_Formal_Incomplete_Type (T, Def);
- when N_Formal_Discrete_Type_Definition =>
+ when N_Formal_Discrete_Type_Definition =>
Analyze_Formal_Discrete_Type (T, Def);
- when N_Formal_Signed_Integer_Type_Definition =>
+ when N_Formal_Signed_Integer_Type_Definition =>
Analyze_Formal_Signed_Integer_Type (T, Def);
- when N_Formal_Modular_Type_Definition =>
+ when N_Formal_Modular_Type_Definition =>
Analyze_Formal_Modular_Type (T, Def);
- when N_Formal_Floating_Point_Definition =>
+ when N_Formal_Floating_Point_Definition =>
Analyze_Formal_Floating_Type (T, Def);
when N_Formal_Ordinary_Fixed_Point_Definition =>
Analyze_Formal_Ordinary_Fixed_Point_Type (T, Def);
- when N_Formal_Decimal_Fixed_Point_Definition =>
+ when N_Formal_Decimal_Fixed_Point_Definition =>
Analyze_Formal_Decimal_Fixed_Point_Type (T, Def);
when N_Array_Type_Definition =>
Analyze_Formal_Array_Type (T, Def);
- when N_Access_To_Object_Definition |
- N_Access_Function_Definition |
- N_Access_Procedure_Definition =>
+ when N_Access_Function_Definition
+ | N_Access_Procedure_Definition
+ | N_Access_To_Object_Definition
+ =>
Analyze_Generic_Access_Type (T, Def);
-- Ada 2005: a interface declaration is encoded as an abstract
-- record declaration or a abstract type derivation.
- when N_Record_Definition =>
+ when N_Record_Definition =>
Analyze_Formal_Interface_Type (N, T, Def);
- when N_Derived_Type_Definition =>
+ when N_Derived_Type_Definition =>
Analyze_Formal_Derived_Interface_Type (N, T, Def);
- when N_Error =>
+ when N_Error =>
null;
- when others =>
+ when others =>
raise Program_Error;
-
end case;
Set_Is_Generic_Type (T);
Set_Ekind (Id, E_Generic_Package);
Set_Etype (Id, Standard_Void_Type);
- -- A generic package declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
+ -- Set SPARK_Mode from context
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id);
+ Set_SPARK_Aux_Pragma_Inherited (Id);
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
End_Package_Scope (Id);
Exit_Generic_Scope (Id);
+ -- If the generic appears within a package unit, the body of that unit
+ -- has to be present for instantiation and inlining.
+
+ if Nkind (Unit (Cunit (Current_Sem_Unit))) = N_Package_Declaration then
+ Set_Body_Needed_For_Inlining
+ (Defining_Entity (Unit (Cunit (Current_Sem_Unit))));
+ end if;
+
if Nkind (Parent (N)) /= N_Compilation_Unit then
Move_Freeze_Nodes (Id, N, Visible_Declarations (Specification (N)));
Move_Freeze_Nodes (Id, N, Private_Declarations (Specification (N)));
Set_Etype (Id, Standard_Void_Type);
end if;
- -- A generic subprogram declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- For a library unit, we have reconstructed the entity for the unit,
-- and must reset it in the library tables. We also make sure that
-- Body_Required is set properly in the original compilation unit node.
Set_Body_Required (Parent (N), Unit_Requires_Body (Id));
end if;
+ -- If the generic appears within a package unit, the body of that unit
+ -- has to be present for instantiation and inlining.
+
+ if Nkind (Unit (Cunit (Current_Sem_Unit))) = N_Package_Declaration
+ and then Unit_Requires_Body (Id)
+ then
+ Set_Body_Needed_For_Inlining
+ (Defining_Entity (Unit (Cunit (Current_Sem_Unit))));
+ end if;
+
Set_Categorization_From_Pragmas (N);
Validate_Categorization_Dependency (N, Id);
-- Analyze_Package_Instantiation --
-----------------------------------
- procedure Analyze_Package_Instantiation (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Gen_Id : constant Node_Id := Name (N);
-
- Act_Decl : Node_Id;
- Act_Decl_Name : Node_Id;
- Act_Decl_Id : Entity_Id;
- Act_Spec : Node_Id;
- Act_Tree : Node_Id;
-
- Gen_Decl : Node_Id;
- Gen_Spec : Node_Id;
- Gen_Unit : Entity_Id;
-
- Is_Actual_Pack : constant Boolean :=
- Is_Internal (Defining_Entity (N));
+ -- WARNING: This routine manages Ghost and SPARK regions. Return statements
+ -- must be replaced by gotos which jump to the end of the routine in order
+ -- to restore the Ghost and SPARK modes.
- Env_Installed : Boolean := False;
- Parent_Installed : Boolean := False;
- Renaming_List : List_Id;
- Unit_Renaming : Node_Id;
- Needs_Body : Boolean;
- Inline_Now : Boolean := False;
+ procedure Analyze_Package_Instantiation (N : Node_Id) is
Has_Inline_Always : Boolean := False;
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
-
- Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
- -- Save the SPARK_Mode-related data for restore on exit
-
- Save_Style_Check : constant Boolean := Style_Check;
- -- Save style check mode for restore on exit
-
procedure Delay_Descriptors (E : Entity_Id);
-- Delay generation of subprogram descriptors for given entity
- function Might_Inline_Subp return Boolean;
+ function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean;
-- If inlining is active and the generic contains inlined subprograms,
-- we instantiate the body. This may cause superfluous instantiations,
-- but it is simpler than detecting the need for the body at the point
-- Might_Inline_Subp --
-----------------------
- function Might_Inline_Subp return Boolean is
+ function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean is
E : Entity_Id;
begin
-- Local declarations
+ Gen_Id : constant Node_Id := Name (N);
+ Is_Actual_Pack : constant Boolean :=
+ Is_Internal (Defining_Entity (N));
+ Loc : constant Source_Ptr := Sloc (N);
+
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
+
+ Saved_Style_Check : constant Boolean := Style_Check;
+ -- Save style check mode for restore on exit
+
+ Act_Decl : Node_Id;
+ Act_Decl_Name : Node_Id;
+ Act_Decl_Id : Entity_Id;
+ Act_Spec : Node_Id;
+ Act_Tree : Node_Id;
+ Env_Installed : Boolean := False;
+ Gen_Decl : Node_Id;
+ Gen_Spec : Node_Id;
+ Gen_Unit : Entity_Id;
+ Inline_Now : Boolean := False;
+ Needs_Body : Boolean;
+ Parent_Installed : Boolean := False;
+ Renaming_List : List_Id;
+ Unit_Renaming : Node_Id;
+
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
Instantiation_Node := N;
- -- Turn off style checking in instances. If the check is enabled on the
- -- generic unit, a warning in an instance would just be noise. If not
- -- enabled on the generic, then a warning in an instance is just wrong.
-
- Style_Check := False;
-
-- Case of instantiation of a generic package
if Nkind (N) = N_Package_Instantiation then
Preanalyze_Actuals (N, Act_Decl_Id);
+ -- Turn off style checking in instances. If the check is enabled on the
+ -- generic unit, a warning in an instance would just be noise. If not
+ -- enabled on the generic, then a warning in an instance is just wrong.
+ -- This must be done after analyzing the actuals, which do come from
+ -- source and are subject to style checking.
+
+ Style_Check := False;
+
Init_Env;
Env_Installed := True;
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A package instantiation is Ghost when it is subject to pragma Ghost
+ -- or the generic template is Ghost. Set the mode now to ensure that
+ -- any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
+
-- Verify that it is the name of a generic package
-- A visibility glitch: if the instance is a child unit and the generic
-- the instance.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the instance spec in case the body is instantiated at a
+ -- later pass. This preserves the original context in effect for
+ -- the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
end if;
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
if Expander_Active
and then (not Is_Child_Unit (Gen_Unit)
or else not Is_Generic_Unit (Scope (Gen_Unit)))
- and then Might_Inline_Subp
+ and then Might_Inline_Subp (Gen_Unit)
and then not Is_Actual_Pack
then
if not Back_End_Inlining
-- predefined subprograms marked Inline_Always, to minimize
-- the use of the run-time library.
- elsif Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Gen_Decl)))
+ elsif In_Predefined_Unit (Gen_Decl)
and then Configurable_Run_Time_Mode
and then Nkind (Parent (N)) /= N_Compilation_Unit
then
(Unit_Requires_Body (Gen_Unit)
or else Enclosing_Body_Present
or else Present (Corresponding_Body (Gen_Decl)))
- and then (Is_In_Main_Unit (N) or else Might_Inline_Subp)
+ and then (Is_In_Main_Unit (N)
+ or else Might_Inline_Subp (Gen_Unit))
and then not Is_Actual_Pack
and then not Inline_Now
and then (Operating_Mode = Generate_Code
Set_Defining_Identifier (N, Act_Decl_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
-
-- Check that if N is an instantiation of System.Dim_Float_IO or
-- System.Dim_Integer_IO, the formal type has a dimension system.
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Style_Check := Saved_Style_Check;
+
exception
when Instantiation_Error =>
if Parent_Installed then
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Style_Check := Saved_Style_Check;
end Analyze_Package_Instantiation;
--------------------------
-- Inline_Instance_Body --
--------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Inline_Instance_Body
(N : Node_Id;
Gen_Unit : Entity_Id;
Gen_Comp : constant Entity_Id :=
Cunit_Entity (Get_Source_Unit (Gen_Unit));
- Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
- -- Save all SPARK_Mode-related attributes as removing enclosing scopes
- -- to provide a clean environment for analysis of the inlined body will
- -- eliminate any previously set SPARK_Mode.
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK mode-related data to restore on exit. Removing
+ -- enclosing scopes to provide a clean environment for analysis of
+ -- the inlined body will eliminate any previously set SPARK_Mode.
Scope_Stack_Depth : constant Pos :=
Scope_Stack.Last - Scope_Stack.First + 1;
- Use_Clauses : array (1 .. Scope_Stack_Depth) of Node_Id;
- Instances : array (1 .. Scope_Stack_Depth) of Entity_Id;
Inner_Scopes : array (1 .. Scope_Stack_Depth) of Entity_Id;
- Curr_Scope : Entity_Id := Empty;
- List : Elist_Id;
- Num_Inner : Nat := 0;
- Num_Scopes : Nat := 0;
- N_Instances : Nat := 0;
- Removed : Boolean := False;
- S : Entity_Id;
- Vis : Boolean;
+ Instances : array (1 .. Scope_Stack_Depth) of Entity_Id;
+ Use_Clauses : array (1 .. Scope_Stack_Depth) of Node_Id;
+
+ Curr_Scope : Entity_Id := Empty;
+ List : Elist_Id;
+ N_Instances : Nat := 0;
+ Num_Inner : Nat := 0;
+ Num_Scopes : Nat := 0;
+ Removed : Boolean := False;
+ S : Entity_Id;
+ Vis : Boolean;
begin
-- Case of generic unit defined in another unit. We must remove the
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
Warnings => Save_Warnings,
- SPARK_Mode => Save_SM,
- SPARK_Mode_Pragma => Save_SMP)),
+ SPARK_Mode => Saved_SM,
+ SPARK_Mode_Pragma => Saved_SMP)),
Inlined_Body => True);
Pop_Scope;
(N : Node_Id;
Subp : Entity_Id) return Boolean
is
-
function Is_Inlined_Or_Child_Of_Inlined (E : Entity_Id) return Boolean;
-- Return True if E is an inlined subprogram, an inlined renaming or a
-- subprogram nested in an inlined subprogram. The inlining machinery
-- Analyze_Subprogram_Instantiation --
--------------------------------------
+ -- WARNING: This routine manages Ghost and SPARK regions. Return statements
+ -- must be replaced by gotos which jump to the end of the routine in order
+ -- to restore the Ghost and SPARK modes.
+
procedure Analyze_Subprogram_Instantiation
(N : Node_Id;
K : Entity_Kind)
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
-
- Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
- -- Save the SPARK_Mode-related data for restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A subprogram instantiation is Ghost when it is subject to pragma
+ -- Ghost or the generic template is Ghost. Set the mode now to ensure
+ -- that any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
+
Generate_Reference (Gen_Unit, Gen_Id);
if Nkind (Gen_Id) = N_Identifier
if Etype (Gen_Unit) = Any_Type then
Restore_Env;
- return;
+ goto Leave;
end if;
-- Verify that it is a generic subprogram of the right kind, and that
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
-
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
- end if;
-
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
Set_Has_Pragma_Inline (Act_Decl_Id, Has_Pragma_Inline (Gen_Unit));
Set_Has_Pragma_Inline (Anon_Id, Has_Pragma_Inline (Gen_Unit));
+ -- Propagate No_Return if pragma applied to generic unit. This must
+ -- be done explicitly because pragma does not appear in generic
+ -- declaration (unlike the aspect case).
+
+ if No_Return (Gen_Unit) then
+ Set_No_Return (Act_Decl_Id);
+ Set_No_Return (Anon_Id);
+ end if;
+
Set_Has_Pragma_Inline_Always
(Act_Decl_Id, Has_Pragma_Inline_Always (Gen_Unit));
Set_Has_Pragma_Inline_Always
(Anon_Id, Has_Pragma_Inline_Always (Gen_Unit));
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
+
+ if SPARK_Mode /= On then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark both the instance spec and the anonymous package in case
+ -- the body is instantiated at a later pass. This preserves the
+ -- original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
+ Set_Ignore_SPARK_Mode_Pragmas (Anon_Id);
+ end if;
+
if not Is_Intrinsic_Subprogram (Gen_Unit) then
Check_Elab_Instantiation (N);
end if;
Error_Msg_NE
("access parameter& is controlling,", N, Formal);
Error_Msg_NE
- ("\corresponding parameter of & must be "
- & "explicitly null-excluding", N, Gen_Id);
+ ("\corresponding parameter of & must be explicitly "
+ & "null-excluding", N, Gen_Id);
end if;
Next_Formal (Formal);
Env_Installed := False;
Generic_Renamings.Set_Last (0);
Generic_Renamings_HTable.Reset;
-
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
end if;
<<Leave>>
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+
exception
when Instantiation_Error =>
if Parent_Installed then
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Subprogram_Instantiation;
-------------------------
Assoc := Associated_Node (Assoc);
end loop;
- -- Follow and additional link in case the final node was rewritten.
+ -- Follow an additional link in case the final node was rewritten.
-- This can only happen with nested generic units.
if (Nkind (Assoc) = N_Identifier or else Nkind (Assoc) in N_Op)
-- An additional special case: an unconstrained type in an object
-- declaration may have been rewritten as a local subtype constrained
-- by the expression in the declaration. We need to recover the
- -- original entity which may be global.
+ -- original entity, which may be global.
if Present (Original_Node (Assoc))
and then Nkind (Parent (N)) = N_Object_Declaration
Decl : Node_Id;
Expr : Node_Id;
+ pragma Warnings (Off, Expr);
F1, F2 : Entity_Id;
Func : Entity_Id;
Op_Name : Name_Id;
(Formal_Pack : Entity_Id;
Actual_Pack : Entity_Id)
is
- E1 : Entity_Id := First_Entity (Actual_Pack);
- E2 : Entity_Id := First_Entity (Formal_Pack);
+ E1 : Entity_Id := First_Entity (Actual_Pack);
+ E2 : Entity_Id := First_Entity (Formal_Pack);
+ Prev_E1 : Entity_Id;
Expr1 : Node_Id;
Expr2 : Node_Id;
-- Start of processing for Check_Formal_Package_Instance
begin
+ Prev_E1 := E1;
while Present (E1) and then Present (E2) loop
exit when Ekind (E1) = E_Package
and then Renamed_Entity (E1) = Renamed_Entity (Actual_Pack);
if No (E1) then
return;
+ -- Entities may be declared without full declaration, such as
+ -- itypes and predefined operators (concatenation for arrays, eg).
+ -- Skip it and keep the formal entity to find a later match for it.
+
+ elsif No (Parent (E2)) and then Ekind (E1) /= Ekind (E2) then
+ E1 := Prev_E1;
+ goto Next_E;
+
-- If the formal entity comes from a formal declaration, it was
-- defaulted in the formal package, and no check is needed on it.
N_Formal_Object_Declaration,
N_Formal_Type_Declaration)
then
+ -- If the formal is a tagged type the corresponding class-wide
+ -- type has been generated as well, and it must be skipped.
+
+ if Is_Type (E2) and then Is_Tagged_Type (E2) then
+ Next_Entity (E2);
+ end if;
+
goto Next_E;
-- Ditto for defaulted formal subprograms.
end if;
<<Next_E>>
+ Prev_E1 := E1;
Next_Entity (E1);
Next_Entity (E2);
end loop;
Set_Is_Generic_Actual_Type (E, True);
Set_Is_Hidden (E, False);
- Set_Is_Potentially_Use_Visible (E,
- In_Use (Instance));
+ Set_Is_Potentially_Use_Visible (E, In_Use (Instance));
-- We constructed the generic actual type as a subtype of the
-- supplied type. This means that it normally would not inherit
(New_N, Copy_Generic_List (Aspect_Specifications (N), Parent_Id));
end if;
- if Instantiating then
+ -- If we are instantiating, we want to adjust the sloc based on the
+ -- current S_Adjustment. However, if this is the root node of a subunit,
+ -- we need to defer that adjustment to below (see "elsif Instantiating
+ -- and Was_Stub"), so it comes after Create_Instantiation_Source has
+ -- computed the adjustment.
+
+ if Instantiating
+ and then not (Nkind (N) in N_Proper_Body
+ and then Was_Originally_Stub (N))
+ then
Adjust_Instantiation_Sloc (New_N, S_Adjustment);
end if;
Set_Selector_Name (New_N,
Copy_Generic_Node (Selector_Name (N), New_N, Instantiating));
- -- For operators, we must copy the right operand
+ -- For operators, copy the operands
elsif Nkind (N) in N_Op then
- Set_Right_Opnd (New_N,
- Copy_Generic_Node (Right_Opnd (N), New_N, Instantiating));
-
- -- And for binary operators, the left operand as well
-
if Nkind (N) in N_Binary_Op then
Set_Left_Opnd (New_N,
Copy_Generic_Node (Left_Opnd (N), New_N, Instantiating));
end if;
+
+ Set_Right_Opnd (New_N,
+ Copy_Generic_Node (Right_Opnd (N), New_N, Instantiating));
end if;
-- Establish a link between an entity from the generic template and the
Copy_Generic_List (Context_Items (N), New_N));
Set_Unit (New_N,
- Copy_Generic_Node (Unit (N), New_N, False));
+ Copy_Generic_Node (Unit (N), New_N, Instantiating => False));
Set_First_Inlined_Subprogram (New_N,
Copy_Generic_Node
- (First_Inlined_Subprogram (N), New_N, False));
+ (First_Inlined_Subprogram (N), New_N, Instantiating => False));
- Set_Aux_Decls_Node (New_N,
- Copy_Generic_Node (Aux_Decls_Node (N), New_N, False));
+ Set_Aux_Decls_Node
+ (New_N,
+ Copy_Generic_Node
+ (Aux_Decls_Node (N), New_N, Instantiating => False));
-- For an assignment node, the assignment is known to be semantically
-- legal if we are instantiating the template. This avoids incorrect
elsif Nkind (N) in N_Proper_Body then
declare
Save_Adjustment : constant Sloc_Adjustment := S_Adjustment;
-
begin
if Instantiating and then Was_Originally_Stub (N) then
Create_Instantiation_Source
(Instantiation_Node,
Defining_Entity (N),
S_Adjustment);
+
+ Adjust_Instantiation_Sloc (New_N, S_Adjustment);
end if;
-- Now copy the fields of the proper body, using the new
Copy_Descendants;
- -- Restore the original adjustment factor in case changed
+ -- Restore the original adjustment factor
S_Adjustment := Save_Adjustment;
end;
-- Do not copy Comment or Ident pragmas their content is relevant to
-- the generic unit, not to the instantiating unit.
- if Nam_In (Pragma_Name (N), Name_Comment, Name_Ident) then
+ if Nam_In (Pragma_Name_Unmapped (N), Name_Comment, Name_Ident) then
New_N := Make_Null_Statement (Sloc (N));
-- Do not copy pragmas generated from aspects because the pragmas do
Gen_Body : Node_Id;
Gen_Decl : Node_Id)
is
- Act_Id : constant Entity_Id := Corresponding_Spec (Act_Body);
- Act_Unit : constant Node_Id := Unit (Cunit (Get_Source_Unit (N)));
- Gen_Id : constant Entity_Id := Corresponding_Spec (Gen_Body);
- Par : constant Entity_Id := Scope (Gen_Id);
- Gen_Unit : constant Node_Id :=
- Unit (Cunit (Get_Source_Unit (Gen_Decl)));
- Orig_Body : Node_Id := Gen_Body;
- F_Node : Node_Id;
- Body_Unit : Node_Id;
+ function In_Same_Scope (Gen_Id, Act_Id : Node_Id) return Boolean;
+ -- Check if the generic definition and the instantiation come from
+ -- a common scope, in which case the instance must be frozen after
+ -- the generic body.
- Must_Delay : Boolean;
-
- function In_Same_Enclosing_Subp return Boolean;
- -- Check whether instance and generic body are within same subprogram.
-
- function True_Sloc (N : Node_Id) return Source_Ptr;
+ function True_Sloc (N, Act_Unit : Node_Id) return Source_Ptr;
-- If the instance is nested inside a generic unit, the Sloc of the
-- instance indicates the place of the original definition, not the
-- point of the current enclosing instance. Pending a better usage of
-- origin of a node by finding the maximum sloc of any ancestor node.
-- Why is this not equivalent to Top_Level_Location ???
- ----------------------------
- -- In_Same_Enclosing_Subp --
- ----------------------------
+ -------------------
+ -- In_Same_Scope --
+ -------------------
- function In_Same_Enclosing_Subp return Boolean is
- Scop : Entity_Id;
- Subp : Entity_Id;
+ function In_Same_Scope (Gen_Id, Act_Id : Node_Id) return Boolean is
+ Act_Scop : Entity_Id := Scope (Act_Id);
+ Gen_Scop : Entity_Id := Scope (Gen_Id);
begin
- Scop := Scope (Act_Id);
- while Scop /= Standard_Standard
- and then not Is_Overloadable (Scop)
+ while Act_Scop /= Standard_Standard
+ and then Gen_Scop /= Standard_Standard
loop
- Scop := Scope (Scop);
- end loop;
-
- if Scop = Standard_Standard then
- return False;
- else
- Subp := Scop;
- end if;
-
- Scop := Scope (Gen_Id);
- while Scop /= Standard_Standard loop
- if Scop = Subp then
+ if Act_Scop = Gen_Scop then
return True;
- else
- Scop := Scope (Scop);
end if;
+
+ Act_Scop := Scope (Act_Scop);
+ Gen_Scop := Scope (Gen_Scop);
end loop;
return False;
- end In_Same_Enclosing_Subp;
+ end In_Same_Scope;
---------------
-- True_Sloc --
---------------
- function True_Sloc (N : Node_Id) return Source_Ptr is
- Res : Source_Ptr;
+ function True_Sloc (N, Act_Unit : Node_Id) return Source_Ptr is
N1 : Node_Id;
+ Res : Source_Ptr;
begin
Res := Sloc (N);
- N1 := N;
+ N1 := N;
while Present (N1) and then N1 /= Act_Unit loop
if Sloc (N1) > Res then
Res := Sloc (N1);
return Res;
end True_Sloc;
+ Act_Id : constant Entity_Id := Corresponding_Spec (Act_Body);
+ Act_Unit : constant Node_Id := Unit (Cunit (Get_Source_Unit (N)));
+ Gen_Id : constant Entity_Id := Corresponding_Spec (Gen_Body);
+ Par : constant Entity_Id := Scope (Gen_Id);
+ Gen_Unit : constant Node_Id :=
+ Unit (Cunit (Get_Source_Unit (Gen_Decl)));
+
+ Body_Unit : Node_Id;
+ F_Node : Node_Id;
+ Must_Delay : Boolean;
+ Orig_Body : Node_Id := Gen_Body;
+
-- Start of processing for Install_Body
begin
Must_Delay :=
(Gen_Unit = Act_Unit
- and then (Nkind_In (Gen_Unit, N_Package_Declaration,
- N_Generic_Package_Declaration)
+ and then (Nkind_In (Gen_Unit, N_Generic_Package_Declaration,
+ N_Package_Declaration)
or else (Gen_Unit = Body_Unit
- and then True_Sloc (N) < Sloc (Orig_Body)))
- and then Is_In_Main_Unit (Gen_Unit)
- and then (Scope (Act_Id) = Scope (Gen_Id)
- or else In_Same_Enclosing_Subp));
+ and then True_Sloc (N, Act_Unit)
+ < Sloc (Orig_Body)))
+ and then Is_In_Main_Unit (Original_Node (Gen_Unit))
+ and then In_Same_Scope (Gen_Id, Act_Id));
-- If this is an early instantiation, the freeze node is placed after
-- the generic body. Otherwise, if the generic appears in an instance,
begin
case Nkind (Original_Node (F)) is
- when N_Formal_Object_Declaration |
- N_Formal_Type_Declaration =>
+ when N_Formal_Object_Declaration
+ | N_Formal_Type_Declaration
+ =>
Formal_Ent := Defining_Identifier (F);
while Chars (Act) /= Chars (Formal_Ent) loop
Next_Entity (Act);
end loop;
- when N_Formal_Subprogram_Declaration |
- N_Formal_Package_Declaration |
- N_Package_Declaration |
- N_Generic_Package_Declaration =>
+ when N_Formal_Package_Declaration
+ | N_Formal_Subprogram_Declaration
+ | N_Generic_Package_Declaration
+ | N_Package_Declaration
+ =>
Formal_Ent := Defining_Entity (F);
while Chars (Act) /= Chars (Formal_Ent) loop
Kind : constant Node_Kind := Nkind (Original_Node (N));
begin
case Kind is
- when N_Formal_Object_Declaration =>
+ when N_Formal_Object_Declaration =>
return Defining_Identifier (N);
- when N_Formal_Type_Declaration =>
+ when N_Formal_Type_Declaration =>
return Defining_Identifier (N);
when N_Formal_Subprogram_Declaration =>
return Defining_Unit_Name (Specification (N));
- when N_Formal_Package_Declaration =>
+ when N_Formal_Package_Declaration =>
return Defining_Identifier (Original_Node (N));
- when N_Generic_Package_Declaration =>
+ when N_Generic_Package_Declaration =>
return Defining_Identifier (Original_Node (N));
-- All other declarations are introduced by semantic analysis and
-- Instantiate_Package_Body --
------------------------------
+ -- WARNING: This routine manages Ghost and SPARK regions. Return statements
+ -- must be replaced by gotos which jump to the end of the routine in order
+ -- to restore the Ghost and SPARK modes.
+
procedure Instantiate_Package_Body
(Body_Info : Pending_Body_Info;
Inlined_Body : Boolean := False;
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
+ Act_Spec : constant Node_Id := Specification (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
-
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Spec : constant Node_Id := Specification (Act_Decl);
- Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec);
-
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- Save_Style_Check : constant Boolean := Style_Check;
-
- Act_Body : Node_Id;
- Act_Body_Id : Entity_Id;
- Act_Body_Name : Node_Id;
- Gen_Body : Node_Id;
- Gen_Body_Id : Node_Id;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
-
- Parent_Installed : Boolean := False;
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
- Vis_Prims_List : Elist_Id := No_Elist;
- -- List of primitives made temporarily visible in the instantiation
- -- to match the visibility of the formal type
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_Style_Check : constant Boolean := Style_Check;
procedure Check_Initialized_Types;
-- In a generic package body, an entity of a generic private type may
end loop;
end Check_Initialized_Types;
+ -- Local variables
+
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
+
+ Act_Body : Node_Id;
+ Act_Body_Id : Entity_Id;
+ Act_Body_Name : Node_Id;
+ Gen_Body : Node_Id;
+ Gen_Body_Id : Node_Id;
+ Par_Ent : Entity_Id := Empty;
+ Par_Vis : Boolean := False;
+ Parent_Installed : Boolean := False;
+
+ Vis_Prims_List : Elist_Id := No_Elist;
+ -- List of primitives made temporarily visible in the instantiation
+ -- to match the visibility of the formal type.
+
-- Start of processing for Instantiate_Package_Body
begin
return;
end if;
+ -- The package being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
Opt.Ada_Version := Body_Info.Version;
Opt.Ada_Version_Pragma := Body_Info.Version_Pragma;
Restore_Warnings (Body_Info.Warnings);
- Opt.SPARK_Mode := Body_Info.SPARK_Mode;
- Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma;
+
+ -- Install the SPARK mode which applies to the package body
+
+ Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
if No (Gen_Body_Id) then
if not Unit_Requires_Body (Defining_Entity (Gen_Decl))
and then Body_Optional
then
- return;
+ goto Leave;
else
Load_Parent_Of_Generic
(Inst_Node, Specification (Gen_Decl), Body_Optional);
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+ -- instance.
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
-- interested in finding possible runtime errors.
if not CodePeer_Mode
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Gen_Decl)))
+ and then In_Predefined_Unit (Gen_Decl)
then
Analyze (Act_Body, Suppress => All_Checks);
else
end if;
Restore_Env;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- Style_Check := Save_Style_Check;
-- If we have no body, and the unit requires a body, then complain. This
-- complaint is suppressed if we have detected other errors (since a
-- was already detected, since this can cause blowups.
else
- return;
+ goto Leave;
end if;
-- Case of package that does not need a body
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Style_Check := Saved_Style_Check;
end Instantiate_Package_Body;
---------------------------------
-- Instantiate_Subprogram_Body --
---------------------------------
+ -- WARNING: This routine manages Ghost and SPARK regions. Return statements
+ -- must be replaced by gotos which jump to the end of the routine in order
+ -- to restore the Ghost and SPARK modes.
+
procedure Instantiate_Subprogram_Body
(Body_Info : Pending_Body_Info;
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Decl_Id : constant Entity_Id :=
- Defining_Unit_Name (Specification (Act_Decl));
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
- Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
+
Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
return;
end if;
+ -- The subprogram being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
Opt.Ada_Version := Body_Info.Version;
Opt.Ada_Version_Pragma := Body_Info.Version_Pragma;
Restore_Warnings (Body_Info.Warnings);
- Opt.SPARK_Mode := Body_Info.SPARK_Mode;
- Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma;
+
+ -- Install the SPARK mode which applies to the subprogram body
+
+ Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
if No (Gen_Body_Id) then
Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit));
Set_Convention (Act_Decl_Id, Convention (Gen_Unit));
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
-- For other cases, compile the body
if Expander_Active
and then Operating_Mode = Generate_Code
then
- Error_Msg_N
- ("missing proper body for instantiation", Gen_Body);
+ Error_Msg_N ("missing proper body for instantiation", Gen_Body);
end if;
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
end if;
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+ -- instance.
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
end if;
Restore_Env;
- Ignore_Pragma_SPARK_Mode := Saved_IPSM;
- Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
-- Body not found. Error was emitted already. If there were no previous
and then Nkind (Parent (Inst_Node)) /= N_Compilation_Unit
then
if Body_Optional then
- return;
+ goto Leave;
elsif Ekind (Act_Decl_Id) = E_Procedure then
Act_Body :=
Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
- New_Copy_List
- (Parameter_Specifications (Parent (Act_Decl_Id)))),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List (
- Make_Raise_Program_Error (Loc,
- Reason =>
- PE_Access_Before_Elaboration))));
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
+ Parameter_Specifications =>
+ New_Copy_List
+ (Parameter_Specifications (Parent (Act_Decl_Id)))),
+
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Make_Raise_Program_Error (Loc,
+ Reason => PE_Access_Before_Elaboration))));
else
Ret_Expr :=
Make_Subprogram_Body (Loc,
Specification =>
Make_Function_Specification (Loc,
- Defining_Unit_Name =>
+ Defining_Unit_Name =>
Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
+ Parameter_Specifications =>
New_Copy_List
(Parameter_Specifications (Parent (Act_Decl_Id))),
Result_Definition =>
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List
- (Make_Simple_Return_Statement (Loc, Ret_Expr))));
+ Statements => New_List (
+ Make_Simple_Return_Statement (Loc, Ret_Expr))));
end if;
Pack_Body :=
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Style_Check := Saved_Style_Check;
end Instantiate_Subprogram_Body;
----------------------
Analyzed_Formal : Node_Id;
Actual_Decls : List_Id) return List_Id
is
- Gen_T : constant Entity_Id := Defining_Identifier (Formal);
A_Gen_T : constant Entity_Id :=
Defining_Identifier (Analyzed_Formal);
- Ancestor : Entity_Id := Empty;
Def : constant Node_Id := Formal_Type_Definition (Formal);
+ Gen_T : constant Entity_Id := Defining_Identifier (Formal);
Act_T : Entity_Id;
+ Ancestor : Entity_Id := Empty;
Decl_Node : Node_Id;
Decl_Nodes : List_Id;
Loc : Source_Ptr;
when N_Access_To_Object_Definition =>
Validate_Access_Type_Instance;
- when N_Access_Function_Definition |
- N_Access_Procedure_Definition =>
+ when N_Access_Function_Definition
+ | N_Access_Procedure_Definition
+ =>
Validate_Access_Subprogram_Instance;
- when N_Record_Definition =>
+ when N_Record_Definition =>
Validate_Interface_Type_Instance;
- when N_Derived_Type_Definition =>
+ when N_Derived_Type_Definition =>
Validate_Derived_Interface_Type_Instance;
when others =>
raise Program_Error;
-
end case;
end if;
return
Current_Unit = Cunit (Main_Unit)
or else Current_Unit = Library_Unit (Cunit (Main_Unit))
- or else (Present (Library_Unit (Current_Unit))
+ or else (Present (Current_Unit)
+ and then Present (Library_Unit (Current_Unit))
and then Is_In_Main_Unit (Library_Unit (Current_Unit)));
end Is_In_Main_Unit;
-- package, in which case the usual generic rule applies.
declare
- Exp_Status : Boolean := True;
- Scop : Entity_Id;
+ Exp_Status : Boolean := True;
+ Scop : Entity_Id;
begin
-- Loop through scopes looking for generic package
-- Package instance
- if
- Nkind (Node (Decl)) = N_Package_Instantiation
+ if Nkind (Node (Decl)) = N_Package_Instantiation
then
Instantiate_Package_Body
(Info, Body_Optional => True);
-- these result in the corresponding pragmas,
-- inserted after the subprogram declaration.
-- They must be skipped as well when retrieving
- -- the desired spec. A direct link would be
- -- more robust ???
+ -- the desired spec. Some of them may have been
+ -- rewritten as null statements.
+ -- A direct link would be more robust ???
declare
Decl : Node_Id :=
(Specification (Info.Act_Decl))));
begin
while Nkind_In (Decl,
- N_Subprogram_Renaming_Declaration, N_Pragma)
+ N_Null_Statement,
+ N_Pragma,
+ N_Subprogram_Renaming_Declaration)
loop
Decl := Prev (Decl);
end loop;
Cur : Entity_Id := Empty;
-- Current homograph of the instance name
- Vis : Boolean;
+ Vis : Boolean := False;
-- Saved visibility status of the current homograph
begin
then
Copy_Dimensions (N2, N);
end if;
-
end Set_Global_Type;
------------------
if Is_Global (Entity (Original_Node (N2))) then
N2 := Original_Node (N2);
Set_Associated_Node (N, N2);
- Set_Global_Type (N, N2);
+ Set_Global_Type (N, N2);
-- Renaming is local, and will be resolved in instance
if Is_Global (Entity (Parent (N2))) then
Change_Selected_Component_To_Expanded_Name (Parent (N));
Set_Associated_Node (Parent (N), Parent (N2));
- Set_Global_Type (Parent (N), Parent (N2));
+ Set_Global_Type (Parent (N), Parent (N2));
Save_Entity_Descendants (N);
-- If this is a reference to the current generic entity, replace
if Is_Global (Entity (Name (Parent (N2)))) then
Change_Selected_Component_To_Expanded_Name (Parent (N));
Set_Associated_Node (Parent (N), Name (Parent (N2)));
- Set_Global_Type (Parent (N), Name (Parent (N2)));
+ Set_Global_Type (Parent (N), Name (Parent (N2)));
Save_Entity_Descendants (N);
else
when N_Unary_Op =>
Save_Global_Descendant (Union_Id (Right_Opnd (N)));
- when N_Expanded_Name |
- N_Selected_Component =>
+ when N_Expanded_Name
+ | N_Selected_Component
+ =>
Save_Global_Descendant (Union_Id (Prefix (N)));
Save_Global_Descendant (Union_Id (Selector_Name (N)));
- when N_Identifier |
- N_Character_Literal |
- N_Operator_Symbol =>
+ when N_Character_Literal
+ | N_Identifier
+ | N_Operator_Symbol
+ =>
null;
when others =>
-- The node did not undergo a transformation
if Nkind (N) = Nkind (Get_Associated_Node (N)) then
+ declare
+ Aux_N2 : constant Node_Id := Get_Associated_Node (N);
+ Orig_N2_Parent : constant Node_Id :=
+ Original_Node (Parent (Aux_N2));
+ begin
+ -- The parent of this identifier is a selected component
+ -- which denotes a named number that was constant folded.
+ -- Preserve the original name for ASIS and link the parent
+ -- with its expanded name. The constant folding will be
+ -- repeated in the instance.
+
+ if Nkind (Parent (N)) = N_Selected_Component
+ and then Nkind_In (Parent (Aux_N2), N_Integer_Literal,
+ N_Real_Literal)
+ and then Is_Entity_Name (Orig_N2_Parent)
+ and then Ekind (Entity (Orig_N2_Parent)) in Named_Kind
+ and then Is_Global (Entity (Orig_N2_Parent))
+ then
+ N2 := Aux_N2;
+ Set_Associated_Node
+ (Parent (N), Original_Node (Parent (N2)));
- -- If this is a discriminant reference, always save it. It is
- -- used in the instance to find the corresponding discriminant
- -- positionally rather than by name.
+ -- Common case
- Set_Original_Discriminant
- (N, Original_Discriminant (Get_Associated_Node (N)));
- Reset_Entity (N);
+ else
+ -- If this is a discriminant reference, always save it.
+ -- It is used in the instance to find the corresponding
+ -- discriminant positionally rather than by name.
+
+ Set_Original_Discriminant
+ (N, Original_Discriminant (Get_Associated_Node (N)));
+ end if;
+
+ Reset_Entity (N);
+ end;
-- The analysis of the generic copy transformed the identifier
-- into another construct. Propagate the changes to the template.
-- Set_Instance_Env --
----------------------
+ -- WARNING: This routine manages SPARK regions
+
procedure Set_Instance_Env
(Gen_Unit : Entity_Id;
Act_Unit : Entity_Id)
is
- Assertion_Status : constant Boolean := Assertions_Enabled;
- Save_SPARK_Mode : constant SPARK_Mode_Type := SPARK_Mode;
- Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma;
+ Saved_AE : constant Boolean := Assertions_Enabled;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK mode-related data because utilizing the configuration
+ -- values of pragmas and switches will eliminate any previously set
+ -- SPARK_Mode.
begin
-- Regardless of the current mode, predefined units are analyzed in the
-- to predefined units. Nothing needs to be done for non-internal units.
-- These are always analyzed in the current mode.
- if Is_Internal_File_Name
- (Fname => Unit_File_Name (Get_Source_Unit (Gen_Unit)),
- Renamings_Included => True)
- then
+ if In_Internal_Unit (Gen_Unit) then
Set_Opt_Config_Switches (True, Current_Sem_Unit = Main_Unit);
-- In Ada2012 we may want to enable assertions in an instance of a
-- as is already the case for some numeric libraries.
if Ada_Version >= Ada_2012 then
- Assertions_Enabled := Assertion_Status;
+ Assertions_Enabled := Saved_AE;
end if;
- -- SPARK_Mode for an instance is the one applicable at the point of
+ -- Reinstall the SPARK_Mode which was in effect at the point of
-- instantiation.
- SPARK_Mode := Save_SPARK_Mode;
- SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
+ Install_SPARK_Mode (Saved_SM, Saved_SMP);
end if;
Current_Instantiated_Parent :=
end loop;
case Attr_Id is
- when Attribute_Adjacent | Attribute_Ceiling | Attribute_Copy_Sign |
- Attribute_Floor | Attribute_Fraction | Attribute_Machine |
- Attribute_Model | Attribute_Remainder | Attribute_Rounding |
- Attribute_Unbiased_Rounding =>
+ when Attribute_Adjacent
+ | Attribute_Ceiling
+ | Attribute_Copy_Sign
+ | Attribute_Floor
+ | Attribute_Fraction
+ | Attribute_Machine
+ | Attribute_Model
+ | Attribute_Remainder
+ | Attribute_Rounding
+ | Attribute_Unbiased_Rounding
+ =>
OK := Is_Fun
and then Num_F = 1
and then Is_Floating_Point_Type (T);
- when Attribute_Image | Attribute_Pred | Attribute_Succ |
- Attribute_Value | Attribute_Wide_Image |
- Attribute_Wide_Value =>
- OK := (Is_Fun and then Num_F = 1 and then Is_Scalar_Type (T));
+ when Attribute_Image
+ | Attribute_Pred
+ | Attribute_Succ
+ | Attribute_Value
+ | Attribute_Wide_Image
+ | Attribute_Wide_Value
+ =>
+ OK := Is_Fun and then Num_F = 1 and then Is_Scalar_Type (T);
- when Attribute_Max | Attribute_Min =>
- OK := (Is_Fun and then Num_F = 2 and then Is_Scalar_Type (T));
+ when Attribute_Max
+ | Attribute_Min
+ =>
+ OK := Is_Fun and then Num_F = 2 and then Is_Scalar_Type (T);
when Attribute_Input =>
OK := (Is_Fun and then Num_F = 1);
- when Attribute_Output | Attribute_Read | Attribute_Write =>
- OK := (not Is_Fun and then Num_F = 2);
+ when Attribute_Output
+ | Attribute_Read
+ | Attribute_Write
+ =>
+ OK := not Is_Fun and then Num_F = 2;
when others =>
OK := False;
projects / gcc.git / blobdiff