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));
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
-- 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);
Set_Defining_Identifier (Decl, Id);
end if;
- Append (Decl, Assoc);
+ Append (Decl, Assoc_List);
if No (Found_Assoc) then
Default :=
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;
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,
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 =>
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;
Set_Ekind (Id, E_Generic_Package);
Set_Etype (Id, Standard_Void_Type);
+ -- Set SPARK_Mode from context
+
+ 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.
-- Analyze_Package_Instantiation --
-----------------------------------
- -- WARNING: This routine manages Ghost regions. Return statements must be
- -- replaced by gotos which jump to the end of the routine and restore the
- -- Ghost mode.
+ -- 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_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));
-
- Env_Installed : Boolean := False;
- Parent_Installed : Boolean := False;
- Renaming_List : List_Id;
- Unit_Renaming : Node_Id;
- Needs_Body : Boolean;
- Inline_Now : Boolean := False;
Has_Inline_Always : Boolean := False;
- Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
- -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance 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
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ 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
-- any nodes generated during analysis and expansion are marked as
-- Ghost.
- Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
-- Verify that it is the name of a generic package
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
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
-
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- 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 =>
Restore_Env;
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
-
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- 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;
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 regions. Return statements must be
- -- replaced by gotos which jump to the end of the routine and restore the
- -- Ghost mode.
+ -- 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;
-- Local variables
- Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
- -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance 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
-
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ 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
-- that any nodes generated during analysis and expansion are marked as
-- Ghost.
- Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit);
Generate_Reference (Gen_Unit, Gen_Id);
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
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
-
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- 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 =>
Restore_Env;
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
-
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ 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;
(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;
-- Instantiate_Package_Body --
------------------------------
- -- WARNING: This routine manages Ghost regions. Return statements must be
- -- replaced by gotos which jump to the end of the routine and restore the
- -- Ghost mode.
+ -- 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;
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
Loc : constant Source_Ptr := Sloc (Inst_Node);
- Save_ISMP : constant Boolean :=
+ Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
- Save_Style_Check : constant Boolean := Style_Check;
+ Saved_Style_Check : constant Boolean := Style_Check;
procedure Check_Initialized_Types;
-- In a generic package body, an entity of a generic private type may
-- Local variables
- Act_Body : Node_Id;
- Act_Body_Id : Entity_Id;
- Act_Body_Name : Node_Id;
- Gen_Body : Node_Id;
- Gen_Body_Id : Node_Id;
- Mode : Ghost_Mode_Type;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
-
+ 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;
-- the mode now to ensure that any nodes generated during instantiation
-- are properly marked as Ghost.
- Set_Ghost_Mode (Act_Decl_Id, Mode);
+ Set_Ghost_Mode (Act_Decl_Id);
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
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
-- 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
Expander_Mode_Restore;
<<Leave>>
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
- Style_Check := Save_Style_Check;
-
- Restore_Ghost_Mode (Mode);
+ 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 regions. Return statements must be
- -- replaced by gotos which jump to the end of the routine and restore the
- -- Ghost mode.
+ -- 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;
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
- Saved_ISMP : constant Boolean :=
- Ignore_SPARK_Mode_Pragmas_In_Instance;
- Saved_Style_Check : constant Boolean := Style_Check;
+ 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;
Act_Body : Node_Id;
Act_Body_Id : Entity_Id;
Gen_Body : Node_Id;
Gen_Body_Id : Node_Id;
- Mode : Ghost_Mode_Type;
Pack_Body : Node_Id;
Par_Ent : Entity_Id := Empty;
Par_Vis : Boolean := False;
-- the mode now to ensure that any nodes generated during instantiation
-- are properly marked as Ghost.
- Set_Ghost_Mode (Act_Decl_Id, Mode);
+ Set_Ghost_Mode (Act_Decl_Id);
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
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
<<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;
-
- Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
----------------------
Cur : Entity_Id := Empty;
-- Current homograph of the instance name
- Vis : Boolean;
+ Vis : Boolean := False;
-- Saved visibility status of the current homograph
begin
-- 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 :=
projects / gcc.git / blobdiff