+2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
+ Add a warning about SPARK mode management. The routine now
+ saves and restores both the mode and associated pragma.
+ (Analyze_Entry_Or_Subprogram_Contract): Add a warning about
+ SPARK mode management. The routine now saves and restores both
+ the mode and associated pragma.
+ (Analyze_Object_Contract):
+ Add a warning about SPARK mode management. The routine
+ now saves and restores both the mode and associated pragma.
+ (Analyze_Package_Body_Contract): Add a warning about SPARK mode
+ management. The routine now saves and restores both the mode
+ and associated pragma. (Analyze_Package_Contract): Add a warning
+ about SPARK mode management. The routine now saves and restores
+ both the mode and associated pragma.
+ (Analyze_Task_Contract):
+ Add a warning about SPARK mode management. The routine now saves
+ and restores both the mode and associated pragma.
+ * expander.adb (Expand): Change the way the Ghost mode is saved
+ and restored.
+ * exp_ch3.adb (Freeze_Type): Change the way the Ghost mode is
+ saved and restored.
+ * exp_disp.adb (Make_DT): Change the way the Ghost mode is saved
+ and restored.
+ * exp_util.adb (Build_DIC_Procedure_Body):
+ Change the way the Ghost mode is saved and restored.
+ (Build_DIC_Procedure_Declaration): Change the way the Ghost
+ mode is saved and restored.
+ (Build_Invariant_Procedure_Body):
+ Change the way the Ghost mode is saved and restored.
+ (Build_Invariant_Procedure_Declaration): Change the way the Ghost
+ mode is saved and restored.
+ (Make_Predicate_Call): Change the
+ way the Ghost mode is saved and restored.
+ * freeze.adb (Freeze_Entity): Change the way the Ghost mode is
+ saved and restored.
+ * ghost.adb (Mark_And_Set_Ghost_Assignment): Remove parameter Mode
+ and its assignment.
+ (Mark_And_Set_Ghost_Body): Remove parameter
+ Mode and its assignment.
+ (Mark_And_Set_Ghost_Completion):
+ Remove parameter Mode and its assignment.
+ (Mark_And_Set_Ghost_Declaration): Remove parameter Mode and its
+ assignment.
+ (Mark_And_Set_Ghost_Instantiation): Remove parameter
+ Mode and its assignment.
+ (Mark_And_Set_Ghost_Procedure_Call):
+ Remove parameter Mode and its assignment.
+ (Set_Ghost_Mode):
+ Remove parameter Mode and its assignment.
+ * ghost.ads (Mark_And_Set_Ghost_Assignment): Remove parameter Mode
+ and update the comment on usage.
+ (Mark_And_Set_Ghost_Body):
+ Remove parameter Mode and update the comment on usage.
+ (Mark_And_Set_Ghost_Completion): Remove parameter Mode and
+ update the comment on usage.
+ (Mark_And_Set_Ghost_Declaration):
+ Remove parameter Mode and update the comment on usage.
+ (Mark_And_Set_Ghost_Instantiation): Remove parameter Mode and
+ update the comment on usage.
+ (Mark_And_Set_Ghost_Procedure_Call):
+ Remove parameter Mode and update the comment on usage.
+ (Set_Ghost_Mode): Remove parameter Mode and update the comment
+ on usage.
+ * lib.ads Remove obsolete fields SPARK_Mode_Pragma from various
+ types.
+ * lib-load.adb (Create_Dummy_Package_Unit): Remove the assignment
+ of obsolete field SPARK_Mode_Pragma.
+ (Load_Main_Source): Remove
+ the assignment of obsolete field SPARK_Mode_Pragma.
+ (Load_Unit): Remove the assignment of obsolete field SPARK_Mode_Pragma.
+ * lib-writ.adb (Add_Preprocessing_Dependency): Remove
+ the assignment of obsolete field SPARK_Mode_Pragma.
+ (Ensure_System_Dependency): Remove the assignment of obsolete
+ field SPARK_Mode_Pragma.
+ * rtsfind.adb (Load_RTU): Add a warning about Ghost and SPARK
+ mode management. Change the way Ghost and SPARK modes are saved
+ and restored.
+ * sem.adb (Analyze): Change the way the Ghost mode is saved
+ and restored.
+ * sem_ch3.adb (Analyze_Object_Declaration): Change the way the
+ Ghost mode is saved and restored.
+ (Process_Full_View): Change
+ the way the Ghost mode is saved and restored.
+ * sem_ch5.adb (Analyze_Assignment): Change the way the Ghost
+ mode is saved and restored.
+ * sem_ch6.adb (Analyze_Procedure_Call): Change the way the Ghost
+ mode is saved and restored.
+ (Analyze_Subprogram_Body_Helper):
+ Change the way the Ghost mode is saved and restored.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Change the way the
+ Ghost mode is saved and restored.
+ * sem_ch10.adb (Analyze_Subunit): Add a warning about SPARK mode
+ management. Save the SPARK mode-related data prior to any changes
+ to the scope stack and contexts. The mode is then reinstalled
+ before the subunit is analyzed in order to restore the original
+ view of the subunit.
+ * sem_ch12.adb (Analyze_Package_Instantiation): Update the
+ warning on region management. Change the way the Ghost and
+ SPARK modes are saved and restored.
+ (Inline_Instance_Body):
+ Add a warning about SPARK mode management. Code clean up.
+ (Analyze_Subprogram_Instantiation): Update the warning on region
+ management. Change the way the Ghost and SPARK modes are saved
+ and restored.
+ (Instantiate_Package_Body): Update the warning
+ on region management. Change the way the Ghost and SPARK modes
+ are saved and restored.
+ (Instantiate_Subprogram_Body): Update
+ the warning on region management. Change the way the Ghost and
+ SPARK modes are saved and restored.
+ (Set_Instance_Env): Add a
+ warning about SPARK mode management. Change the way SPARK mode
+ is saved and restored.
+ * sem_ch13.adb (Build_Predicate_Functions):
+ Change the way the Ghost mode is saved and restored.
+ (Build_Predicate_Function_Declaration): Change the way the Ghost
+ mode is saved and restored.
+ * sem_elab.adb (Check_Elab_Calls): Add a warning about SPARK
+ mode management. Change the way SPARK mode is saved and restored.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
+ Change the way the Ghost mode is saved and restored.
+ (Analyze_Initial_Condition_In_Decl_Part): Change the way
+ the Ghost mode is saved and restored.
+ (Analyze_Pragma):
+ Change the way the Ghost mode is saved and restored.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Change the way the
+ Ghost mode is saved and restored.
+ * sem_util.adb (Install_SPARK_Mode): New routine.
+ (Restore_SPARK_Mode): New routine.
+ (Save_SPARK_Mode_And_Set): Removed.
+ (Set_SPARK_Mode): New routine.
+ * sem_util.ads (Install_SPARK_Mode): New routine.
+ (Restore_SPARK_Mode): New routine.
+ (Save_SPARK_Mode_And_Set): Removed.
+ (Set_SPARK_Mode): New routine.
+
2017-04-25 Ed Schonberg <schonberg@adacore.com>
* sem_util.adb, sem_util.ads (From_Nested_Package): New predicate
-- 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
-- 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.
-- 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.
-- 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)
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
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
-- 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.
-- 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.
-- 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
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
-- 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)
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
-- 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);
-- 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.
-- 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;
-- 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
-- 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.
-- 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
-- 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.
-- 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;
-------------------------------------------------
-- --
-- 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- --
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
-- 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.
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;
-- --
-- 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- --
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;
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;
-- 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
Register_CG_Node (Typ);
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
return Result;
end Make_DT;
-- --
-- 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- --
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;
-- 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.
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Body;
-------------------------------------
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;
-- 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.
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Declaration;
------------------------------------
-- 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;
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Body;
-------------------------------------------
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;
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Declaration;
--------------------------
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)));
-- 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
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;
-- --
-- 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- --
-- 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)
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Expand;
---------------------------
-- 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
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
+
return Result;
end Freeze_Entity;
-- --
-- B o d y --
-- --
--- Copyright (C) 2014-2016, Free Software Foundation, Inc. --
+-- 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- --
-- 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.
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
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)).
-- 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.
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
-- 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.
-- 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
-- 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.
-- --
-- S p e c --
-- --
--- Copyright (C) 2014-2016, Free Software Foundation, Inc. --
+-- 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- --
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
--
-- * 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:
--
--
-- * 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
--
-- * 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
--
-- * 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:
-- 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
-- --
-- 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- --
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);
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;
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
-- --
-- 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- --
Serial_Number => 0,
Version => 0,
Error_Location => No_Location,
- OA_Setting => 'O',
- SPARK_Mode_Pragma => Empty);
+ OA_Setting => 'O');
end Add_Preprocessing_Dependency;
------------------------------
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
-- --
-- S p e c --
-- --
--- 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- --
Filler : Boolean;
Loading : Boolean;
OA_Setting : Character;
- SPARK_Mode_Pragma : Node_Id;
end record;
-- The following representation clause ensures that the above record
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 (
-- --
-- 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- --
-- 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;
-- 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
-- Provide a clean environment for the unit
Install_Ghost_Mode (None);
+ Install_SPARK_Mode (None, Empty);
-- Note if secondary stack is used
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;
--------------------
-- --
-- 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- --
-- 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);
-- 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
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
-- --
-- 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- --
-- 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;
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
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);
-- 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
(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);
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;
-------------------------
-- 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
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;
----------------------
-- 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
-- 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 :=
-- 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
-- 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
end;
end if;
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Build_Predicate_Functions;
------------------------------------------
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,
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;
-- --
-- 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- --
-- 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
-- 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);
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;
---------------------------
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Process_Full_View;
-----------------------------------
-- --
-- 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- --
-- 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
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
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
-- --
-- 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- --
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
-- 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
end if;
<<Leave>>
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Procedure_Call;
------------------------------
-- 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
-- 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));
-- 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);
-- 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.
-- 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;
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;
------------------------------------
-- --
-- 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- --
-- 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;
-- 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);
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;
---------------------------------
-- 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
From_Elab_Code := Delay_Check.Table (J).From_Elab_Code;
In_Task_Activation := Delay_Check.Table (J).In_Task_Activation;
- -- Set appropriate value of SPARK_Mode
+ Saved_SM := SPARK_Mode;
+ Saved_SMP := SPARK_Mode_Pragma;
- Save_SPARK_Mode := SPARK_Mode;
+ -- Set appropriate value of SPARK_Mode
if Delay_Check.Table (J).From_SPARK_Code then
SPARK_Mode := On;
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;
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
-- 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
end if;
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Mode);
+
+ Restore_Ghost_Mode (Saved_GM);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
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
-- 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
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;
--------------------------------------
-- 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
-- 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);
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- Restore_Ghost_Mode (Mode);
+ Restore_Ghost_Mode (Saved_GM);
end Check;
--------------------------
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
-- 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.
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;
------------------------------------------
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 --
-----------------------------
-- 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;
--------------------------------
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 --
-- 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
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
-- 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
-- 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
projects / gcc.git / commitdiff