exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and restore the Ghost mode.

2015-05-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
	restore the Ghost mode.
	(Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
	(Freeze_Type): Update the call to Set_Ghost_Mode.
	(Restore_Globals): New routine.
	* exp_ch5.adb Add with and use clauses for Ghost.
	(Expand_N_Assignment_Statement): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch6.adb Add with and use clauses for Ghost.
	(Expand_N_Procedure_Call_Statement): Capture, set and
	restore the Ghost mode.
	(Expand_N_Subprogram_Body):
	Code cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Subprogram_Declaration): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch7.adb Add with and use clauses for Ghost.
	(Expand_N_Package_Body): Capture, set and restore the Ghost mode.
	(Expand_N_Package_Declaration): Capture, set and restore the
	Ghost mode.
	(Wrap_HSS_In_Block): Create a proper identifier for the block.
	* exp_ch8.adb Add with and use clauses for Ghost.
	(Expand_N_Exception_Renaming_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Object_Renaming_Declaration): Capture, set and restore
	the Ghost mode.
	(Expand_N_Package_Renaming_Declaration): Capture, set and restore the
	Ghost mode.
	(Expand_N_Subprogram_Renaming_Declaration): Capture, set and
	restore the Ghost mode.
	* exp_ch11.adb (Expand_N_Exception_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	* exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
	not initialize the dispatch table slot of a Ghost subprogram.
	* exp_prag.adb Add with and use clauses for Ghost.
	(Expand_Pragma_Check): Capture, set and restore the Ghost mode.
	(Expand_Pragma_Contract_Cases): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Initial_Condition): Capture, set and
	restore the Ghost mode.
	(Expand_Pragma_Loop_Variant): Capture,
	set and restore the Ghost mode.
	(Restore_Globals): New routine.
	* exp_util.adb Add with and use clauses for Ghost.
	(Make_Predicate_Call): Code cleanup. Capture, set and restore
	the Ghost mode.
	(Restore_Globals): New routine.
	* freeze.adb (Freeze_Entity): Code cleanup. Update the call
	to Set_Ghost_Mode.
	* ghost.adb Add with and use clause for Sem_Prag.
	(Check_Ghost_Completion): Code cleanup.
	(Check_Ghost_Overriding): New routine.
	(Check_Ghost_Policy): Code cleanup.
	(Ghost_Entity): New routine.
	(Is_Ghost_Declaration): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_OK_Context): Reimplemented.
	(Is_OK_Declaration): New routine.
	(Is_OK_Pragma): New routine.
	(Is_OK_Statement): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Propagate_Ignored_Ghost_Code): Update the comment on usage.
	(Set_From_Entity): New routine.
	(Set_From_Policy): New routine.
	(Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	(Set_Ghost_Mode_From_Policy): Removed.
	* ghost.ads (Check_Ghost_Overriding): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Set_Ghost_Mode): Update the parameter profile. Update the
	comment on usage.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	* sem_ch3.adb (Analyze_Full_Type_Declaration):
	Capture and restore the Ghost mode. Mark a type
	as Ghost regardless of whether it comes from source.
	(Analyze_Incomplete_Type_Decl): Capture, set and restore the
	Ghost mode.
	(Analyze_Number_Declaration): Capture and restore the Ghost mode.
	(Analyze_Object_Declaration): Capture and restore the Ghost mode.
	(Analyze_Private_Extension_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
	(Process_Full_View): The full view inherits all Ghost-related
	attributes from the private view.
	(Restore_Globals): New routine.
	* sem_ch5.adb (Analyze_Assignment): Capture and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
	Code cleanup. Capture and restore the Ghost mode. Mark a
	subprogram as Ghost regarless of whether it comes from source.
	(Analyze_Procedure_Call): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
	(New_Overloaded_Entity): Ensure that a
	parent subprogram and an overriding subprogram have compatible
	Ghost policies.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
	the Ghost mode.
	(Analyze_Package_Declaration): Capture and
	restore the Ghost mode. Mark a package as Ghost when it is
	declared in a Ghost region.
	(Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch8.adb (Analyze_Exception_Renaming): Code
	reformatting. Capture and restore the Ghost mode. A renaming
	becomes Ghost when its name references a Ghost entity.
	(Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Object_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Package_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Subprogram_Renaming): Capture and restore the Ghost
	mode. A renaming becomes Ghost when its name references a
	Ghost entity.
	* sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
	and restore the Ghost mode.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Generic_Subprogram_Declaration):
	Capture and restore the Ghost mode.
	* sem_ch13.adb Add with and use clauses for Ghost.
	(Add_Invariant): New routine.
	(Add_Invariants): Factor out code.
	(Add_Predicate): New routine.
	(Add_Predicates): Factor out code.
	(Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
	set and restore the Ghost mode.
	(Build_Invariant_Procedure): Code cleanup.
	(Build_Predicate_Functions): Capture, set and
	restore the Ghost mode. Mark the generated functions as Ghost.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_External_Property_In_Decl_Part): Capture, set and restore
	the Ghost mode.
	(Analyze_Initial_Condition_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_Pragma):
	Code cleanup. Capture, set and restore the Ghost mode. Flag
	pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
	Unreferenced_Objects as illegal when it applies to both Ghost
	and living arguments. Pragma Ghost cannot apply to synchronized
	objects.
	(Check_Kind): Moved to the spec of Sem_Prag.
	(Process_Inline): Flag the pragma as illegal when it applies to
	both Ghost and living arguments.
	(Restore_Globals): New routine.
	* sem_prag.ads Add pragma Default_Initial_Condition
	to table Assertion_Expression_Pragma. Add new table
	Is_Aspect_Specifying_Pragma.
	(Check_Kind): Moved from body of Sem_Prag.
	* sem_util.adb Add with and use clauses for Ghost.
	(Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
	the Ghost mode.
	(Build_Default_Init_Cond_Procedure_Declaration):
	Capture, set and restore the Ghost mode. Mark the default
	initial condition procedure as Ghost when it is declared
	in a Ghost region.
	(Is_Renaming_Declaration): New routine.
	(Policy_In_List): Account for the single argument version of
	Check_Pragma.
	* sem_util.ads (Is_Renaming_Declaration): New routine.
	* sinfo.adb (Is_Ghost_Pragma): New routine.
	(Set_Is_Ghost_Pragma): New routine.
	* sinfo.ads New attribute Is_Ghost_Pragma.
	(Is_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Ghost_Pragma): New routine along with pragma Inline.

From-SVN: r223684

1 files changed, 131 insertions, 21 deletions

diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index cb3f82e..52f6935 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -33,31 +33,122 @@ with Types;  use Types;
 
 package Sem_Prag is
 
+   --  The following table lists all pragmas that emulate an Ada 2012 aspect
+
+   Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
+     (Pragma_Abstract_State               => True,
+      Pragma_All_Calls_Remote             => True,
+      Pragma_Annotate                     => True,
+      Pragma_Async_Readers                => True,
+      Pragma_Async_Writers                => True,
+      Pragma_Asynchronous                 => True,
+      Pragma_Atomic                       => True,
+      Pragma_Atomic_Components            => True,
+      Pragma_Attach_Handler               => True,
+      Pragma_Contract_Cases               => True,
+      Pragma_Convention                   => True,
+      Pragma_CPU                          => True,
+      Pragma_Default_Initial_Condition    => True,
+      Pragma_Default_Storage_Pool         => True,
+      Pragma_Depends                      => True,
+      Pragma_Discard_Names                => True,
+      Pragma_Dispatching_Domain           => True,
+      Pragma_Effective_Reads              => True,
+      Pragma_Effective_Writes             => True,
+      Pragma_Elaborate_Body               => True,
+      Pragma_Export                       => True,
+      Pragma_Extensions_Visible           => True,
+      Pragma_Favor_Top_Level              => True,
+      Pragma_Ghost                        => True,
+      Pragma_Global                       => True,
+      Pragma_Import                       => True,
+      Pragma_Independent                  => True,
+      Pragma_Independent_Components       => True,
+      Pragma_Initial_Condition            => True,
+      Pragma_Initializes                  => True,
+      Pragma_Inline                       => True,
+      Pragma_Inline_Always                => True,
+      Pragma_Interrupt_Handler            => True,
+      Pragma_Interrupt_Priority           => True,
+      Pragma_Invariant                    => True,
+      Pragma_Linker_Section               => True,
+      Pragma_Lock_Free                    => True,
+      Pragma_No_Elaboration_Code_All      => True,
+      Pragma_No_Return                    => True,
+      Pragma_Obsolescent                  => True,
+      Pragma_Pack                         => True,
+      Pragma_Part_Of                      => True,
+      Pragma_Persistent_BSS               => True,
+      Pragma_Post                         => True,
+      Pragma_Post_Class                   => True,
+      Pragma_Postcondition                => True,
+      Pragma_Pre                          => True,
+      Pragma_Pre_Class                    => True,
+      Pragma_Precondition                 => True,
+      Pragma_Predicate                    => True,
+      Pragma_Preelaborable_Initialization => True,
+      Pragma_Preelaborate                 => True,
+      Pragma_Priority                     => True,
+      Pragma_Pure                         => True,
+      Pragma_Pure_Function                => True,
+      Pragma_Refined_Depends              => True,
+      Pragma_Refined_Global               => True,
+      Pragma_Refined_Post                 => True,
+      Pragma_Refined_State                => True,
+      Pragma_Relative_Deadline            => True,
+      Pragma_Remote_Access_Type           => True,
+      Pragma_Remote_Call_Interface        => True,
+      Pragma_Remote_Types                 => True,
+      Pragma_Shared                       => True,
+      Pragma_Shared_Passive               => True,
+      Pragma_Simple_Storage_Pool_Type     => True,
+      Pragma_SPARK_Mode                   => True,
+      Pragma_Storage_Size                 => True,
+      Pragma_Suppress                     => True,
+      Pragma_Suppress_Debug_Info          => True,
+      Pragma_Suppress_Initialization      => True,
+      Pragma_Test_Case                    => True,
+      Pragma_Thread_Local_Storage         => True,
+      Pragma_Type_Invariant               => True,
+      Pragma_Unchecked_Union              => True,
+      Pragma_Universal_Aliasing           => True,
+      Pragma_Universal_Data               => True,
+      Pragma_Unmodified                   => True,
+      Pragma_Unreferenced                 => True,
+      Pragma_Unreferenced_Objects         => True,
+      Pragma_Unsuppress                   => True,
+      Pragma_Volatile                     => True,
+      Pragma_Volatile_Components          => True,
+      Pragma_Volatile_Full_Access         => True,
+      Pragma_Warnings                     => True,
+      others                              => False);
+
    --  The following table lists all pragmas that act as an assertion
    --  expression.
 
    Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
-     (Pragma_Assert               => True,
-      Pragma_Assert_And_Cut       => True,
-      Pragma_Assume               => True,
-      Pragma_Check                => True,
-      Pragma_Contract_Cases       => True,
-      Pragma_Initial_Condition    => True,
-      Pragma_Invariant            => True,
-      Pragma_Loop_Invariant       => True,
-      Pragma_Loop_Variant         => True,
-      Pragma_Post                 => True,
-      Pragma_Post_Class           => True,
-      Pragma_Postcondition        => True,
-      Pragma_Pre                  => True,
-      Pragma_Pre_Class            => True,
-      Pragma_Precondition         => True,
-      Pragma_Predicate            => True,
-      Pragma_Refined_Post         => True,
-      Pragma_Test_Case            => True,
-      Pragma_Type_Invariant       => True,
-      Pragma_Type_Invariant_Class => True,
-      others                      => False);
+     (Pragma_Assert                    => True,
+      Pragma_Assert_And_Cut            => True,
+      Pragma_Assume                    => True,
+      Pragma_Check                     => True,
+      Pragma_Contract_Cases            => True,
+      Pragma_Default_Initial_Condition => True,
+      Pragma_Initial_Condition         => True,
+      Pragma_Invariant                 => True,
+      Pragma_Loop_Invariant            => True,
+      Pragma_Loop_Variant              => True,
+      Pragma_Post                      => True,
+      Pragma_Post_Class                => True,
+      Pragma_Postcondition             => True,
+      Pragma_Pre                       => True,
+      Pragma_Pre_Class                 => True,
+      Pragma_Precondition              => True,
+      Pragma_Predicate                 => True,
+      Pragma_Refined_Post              => True,
+      Pragma_Test_Case                 => True,
+      Pragma_Type_Invariant            => True,
+      Pragma_Type_Invariant_Class      => True,
+      others                           => False);
 
    --  The following table lists all the implementation-defined pragmas that
    --  may apply to a body stub (no language defined pragmas apply). The table
@@ -156,6 +247,25 @@ package Sem_Prag is
    --  is the related variable or state. Ensure legality of the combination and
    --  issue an error for an illegal combination.
 
+   function Check_Kind (Nam : Name_Id) return Name_Id;
+   --  This function is used in connection with pragmas Assert, Check,
+   --  and assertion aspects and pragmas, to determine if Check pragmas
+   --  (or corresponding assertion aspects or pragmas) are currently active
+   --  as determined by the presence of -gnata on the command line (which
+   --  sets the default), and the appearance of pragmas Check_Policy and
+   --  Assertion_Policy as configuration pragmas either in a configuration
+   --  pragma file, or at the start of the current unit, or locally given
+   --  Check_Policy and Assertion_Policy pragmas that are currently active.
+   --
+   --  The value returned is one of the names Check, Ignore, Disable (On
+   --  returns Check, and Off returns Ignore).
+   --
+   --  Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
+   --  and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
+   --  Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
+   --  _Post, _Invariant, or _Type_Invariant, which are special names used
+   --  in identifiers to represent these attribute references.
+
    procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
    --  Determine whether the placement within the state space of an abstract
    --  state, variable or package instantiation denoted by Item_Id requires the