OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Add a warning about SPARK mode management.

Browse Source 
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.

From-SVN: r247230
This commit is contained in:
Hristian Kirtchev 2017-04-25 13:30:56 +00:00 committed by Arnaud Charlet
parent e1691d7e60
commit f9a8f91057
25 changed files with 588 additions and 423 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

138
gcc/ada/ChangeLog
View File

@ -1,3 +1,141 @@
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

106
gcc/ada/contracts.adb
View File

@ -444,11 +444,18 @@ package body Contracts is
-- 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
@ -473,7 +480,7 @@ package body Contracts 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.
@ -499,7 +506,7 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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 @@ package body Contracts is
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 @@ package body Contracts is
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
@ -557,7 +571,7 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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,21 +697,28 @@ package body Contracts is
-- 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
@ -728,8 +749,7 @@ package body Contracts is
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 @@ package body Contracts is
-- 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 @@ package body Contracts is
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 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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,10 +1238,18 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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 @@ package body Contracts is
-- 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;
-------------------------------------------------

20
gcc/ada/exp_ch3.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -7193,9 +7193,10 @@ package body Exp_Ch3 is
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
@ -7204,8 +7205,7 @@ package body Exp_Ch3 is
-- 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 @@ package body Exp_Ch3 is
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;

10
gcc/ada/exp_disp.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -4396,6 +4396,9 @@ package body Exp_Disp is
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 @@ package body Exp_Disp is
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 @@ package body Exp_Disp is
-- 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 @@ package body Exp_Disp is
Register_CG_Node (Typ);
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
return Result;
end Make_DT;

43
gcc/ada/exp_util.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -1529,11 +1529,13 @@ package body Exp_Util 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;
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 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Body;
-------------------------------------
@ -1776,9 +1778,11 @@ package body Exp_Util is
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 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Build_DIC_Procedure_Declaration;
------------------------------------
@ -2889,8 +2893,10 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Body;
-------------------------------------------
@ -3245,7 +3251,9 @@ package body Exp_Util is
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 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Build_Invariant_Procedure_Declaration;
--------------------------
@ -9288,9 +9296,11 @@ package body Exp_Util is
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 @@ package body Exp_Util is
-- 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 @@ package body Exp_Util is
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;

9
gcc/ada/expander.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -82,7 +82,8 @@ package body Expander is
-- 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 @@ package body Expander is
-- 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 @@ package body Expander is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Expand;
---------------------------

8
gcc/ada/freeze.adb
View File

@ -5107,7 +5107,8 @@ package body Freeze is
-- 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 @@ package body Freeze is
-- 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 @@ package body Freeze is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
return Result;
end Freeze_Entity;

59
gcc/ada/ghost.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -1099,17 +1099,10 @@ package body Ghost is
-- 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 @@ package body Ghost is
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 @@ package body Ghost is
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 @@ package body Ghost is
-- 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 @@ package body Ghost is
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 @@ package body Ghost is
-- 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 @@ package body Ghost is
-- 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 @@ package body Ghost is
-- 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.

58
gcc/ada/ghost.ads
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -101,21 +101,17 @@ package Ghost is
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 @@ package Ghost is
--
-- * 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 @@ package Ghost is
--
-- * 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 @@ package Ghost is
--
-- * 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 @@ package Ghost is
--
-- * 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 @@ package Ghost is
-- 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

11
gcc/ada/lib-load.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -227,8 +227,7 @@ package body Lib.Load is
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 @@ package body Lib.Load is
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 @@ package body Lib.Load is
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

8
gcc/ada/lib-writ.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -95,8 +95,7 @@ package body Lib.Writ is
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 @@ package body Lib.Writ is
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
gcc/ada/lib.ads
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -811,7 +811,6 @@ private
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 @@ private
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 (

15
gcc/ada/rtsfind.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -864,6 +864,10 @@ package body Rtsfind is
-- 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 @@ package body Rtsfind is
-- 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 @@ package body Rtsfind is
-- 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 @@ package body Rtsfind is
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;
--------------------

13
gcc/ada/sem.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -102,8 +102,8 @@ package body Sem is
-- 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 @@ package body Sem is
-- 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 @@ package body Sem is
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

18
gcc/ada/sem_ch10.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -2058,6 +2058,10 @@ package body Sem_Ch10 is
-- 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 @@ package body Sem_Ch10 is
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 @@ package body Sem_Ch10 is
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);

