===================================================================
@@ -444,12 +444,19 @@
-- Analyze_Entry_Or_Subprogram_Body_Contract --
-----------------------------------------------
+ -- 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 Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
Items : constant Node_Id := Contract (Body_Id);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
- Mode : SPARK_Mode_Type;
+ 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
+
begin
-- When a subprogram body declaration is illegal, its defining entity is
-- left unanalyzed. There is nothing left to do in this case because the
@@ -473,7 +480,7 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
+ Set_SPARK_Mode (Body_Id);
-- Ensure that the contract cases or postconditions mention 'Result or
-- define a post-state.
@@ -499,7 +506,7 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic subprogram body now that
-- the contract has been analyzed.
@@ -523,6 +530,10 @@
-- Analyze_Entry_Or_Subprogram_Contract --
------------------------------------------
+ -- 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 Analyze_Entry_Or_Subprogram_Contract
(Subp_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
@@ -530,6 +541,10 @@
Items : constant Node_Id := Contract (Subp_Id);
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ 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
+
Skip_Assert_Exprs : constant Boolean :=
Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
and then not ASIS_Mode
@@ -537,7 +552,6 @@
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
@@ -557,7 +571,7 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+ Set_SPARK_Mode (Subp_Id);
-- All subprograms carry a contract, but for some it is not significant
-- and should not be processed.
@@ -667,7 +681,7 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic subprogram now that the
-- contract has been analyzed.
@@ -683,22 +697,29 @@
-- Analyze_Object_Contract --
-----------------------------
+ -- 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 Analyze_Object_Contract
(Obj_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
is
- Obj_Typ : constant Entity_Id := Etype (Obj_Id);
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Items : Node_Id;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Ref_Elmt : Elmt_Id;
- Restore_Mode : Boolean := False;
- Seen : Boolean := False;
+ Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+ 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
+
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Ref_Elmt : Elmt_Id;
+ Seen : Boolean := False;
+
begin
-- The loop parameter in an element iterator over a formal container
-- is declared with an object declaration, but no contracts apply.
@@ -728,8 +749,7 @@
if Is_Single_Concurrent_Object (Obj_Id)
and then Present (SPARK_Pragma (Obj_Id))
then
- Restore_Mode := True;
- Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+ Set_SPARK_Mode (Obj_Id);
end if;
-- Constant-related checks
@@ -929,15 +949,17 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- if Restore_Mode then
- Restore_SPARK_Mode (Mode);
- end if;
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Object_Contract;
-----------------------------------
-- Analyze_Package_Body_Contract --
-----------------------------------
+ -- 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 Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
@@ -945,7 +967,11 @@
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
Items : constant Node_Id := Contract (Body_Id);
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
- Mode : SPARK_Mode_Type;
+
+ 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
+
Ref_State : Node_Id;
begin
@@ -964,7 +990,7 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related package body.
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
+ Set_SPARK_Mode (Body_Id);
Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
@@ -978,7 +1004,7 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic package body now that the
-- contract has been analyzed.
@@ -994,12 +1020,20 @@
-- Analyze_Package_Contract --
------------------------------
+ -- 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 Analyze_Package_Contract (Pack_Id : Entity_Id) is
Items : constant Node_Id := Contract (Pack_Id);
Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
+
+ 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
+
Init : Node_Id := Empty;
Init_Cond : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
@@ -1019,7 +1053,7 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related package.
- Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+ Set_SPARK_Mode (Pack_Id);
if Present (Items) then
@@ -1066,7 +1100,7 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic package now that the
-- contract has been analyzed.
@@ -1204,11 +1238,19 @@
-- Analyze_Task_Contract --
---------------------------
+ -- 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 Analyze_Task_Contract (Task_Id : Entity_Id) is
Items : constant Node_Id := Contract (Task_Id);
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
+ 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
+
+ Prag : Node_Id;
+
begin
-- Do not analyze a contract multiple times
@@ -1225,7 +1267,7 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related task unit.
- Save_SPARK_Mode_And_Set (Task_Id, Mode);
+ Set_SPARK_Mode (Task_Id);
-- Analyze Global first, as Depends may mention items classified in the
-- global categorization.
@@ -1248,7 +1290,7 @@
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Task_Contract;
-------------------------------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -82,7 +82,8 @@
-- Ghost mode.
procedure Expand (N : Node_Id) is
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
begin
-- If we were analyzing a default expression (or other spec expression)
@@ -98,7 +99,7 @@
-- Establish the Ghost mode of the context to ensure that any generated
-- nodes during expansion are marked as Ghost.
- Set_Ghost_Mode (N, Mode);
+ Set_Ghost_Mode (N);
-- The GNATprove_Mode flag indicates that a light expansion for formal
-- verification should be used. This expansion is never done inside
@@ -529,7 +530,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Expand;
---------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -7193,10 +7193,11 @@
Def_Id : constant Entity_Id := Entity (N);
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
- Result : Boolean := False;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+ Result : Boolean := False;
+
-- Start of processing for Freeze_Type
begin
@@ -7204,8 +7205,7 @@
-- now to ensure that any nodes generated during freezing are properly
-- marked as Ghost.
- Set_Ghost_Mode (Def_Id, Mode);
- Mode_Set := True;
+ Set_Ghost_Mode (Def_Id);
-- Process any remote access-to-class-wide types designating the type
-- being frozen.
@@ -7548,17 +7548,13 @@
Build_Invariant_Procedure_Body (Def_Id);
end if;
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ Restore_Ghost_Mode (Saved_GM);
return Result;
exception
when RE_Not_Available =>
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ Restore_Ghost_Mode (Saved_GM);
return False;
end Freeze_Type;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -4396,6 +4396,9 @@
Name_TSD : constant Name_Id :=
New_External_Name (Tname, 'B', Suffix_Index => -1);
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
AI : Elmt_Id;
AI_Tag_Elmt : Elmt_Id;
AI_Tag_Comp : Elmt_Id;
@@ -4408,7 +4411,6 @@
ITable : Node_Id;
I_Depth : Nat := 0;
Iface_Table_Node : Node_Id;
- Mode : Ghost_Mode_Type;
Name_ITable : Name_Id;
Nb_Predef_Prims : Nat := 0;
Nb_Prim : Nat := 0;
@@ -4436,7 +4438,7 @@
-- the mode now to ensure that any nodes generated during dispatch table
-- creation are properly marked as Ghost.
- Set_Ghost_Mode (Typ, Mode);
+ Set_Ghost_Mode (Typ);
-- Handle cases in which there is no need to build the dispatch table
@@ -6242,7 +6244,7 @@
Register_CG_Node (Typ);
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
return Result;
end Make_DT;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -1529,11 +1529,13 @@
Loc : constant Source_Ptr := Sloc (Typ);
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
- Mode : Ghost_Mode_Type;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
@@ -1582,7 +1584,7 @@
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the DIC procedure is properly marked as Ghost.
- Set_Ghost_Mode (Work_Typ, Mode);
+ Set_Ghost_Mode (Work_Typ);
-- The working type must be either define a DIC pragma of its own or
-- inherit one from a parent type.
@@ -1762,7 +1764,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Body;
-------------------------------------
@@ -1776,9 +1778,11 @@
procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
Loc : constant Source_Ptr := Sloc (Typ);
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
- Mode : Ghost_Mode_Type;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Typ_Decl : Node_Id;
@@ -1835,7 +1839,7 @@
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the DIC procedure is properly marked as Ghost.
- Set_Ghost_Mode (Work_Typ, Mode);
+ Set_Ghost_Mode (Work_Typ);
-- The type must be either subject to a DIC pragma or inherit one from a
-- parent type.
@@ -1959,7 +1963,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Declaration;
------------------------------------
@@ -2889,8 +2893,10 @@
-- Local variables
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Dummy : Entity_Id;
- Mode : Ghost_Mode_Type;
Priv_Item : Node_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
@@ -2944,7 +2950,7 @@
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the invariant procedure is properly marked as Ghost.
- Set_Ghost_Mode (Work_Typ, Mode);
+ Set_Ghost_Mode (Work_Typ);
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent types or interfaces, or be an array or record
@@ -3228,7 +3234,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Body;
-------------------------------------------
@@ -3245,7 +3251,9 @@
is
Loc : constant Source_Ptr := Sloc (Typ);
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Nam : Name_Id;
@@ -3295,7 +3303,7 @@
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the invariant procedure is properly marked as Ghost.
- Set_Ghost_Mode (Work_Typ, Mode);
+ Set_Ghost_Mode (Work_Typ);
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent or interface types, or be an array or record
@@ -3452,7 +3460,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Declaration;
--------------------------
@@ -9288,9 +9296,11 @@
is
Loc : constant Source_Ptr := Sloc (Expr);
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Call : Node_Id;
Func_Id : Entity_Id;
- Mode : Ghost_Mode_Type;
begin
pragma Assert (Present (Predicate_Function (Typ)));
@@ -9298,7 +9308,7 @@
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the call is properly marked as Ghost.
- Set_Ghost_Mode (Typ, Mode);
+ Set_Ghost_Mode (Typ);
-- Call special membership version if requested and available
@@ -9315,7 +9325,8 @@
Name => New_Occurrence_Of (Func_Id, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
+
return Call;
end Make_Predicate_Call;
===================================================================
@@ -5107,7 +5107,8 @@
-- Local variables
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
-- Start of processing for Freeze_Entity
@@ -5116,7 +5117,7 @@
-- now to ensure that any nodes generated during freezing are properly
-- flagged as Ghost.
- Set_Ghost_Mode (E, Mode);
+ Set_Ghost_Mode (E);
-- We are going to test for various reasons why this entity need not be
-- frozen here, but in the case of an Itype that's defined within a
@@ -6723,7 +6724,8 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
+
return Result;
end Freeze_Entity;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 2014-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- --
@@ -1099,17 +1099,10 @@
-- Mark_And_Set_Ghost_Assignment --
-----------------------------------
- procedure Mark_And_Set_Ghost_Assignment
- (N : Node_Id;
- Mode : out Ghost_Mode_Type)
- is
+ procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is
Id : Entity_Id;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- An assignment statement becomes Ghost when its target denotes a Ghost
-- object. Install the Ghost mode of the target.
@@ -1134,17 +1127,12 @@
procedure Mark_And_Set_Ghost_Body
(N : Node_Id;
- Spec_Id : Entity_Id;
- Mode : out Ghost_Mode_Type)
+ Spec_Id : Entity_Id)
is
Body_Id : constant Entity_Id := Defining_Entity (N);
Policy : Name_Id := No_Name;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- A body becomes Ghost when it is subject to aspect or pragma Ghost
if Is_Subject_To_Ghost (N) then
@@ -1193,17 +1181,12 @@
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
- Prev_Id : Entity_Id;
- Mode : out Ghost_Mode_Type)
+ Prev_Id : Entity_Id)
is
Compl_Id : constant Entity_Id := Defining_Entity (N);
Policy : Name_Id := No_Name;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- A completion elaborated in a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
@@ -1243,18 +1226,11 @@
-- Mark_And_Set_Ghost_Declaration --
------------------------------------
- procedure Mark_And_Set_Ghost_Declaration
- (N : Node_Id;
- Mode : out Ghost_Mode_Type)
- is
+ procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is
Par_Id : Entity_Id;
Policy : Name_Id := No_Name;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- A declaration becomes Ghost when it is subject to aspect or pragma
-- Ghost.
@@ -1309,16 +1285,11 @@
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
- Gen_Id : Entity_Id;
- Mode : out Ghost_Mode_Type)
+ Gen_Id : Entity_Id)
is
Policy : Name_Id := No_Name;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- An instantiation becomes Ghost when it is subject to pragma Ghost
if Is_Subject_To_Ghost (N) then
@@ -1355,17 +1326,10 @@
-- Mark_And_Set_Ghost_Procedure_Call --
---------------------------------------
- procedure Mark_And_Set_Ghost_Procedure_Call
- (N : Node_Id;
- Mode : out Ghost_Mode_Type)
- is
+ procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is
Id : Entity_Id;
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- A procedure call becomes Ghost when the procedure being invoked is
-- Ghost. Install the Ghost mode of the procedure.
@@ -1695,10 +1659,7 @@
-- Set_Ghost_Mode --
--------------------
- procedure Set_Ghost_Mode
- (N : Node_Or_Entity_Id;
- Mode : out Ghost_Mode_Type)
- is
+ procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-- Install the Ghost mode of entity Id
@@ -1724,10 +1685,6 @@
-- Start of processing for Set_Ghost_Mode
begin
- -- Save the previous Ghost mode in effect
-
- Mode := Ghost_Mode;
-
-- The Ghost mode of an assignment statement depends on the Ghost mode
-- of the target.
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 2014-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- --
@@ -101,21 +101,17 @@
procedure Lock;
-- Lock internal tables before calling backend
- procedure Mark_And_Set_Ghost_Assignment
- (N : Node_Id;
- Mode : out Ghost_Mode_Type);
+ procedure Mark_And_Set_Ghost_Assignment (N : Node_Id);
-- Mark assignment statement N as Ghost when:
--
-- * The left hand side denotes a Ghost entity
--
- -- Install the Ghost mode of the assignment statement. Mode is the Ghost
- -- mode in effect prior to processing the assignment. This routine starts
+ -- Install the Ghost mode of the assignment statement. This routine starts
-- a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
procedure Mark_And_Set_Ghost_Body
(N : Node_Id;
- Spec_Id : Entity_Id;
- Mode : out Ghost_Mode_Type);
+ Spec_Id : Entity_Id);
-- Mark package or subprogram body N as Ghost when:
--
-- * The body is subject to pragma Ghost
@@ -125,14 +121,12 @@
--
-- * The body appears within a Ghost region
--
- -- Install the Ghost mode of the body. Mode is the Ghost mode prior to
- -- processing the body. This routine starts a Ghost region and must be
- -- used in conjunction with Restore_Ghost_Mode.
+ -- Install the Ghost mode of the body. This routine starts a Ghost region
+ -- and must be used in conjunction with Restore_Ghost_Mode.
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
- Prev_Id : Entity_Id;
- Mode : out Ghost_Mode_Type);
+ Prev_Id : Entity_Id);
-- Mark completion N of a deferred constant or private type [extension]
-- Ghost when:
--
@@ -140,13 +134,10 @@
--
-- * The completion appears within a Ghost region
--
- -- Install the Ghost mode of the completion. Mode is the Ghost mode prior
- -- to processing the completion. This routine starts a Ghost region and
- -- must be used in conjunction with Restore_Ghost_Mode.
+ -- Install the Ghost mode of the completion. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
- procedure Mark_And_Set_Ghost_Declaration
- (N : Node_Id;
- Mode : out Ghost_Mode_Type);
+ procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
-- Mark declaration N as Ghost when:
--
-- * The declaration is subject to pragma Ghost
@@ -156,14 +147,12 @@
--
-- * The declaration appears within a Ghost region
--
- -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior
- -- to processing the declaration. This routine starts a Ghost region and
- -- must be used in conjunction with Restore_Ghost_Mode.
+ -- Install the Ghost mode of the declaration. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
- Gen_Id : Entity_Id;
- Mode : out Ghost_Mode_Type);
+ Gen_Id : Entity_Id);
-- Mark instantiation N as Ghost when:
--
-- * The instantiation is subject to pragma Ghost
@@ -172,20 +161,16 @@
--
-- * The instantiation appears within a Ghost region
--
- -- Install the Ghost mode of the instantiation. Mode is the Ghost mode
- -- prior to processing the instantiation. This routine starts a Ghost
+ -- Install the Ghost mode of the instantiation. This routine starts a Ghost
-- region and must be used in conjunction with Restore_Ghost_Mode.
- procedure Mark_And_Set_Ghost_Procedure_Call
- (N : Node_Id;
- Mode : out Ghost_Mode_Type);
+ procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
-- Mark procedure call N as Ghost when:
--
-- * The procedure being invoked is a Ghost entity
--
- -- Install the Ghost mode of the procedure call. Mode is the Ghost mode
- -- prior to processing the procedure call. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- Install the Ghost mode of the procedure call. This routine starts a
+ -- Ghost region and must be used in conjunction with Restore_Ghost_Mode.
procedure Mark_Ghost_Clause (N : Node_Id);
-- Mark use package, use type, or with clause N as Ghost when:
@@ -220,12 +205,9 @@
-- region denoted by Mode. This routine must be used in conjunction
-- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
- procedure Set_Ghost_Mode
- (N : Node_Or_Entity_Id;
- Mode : out Ghost_Mode_Type);
- -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior
- -- to processing the node. This routine starts a Ghost region and must be
- -- used in conjunction with Restore_Ghost_Mode.
+ procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
+ -- Install the Ghost mode of arbitrary node N. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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- --
@@ -811,7 +811,6 @@
Filler : Boolean;
Loading : Boolean;
OA_Setting : Character;
- SPARK_Mode_Pragma : Node_Id;
end record;
-- The following representation clause ensures that the above record
@@ -841,10 +840,9 @@
Filler at 61 range 0 .. 7;
OA_Setting at 62 range 0 .. 7;
Loading at 63 range 0 .. 7;
- SPARK_Mode_Pragma at 64 range 0 .. 31;
end record;
- for Unit_Record'Size use 68 * 8;
+ for Unit_Record'Size use 64 * 8;
-- This ensures that we did not leave out any fields
package Units is new Table.Table (
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -227,8 +227,7 @@
Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False),
Unit_Name => Spec_Name,
Version => 0,
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
Set_Comes_From_Source_Default (Save_CS);
Set_Error_Posted (Cunit_Entity);
@@ -334,8 +333,7 @@
Unit_File_Name => Fname,
Unit_Name => No_Unit_Name,
Version => Version,
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
end if;
end Load_Main_Source;
@@ -700,8 +698,7 @@
Unit_File_Name => Fname,
Unit_Name => Uname_Actual,
Version => Source_Checksum (Src_Ind),
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
-- Parse the new unit
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -95,8 +95,7 @@
Serial_Number => 0,
Version => 0,
Error_Location => No_Location,
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
end Add_Preprocessing_Dependency;
------------------------------
@@ -153,8 +152,7 @@
Serial_Number => 0,
Version => 0,
Error_Location => No_Location,
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
-- Parse system.ads so that the checksum is set right. Style checks are
-- not applied. The Ekind is set to ensure that this reference is always
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -864,6 +864,10 @@
-- Load_RTU --
--------------
+ -- 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 Load_RTU
(U_Id : RTU_Id;
Id : RE_Id := RE_Null;
@@ -926,7 +930,10 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save Ghost and SPARK mode-related data to restore on exit
-- Start of processing for Load_RTU
@@ -940,6 +947,7 @@
-- Provide a clean environment for the unit
Install_Ghost_Mode (None);
+ Install_SPARK_Mode (None, Empty);
-- Note if secondary stack is used
@@ -1042,7 +1050,8 @@
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
- Restore_Ghost_Mode (Save_Ghost_Mode);
+ Restore_Ghost_Mode (Save_GM);
+ Restore_SPARK_Mode (Save_SM, Save_SMP);
end Load_RTU;
--------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -102,8 +102,8 @@
-- Ghost mode.
procedure Analyze (N : Node_Id) is
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
begin
Debug_A_Entry ("analyzing ", N);
@@ -120,8 +120,7 @@
-- marked as Ghost.
if Is_Declaration (N) then
- Mark_And_Set_Ghost_Declaration (N, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Declaration (N);
end if;
-- Otherwise processing depends on the node kind
@@ -762,9 +761,7 @@
Expand_SPARK_Potential_Renaming (N);
end if;
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ Restore_Ghost_Mode (Saved_GM);
end Analyze;
-- Version with check(s) suppressed
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -2058,6 +2058,10 @@
-- context before analyzing the proper body itself. On exit, we remove only
-- the explicit context of the subunit.
+ -- 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 Analyze_Subunit (N : Node_Id) is
Lib_Unit : constant Node_Id := Library_Unit (N);
Par_Unit : constant Entity_Id := Current_Scope;
@@ -2290,6 +2294,12 @@
Pop_Scope;
end Remove_Scope;
+ 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
+ -- eclosing scopes and contexts to provide a clean environment for the
+ -- context of the subunit will eliminate any previously set SPARK_Mode.
+
-- Start of processing for Analyze_Subunit
begin
@@ -2386,6 +2396,12 @@
end if;
Generate_Parent_References (Unit (N), Par_Unit);
+
+ -- Reinstall the SPARK_Mode which was in effect prior to any scope and
+ -- context manipulations.
+
+ Install_SPARK_Mode (Saved_SM, Saved_SMP);
+
Analyze (Proper_Body (Unit (N)));
Remove_Context (N);
===================================================================
@@ -3598,49 +3598,17 @@
-- 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
@@ -3662,7 +3630,7 @@
-- 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
@@ -3691,9 +3659,36 @@
-- 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
-- to match the visibility of the formal type
@@ -3771,8 +3766,7 @@
-- 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
@@ -4049,7 +4043,7 @@
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
@@ -4098,7 +4092,8 @@
(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
@@ -4466,15 +4461,11 @@
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;
+ 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;
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
-
exception
when Instantiation_Error =>
if Parent_Installed then
@@ -4485,20 +4476,20 @@
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;
@@ -4509,27 +4500,28 @@
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
-- complete context of the current unit to install that of the generic.
@@ -4672,8 +4664,8 @@
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;
@@ -4812,7 +4804,6 @@
(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
@@ -4882,9 +4873,9 @@
-- 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;
@@ -5130,16 +5121,13 @@
-- Local variables
- Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
- -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance 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
- 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;
-
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
@@ -5180,8 +5168,7 @@
-- 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);
@@ -5446,14 +5433,10 @@
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;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
-
exception
when Instantiation_Error =>
if Parent_Installed then
@@ -5464,13 +5447,9 @@
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;
-------------------------
@@ -10847,9 +10826,9 @@
-- 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;
@@ -10865,9 +10844,9 @@
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
@@ -10939,15 +10918,18 @@
-- 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;
@@ -10970,7 +10952,7 @@
-- 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);
@@ -10984,9 +10966,11 @@
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
-- Do not look for parent of generic body if none is required.
@@ -11264,19 +11248,19 @@
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;
@@ -11292,16 +11276,20 @@
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;
@@ -11324,7 +11312,7 @@
-- 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);
@@ -11338,9 +11326,11 @@
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
-- For imported generic subprogram, no body to compile, complete
@@ -11575,9 +11565,9 @@
<<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;
----------------------
@@ -15413,13 +15403,18 @@
-- 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
@@ -15440,14 +15435,13 @@
-- 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 :=
===================================================================
@@ -8566,7 +8566,8 @@
-- Local variables
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
-- Start of processing for Build_Predicate_Functions
@@ -8583,7 +8584,7 @@
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the predicate functions are properly marked as Ghost.
- Set_Ghost_Mode (Typ, Mode);
+ Set_Ghost_Mode (Typ);
-- Prepare to construct predicate expression
@@ -8937,7 +8938,7 @@
end;
end if;
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Predicate_Functions;
------------------------------------------
@@ -8953,16 +8954,18 @@
is
Loc : constant Source_Ptr := Sloc (Typ);
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Func_Decl : Node_Id;
Func_Id : Entity_Id;
- Mode : Ghost_Mode_Type;
Spec : Node_Id;
begin
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the predicate functions are properly marked as Ghost.
- Set_Ghost_Mode (Typ, Mode);
+ Set_Ghost_Mode (Typ);
Func_Id :=
Make_Defining_Identifier (Loc,
@@ -8996,7 +8999,7 @@
Insert_After (Parent (Typ), Func_Decl);
Analyze (Func_Decl);
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
return Func_Decl;
end Build_Predicate_Function_Declaration;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -3688,8 +3688,9 @@
-- Local variables
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Related_Id : Entity_Id;
-- Start of processing for Analyze_Object_Declaration
@@ -3760,8 +3761,7 @@
-- The object declaration is Ghost when it completes a deferred Ghost
-- constant.
- Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Completion (N, Prev_Entity);
Constant_Redeclaration (Id, N, T);
@@ -4700,9 +4700,7 @@
Check_No_Hidden_State (Id);
end if;
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Object_Declaration;
---------------------------
@@ -19858,15 +19856,16 @@
-- Local variables
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+
Full_Indic : Node_Id;
Full_Parent : Entity_Id;
- Mode : Ghost_Mode_Type;
Priv_Parent : Entity_Id;
-- Start of processing for Process_Full_View
begin
- Mark_And_Set_Ghost_Completion (N, Priv_T, Mode);
+ Mark_And_Set_Ghost_Completion (N, Priv_T);
-- First some sanity checks that must be done after semantic
-- decoration of the full view and thus cannot be placed with other
@@ -20519,7 +20518,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Process_Full_View;
-----------------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -284,7 +284,8 @@
-- Local variables
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
-- Start of processing for Analyze_Assignment
@@ -310,7 +311,7 @@
Current_Assignment := Empty;
end if;
- Mark_And_Set_Ghost_Assignment (N, Mode);
+ Mark_And_Set_Ghost_Assignment (N);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
@@ -939,7 +940,7 @@
Analyze_Dimension (N);
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
-- If the right-hand side contains target names, expansion has been
-- disabled to prevent expansion that might move target names out of
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -1553,10 +1553,13 @@
Actuals : constant List_Id := Parameter_Associations (N);
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
- Actual : Node_Id;
- Mode : Ghost_Mode_Type;
- New_N : Node_Id;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
+ Actual : Node_Id;
+ New_N : Node_Id;
+
-- Start of processing for Analyze_Procedure_Call
begin
@@ -1598,7 +1601,7 @@
-- Set the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Mark_And_Set_Ghost_Procedure_Call (N, Mode);
+ Mark_And_Set_Ghost_Procedure_Call (N);
-- Otherwise analyze the parameters
@@ -1793,7 +1796,7 @@
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Procedure_Call;
------------------------------
@@ -3314,9 +3317,10 @@
-- Local variables
- Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
- 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;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
-- Start of processing for Analyze_Subprogram_Body_Helper
@@ -3368,8 +3372,7 @@
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Body (N, Spec_Id);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id));
@@ -3414,8 +3417,7 @@
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Body (N, Spec_Id);
else
Spec_Id := Find_Corresponding_Spec (N);
@@ -3425,8 +3427,7 @@
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Body (N, Spec_Id);
-- In GNATprove mode, if the body has no previous spec, create
-- one so that the inlining machinery can operate properly.
@@ -3527,8 +3528,7 @@
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
- Mode_Set := True;
+ Mark_And_Set_Ghost_Body (N, Spec_Id);
end if;
end if;
@@ -4447,11 +4447,8 @@
end if;
<<Leave>>
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
-
- if Mode_Set then
- Restore_Ghost_Mode (Mode);
- end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Subprogram_Body_Helper;
------------------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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- --
@@ -539,12 +539,14 @@
-- Local variables
- Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save the Ghost and SPARK mode-related data to restore on exit
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
- Mode : Ghost_Mode_Type;
New_N : Node_Id;
Pack_Decl : Node_Id;
Spec_Id : Entity_Id;
@@ -647,7 +649,7 @@
-- the mode now to ensure that any nodes generated during analysis and
-- expansion are properly flagged as ignored Ghost.
- Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mark_And_Set_Ghost_Body (N, Spec_Id);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Style.Check_Identifier (Body_Id, Spec_Id);
@@ -941,9 +943,8 @@
end if;
end if;
- Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
-
- Restore_Ghost_Mode (Mode);
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Package_Body_Helper;
---------------------------------
===================================================================
@@ -1937,8 +1937,11 @@
-- Check_Elab_Calls --
----------------------
+ -- WARNING: This routine manages SPARK regions
+
procedure Check_Elab_Calls is
- Save_SPARK_Mode : SPARK_Mode_Type;
+ Saved_SM : SPARK_Mode_Type;
+ Saved_SMP : Node_Id;
begin
-- If expansion is disabled, do not generate any checks, unless we
@@ -1966,10 +1969,11 @@
From_Elab_Code := Delay_Check.Table (J).From_Elab_Code;
In_Task_Activation := Delay_Check.Table (J).In_Task_Activation;
+ Saved_SM := SPARK_Mode;
+ Saved_SMP := SPARK_Mode_Pragma;
+
-- Set appropriate value of SPARK_Mode
- Save_SPARK_Mode := SPARK_Mode;
-
if Delay_Check.Table (J).From_SPARK_Code then
SPARK_Mode := On;
end if;
@@ -1980,7 +1984,7 @@
Outer_Scope => Delay_Check.Table (J).Outer_Scope,
Orig_Ent => Delay_Check.Table (J).Orig_Ent);
- SPARK_Mode := Save_SPARK_Mode;
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
Pop_Scope;
end loop;
===================================================================
@@ -472,8 +472,10 @@
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
CCase : Node_Id;
- Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
@@ -490,7 +492,7 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N, Mode);
+ Set_Ghost_Mode (N);
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
@@ -537,7 +539,8 @@
end if;
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Mode);
+
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
@@ -2672,7 +2675,8 @@
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
- Mode : Ghost_Mode_Type;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
begin
-- Do not analyze the pragma multiple times
@@ -2686,7 +2690,7 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N, Mode);
+ Set_Ghost_Mode (N);
-- The expression is preanalyzed because it has not been moved to its
-- final place yet. A direct analysis may generate side effects and this
@@ -2695,7 +2699,7 @@
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
@@ -12662,10 +12666,12 @@
-- restore the Ghost mode.
when Pragma_Check => Check : declare
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Cname : Name_Id;
Eloc : Source_Ptr;
Expr : Node_Id;
- Mode : Ghost_Mode_Type;
Str : Node_Id;
begin
@@ -12673,7 +12679,7 @@
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are marked as Ghost.
- Set_Ghost_Mode (N, Mode);
+ Set_Ghost_Mode (N);
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
@@ -12857,7 +12863,7 @@
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Check;
--------------------------
@@ -24031,8 +24037,10 @@
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the Ghost mode to restore on exit
+
Errors : Nat;
- Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
@@ -24049,7 +24057,7 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N, Mode);
+ Set_Ghost_Mode (N);
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
@@ -24120,7 +24128,7 @@
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
===================================================================
@@ -11694,6 +11694,16 @@
end loop;
end Install_Generic_Formals;
+ ------------------------
+ -- Install_SPARK_Mode --
+ ------------------------
+
+ procedure Install_SPARK_Mode (Mode : SPARK_Mode_Type; Prag : Node_Id) is
+ begin
+ SPARK_Mode := Mode;
+ SPARK_Mode_Pragma := Prag;
+ end Install_SPARK_Mode;
+
-----------------------------
-- Is_Actual_Out_Parameter --
-----------------------------
@@ -19830,9 +19840,13 @@
-- Restore_SPARK_Mode --
------------------------
- procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type) is
+ procedure Restore_SPARK_Mode
+ (Mode : SPARK_Mode_Type;
+ Prag : Node_Id)
+ is
begin
- SPARK_Mode := Mode;
+ SPARK_Mode := Mode;
+ SPARK_Mode_Pragma := Prag;
end Restore_SPARK_Mode;
--------------------------------
@@ -20156,28 +20170,23 @@
end if;
end Same_Value;
- -----------------------------
- -- Save_SPARK_Mode_And_Set --
- -----------------------------
+ --------------------
+ -- Set_SPARK_Mode --
+ --------------------
- procedure Save_SPARK_Mode_And_Set
- (Context : Entity_Id;
- Mode : out SPARK_Mode_Type)
- is
+ procedure Set_SPARK_Mode (Context : Entity_Id) is
begin
- -- Save the current mode in effect
-
- Mode := SPARK_Mode;
-
-- Do not consider illegal or partially decorated constructs
if Ekind (Context) = E_Void or else Error_Posted (Context) then
null;
elsif Present (SPARK_Pragma (Context)) then
- SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context));
+ Install_SPARK_Mode
+ (Mode => Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context)),
+ Prag => SPARK_Pragma (Context));
end if;
- end Save_SPARK_Mode_And_Set;
+ end Set_SPARK_Mode;
-------------------------
-- Scalar_Part_Present --
===================================================================
@@ -1331,6 +1331,9 @@
-- Install both the generic formal parameters and the formal parameters of
-- generic subprogram Subp_Id into visibility.
+ procedure Install_SPARK_Mode (Mode : SPARK_Mode_Type; Prag : Node_Id);
+ -- Establish the SPARK_Mode and SPARK_Mode_Pragma currently in effect
+
function Is_Actual_Out_Parameter (N : Node_Id) return Boolean;
-- Determines if N is an actual parameter of out mode in a subprogram call
@@ -2209,9 +2212,11 @@
procedure Reset_Analyzed_Flags (N : Node_Id);
-- Reset the Analyzed flags in all nodes of the tree whose root is N
- procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type);
- -- Set the current SPARK_Mode to whatever Mode denotes. This routime must
- -- be used in tandem with Save_SPARK_Mode_And_Set.
+ procedure Restore_SPARK_Mode
+ (Mode : SPARK_Mode_Type;
+ Prag : Node_Id);
+ -- Set the current SPARK_Mode to Mode and SPARK_Mode_Pragma to Prag. This
+ -- routine must be used in tandem with Set_SPARK_Mode.
function Returns_Unconstrained_Type (Subp : Entity_Id) return Boolean;
-- Return true if Subp is a function that returns an unconstrained type
@@ -2269,13 +2274,6 @@
-- A result of False does not necessarily mean they have different values,
-- just that it is not possible to determine they have the same value.
- procedure Save_SPARK_Mode_And_Set
- (Context : Entity_Id;
- Mode : out SPARK_Mode_Type);
- -- Save the current SPARK_Mode in effect in Mode. Establish the SPARK_Mode
- -- (if any) of a package or a subprogram denoted by Context. This routine
- -- must be used in tandem with Restore_SPARK_Mode.
-
function Scalar_Part_Present (T : Entity_Id) return Boolean;
-- Tests if type T can be determined at compile time to have at least one
-- scalar part in the sense of the Valid_Scalars attribute. Returns True if
@@ -2371,6 +2369,11 @@
-- value from T2 to T1. It does NOT copy the RM_Size field, which must be
-- separately set if this is required to be copied also.
+ procedure Set_SPARK_Mode (Context : Entity_Id);
+ -- Establish the SPARK_Mode and SPARK_Mode_Pragma (if any) of a package or
+ -- a subprogram denoted by Context. This routine must be used in tandem
+ -- with Restore_SPARK_Mode.
+
function Scope_Is_Transient return Boolean;
-- True if the current scope is transient