282
gcc/ada/sem_ch12.adb
View File

@ -3598,49 +3598,17 @@ package body Sem_Ch12 is
-- 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 @@ package body Sem_Ch12 is
-- 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,8 +3659,35 @@ package body Sem_Ch12 is
-- 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
@ -3771,8 +3766,7 @@ package body Sem_Ch12 is
-- 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 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
(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,14 +4461,10 @@ package body Sem_Ch12 is
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 =>
@ -4485,20 +4476,20 @@ package body Sem_Ch12 is
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,26 +4500,27 @@ package body Sem_Ch12 is
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
@ -4672,8 +4664,8 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
(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 @@ package body Sem_Ch12 is
-- 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,15 +5121,12 @@ package body Sem_Ch12 is
-- 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
@ -5180,8 +5168,7 @@ package body Sem_Ch12 is
-- 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,13 +5433,9 @@ package body Sem_Ch12 is
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 =>
@ -5464,13 +5447,9 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
-- 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 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
-- 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 @@ package body Sem_Ch12 is
-- 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,8 +10966,10 @@ package body Sem_Ch12 is
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
@ -11264,19 +11248,19 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
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 @@ package body Sem_Ch12 is
-- 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,8 +11326,10 @@ package body Sem_Ch12 is
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
@ -11575,9 +11565,9 @@ package body Sem_Ch12 is
<<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 @@ package body Sem_Ch12 is
-- 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 @@ package body Sem_Ch12 is
-- 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 :=

15
gcc/ada/sem_ch13.adb
View File

@ -8566,7 +8566,8 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
end;
end if;
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Build_Predicate_Functions;
------------------------------------------
@ -8953,16 +8954,18 @@ package body Sem_Ch13 is
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 @@ package body Sem_Ch13 is
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;

21
gcc/ada/sem_ch3.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -3688,8 +3688,9 @@ package body Sem_Ch3 is
-- 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 @@ package body Sem_Ch3 is
-- 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 @@ package body Sem_Ch3 is
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 @@ package body Sem_Ch3 is
-- 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 @@ package body Sem_Ch3 is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Process_Full_View;
-----------------------------------

9
gcc/ada/sem_ch5.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -284,7 +284,8 @@ package body Sem_Ch5 is
-- 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 @@ package body Sem_Ch5 is
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 @@ package body Sem_Ch5 is
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

41
gcc/ada/sem_ch6.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -1553,9 +1553,12 @@ package body Sem_Ch6 is
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
@ -1598,7 +1601,7 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
end if;
<<Leave>>
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Analyze_Procedure_Call;
------------------------------
@ -3314,9 +3317,10 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
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;
------------------------------------

15
gcc/ada/sem_ch7.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -539,12 +539,14 @@ package body Sem_Ch7 is
-- 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 @@ package body Sem_Ch7 is
-- 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 @@ package body Sem_Ch7 is
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;
---------------------------------

12
gcc/ada/sem_elab.adb
View File

@ -1937,8 +1937,11 @@ package body Sem_Elab is
-- 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,9 +1969,10 @@ package body Sem_Elab is
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;
@ -1980,7 +1984,7 @@ package body Sem_Elab is
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;

32
gcc/ada/sem_prag.adb
View File

@ -472,8 +472,10 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
Restore_Ghost_Mode (Mode);
Restore_Ghost_Mode (Saved_GM);
end Check;
--------------------------
@ -24031,8 +24037,10 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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;
------------------------------------------

39
gcc/ada/sem_util.adb
View File

@ -11694,6 +11694,16 @@ package body Sem_Util is
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 @@ package body Sem_Util is
-- 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 @@ package body Sem_Util is
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 --

23
gcc/ada/sem_util.ads
View File

@ -1331,6 +1331,9 @@ package Sem_Util is
-- 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 @@ package Sem_Util is
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 @@ package Sem_Util is
-- 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 @@ package Sem_Util is
-- 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