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, 118 insertions, 28 deletions

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 5c886db..07579f0 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -209,9 +209,10 @@ package body Sem_Ch6 is
    ---------------------------------------------
 
    procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id) is
-      Designator : constant Entity_Id :=
-                     Analyze_Subprogram_Specification (Specification (N));
-      Scop       : constant Entity_Id := Current_Scope;
+      GM      : constant Ghost_Mode_Type := Ghost_Mode;
+      Scop    : constant Entity_Id := Current_Scope;
+      Subp_Id : constant Entity_Id :=
+                  Analyze_Subprogram_Specification (Specification (N));
 
    begin
       --  The abstract subprogram declaration may be subject to pragma Ghost
@@ -222,45 +223,49 @@ package body Sem_Ch6 is
       Set_Ghost_Mode (N);
       Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
 
-      Generate_Definition (Designator);
+      Generate_Definition (Subp_Id);
 
-      Set_Is_Abstract_Subprogram (Designator);
-      New_Overloaded_Entity (Designator);
-      Check_Delayed_Subprogram (Designator);
+      Set_Is_Abstract_Subprogram (Subp_Id);
+      New_Overloaded_Entity (Subp_Id);
+      Check_Delayed_Subprogram (Subp_Id);
 
-      Set_Categorization_From_Scope (Designator, Scop);
+      Set_Categorization_From_Scope (Subp_Id, Scop);
 
       --  An abstract subprogram declared within a Ghost region is rendered
       --  Ghost (SPARK RM 6.9(2)).
 
-      if Comes_From_Source (Designator) and then Ghost_Mode > None then
-         Set_Is_Ghost_Entity (Designator);
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (Subp_Id);
       end if;
 
-      if Ekind (Scope (Designator)) = E_Protected_Type then
-         Error_Msg_N
-           ("abstract subprogram not allowed in protected type", N);
+      if Ekind (Scope (Subp_Id)) = E_Protected_Type then
+         Error_Msg_N ("abstract subprogram not allowed in protected type", N);
 
       --  Issue a warning if the abstract subprogram is neither a dispatching
       --  operation nor an operation that overrides an inherited subprogram or
       --  predefined operator, since this most likely indicates a mistake.
 
       elsif Warn_On_Redundant_Constructs
-        and then not Is_Dispatching_Operation (Designator)
-        and then not Present (Overridden_Operation (Designator))
-        and then (not Is_Operator_Symbol_Name (Chars (Designator))
-                   or else Scop /= Scope (Etype (First_Formal (Designator))))
+        and then not Is_Dispatching_Operation (Subp_Id)
+        and then not Present (Overridden_Operation (Subp_Id))
+        and then (not Is_Operator_Symbol_Name (Chars (Subp_Id))
+                   or else Scop /= Scope (Etype (First_Formal (Subp_Id))))
       then
          Error_Msg_N
            ("abstract subprogram is not dispatching or overriding?r?", N);
       end if;
 
-      Generate_Reference_To_Formals (Designator);
-      Check_Eliminated (Designator);
+      Generate_Reference_To_Formals (Subp_Id);
+      Check_Eliminated (Subp_Id);
 
       if Has_Aspects (N) then
-         Analyze_Aspect_Specifications (N, Designator);
+         Analyze_Aspect_Specifications (N, Subp_Id);
       end if;
+
+      --  Restore the original Ghost mode once analysis and expansion have
+      --  taken place.
+
+      Ghost_Mode := GM;
    end Analyze_Abstract_Subprogram_Declaration;
 
    ---------------------------------
@@ -1542,16 +1547,15 @@ package body Sem_Ch6 is
    ----------------------------
 
    procedure Analyze_Procedure_Call (N : Node_Id) is
-      Loc     : constant Source_Ptr := Sloc (N);
-      P       : constant Node_Id    := Name (N);
-      Actuals : constant List_Id    := Parameter_Associations (N);
-      Actual  : Node_Id;
-      New_N   : Node_Id;
+      GM : constant Ghost_Mode_Type := Ghost_Mode;
 
       procedure Analyze_Call_And_Resolve;
       --  Do Analyze and Resolve calls for procedure call
       --  At end, check illegal order dependence.
 
+      procedure Restore_Globals;
+      --  Restore the values of all saved global variables
+
       ------------------------------
       -- Analyze_Call_And_Resolve --
       ------------------------------
@@ -1566,6 +1570,23 @@ package body Sem_Ch6 is
          end if;
       end Analyze_Call_And_Resolve;
 
+      ---------------------
+      -- Restore_Globals --
+      ---------------------
+
+      procedure Restore_Globals is
+      begin
+         Ghost_Mode := GM;
+      end Restore_Globals;
+
+      --  Local variables
+
+      Actuals : constant List_Id    := Parameter_Associations (N);
+      Loc     : constant Source_Ptr := Sloc (N);
+      P       : constant Node_Id    := Name (N);
+      Actual  : Node_Id;
+      New_N   : Node_Id;
+
    --  Start of processing for Analyze_Procedure_Call
 
    begin
@@ -1636,6 +1657,7 @@ package body Sem_Ch6 is
         and then Is_Record_Type (Etype (Entity (P)))
         and then Remote_AST_I_Dereference (P)
       then
+         Restore_Globals;
          return;
 
       elsif Is_Entity_Name (P)
@@ -1771,6 +1793,8 @@ package body Sem_Ch6 is
       else
          Error_Msg_N ("invalid procedure or entry call", N);
       end if;
+
+      Restore_Globals;
    end Analyze_Procedure_Call;
 
    ------------------------------
@@ -2251,6 +2275,7 @@ package body Sem_Ch6 is
    --  the subprogram, or to perform conformance checks.
 
    procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
+      GM           : constant Ghost_Mode_Type := Ghost_Mode;
       Loc          : constant Source_Ptr := Sloc (N);
       Body_Spec    : Node_Id             := Specification (N);
       Body_Id      : Entity_Id           := Defining_Entity (Body_Spec);
@@ -2326,6 +2351,9 @@ package body Sem_Ch6 is
       --  Determine whether subprogram Subp_Id is a primitive of a concurrent
       --  type that implements an interface and has a private view.
 
+      procedure Restore_Globals;
+      --  Restore the values of all saved global variables
+
       procedure Set_Trivial_Subprogram (N : Node_Id);
       --  Sets the Is_Trivial_Subprogram flag in both spec and body of the
       --  subprogram whose body is being analyzed. N is the statement node
@@ -2902,6 +2930,15 @@ package body Sem_Ch6 is
          return False;
       end Is_Private_Concurrent_Primitive;
 
+      ---------------------
+      -- Restore_Globals --
+      ---------------------
+
+      procedure Restore_Globals is
+      begin
+         Ghost_Mode := GM;
+      end Restore_Globals;
+
       ----------------------------
       -- Set_Trivial_Subprogram --
       ----------------------------
@@ -3044,6 +3081,7 @@ package body Sem_Ch6 is
                Check_Missing_Return;
             end if;
 
+            Restore_Globals;
             return;
 
          else
@@ -3051,6 +3089,7 @@ package body Sem_Ch6 is
             --  enter name will post error.
 
             Enter_Name (Body_Id);
+            Restore_Globals;
             return;
          end if;
 
@@ -3061,6 +3100,7 @@ package body Sem_Ch6 is
       --  analysis.
 
       elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
+         Restore_Globals;
          return;
 
       else
@@ -3139,6 +3179,7 @@ package body Sem_Ch6 is
             --  If this is a duplicate body, no point in analyzing it
 
             if Error_Posted (N) then
+               Restore_Globals;
                return;
             end if;
 
@@ -3251,6 +3292,7 @@ package body Sem_Ch6 is
 
          if Is_Abstract_Subprogram (Spec_Id) then
             Error_Msg_N ("an abstract subprogram cannot have a body", N);
+            Restore_Globals;
             return;
 
          else
@@ -3320,6 +3362,7 @@ package body Sem_Ch6 is
             if not Conformant
               and then not Mode_Conformant (Body_Id, Spec_Id)
             then
+               Restore_Globals;
                return;
             end if;
          end if;
@@ -3526,6 +3569,7 @@ package body Sem_Ch6 is
             Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
          end if;
 
+         Restore_Globals;
          return;
       end if;
 
@@ -3989,6 +4033,8 @@ package body Sem_Ch6 is
             Set_Has_Nested_Subprogram (Ent);
          end if;
       end;
+
+      Restore_Globals;
    end Analyze_Subprogram_Body_Helper;
 
    ---------------------------------
@@ -4093,12 +4139,30 @@ package body Sem_Ch6 is
    ------------------------------------
 
    procedure Analyze_Subprogram_Declaration (N : Node_Id) is
+      GM : constant Ghost_Mode_Type := Ghost_Mode;
+
+      procedure Restore_Globals;
+      --  Restore the values of all saved global variables
+
+      ---------------------
+      -- Restore_Globals --
+      ---------------------
+
+      procedure Restore_Globals is
+      begin
+         Ghost_Mode := GM;
+      end Restore_Globals;
+
+      --  Local variables
+
       Scop       : constant Entity_Id := Current_Scope;
       Designator : Entity_Id;
 
       Is_Completion : Boolean;
       --  Indicates whether a null procedure declaration is a completion
 
+   --  Start of processing for Analyze_Subprogram_Declaration
+
    begin
       --  The subprogram declaration may be subject to pragma Ghost with policy
       --  Ignore. Set the mode now to ensure that any nodes generated during
@@ -4124,10 +4188,10 @@ package body Sem_Ch6 is
 
          Analyze_Null_Procedure (N, Is_Completion);
 
-         if Is_Completion then
-
-            --  The null procedure acts as a body, nothing further is needed
+         --  The null procedure acts as a body, nothing further is needed
 
+         if Is_Completion then
+            Restore_Globals;
             return;
          end if;
       end if;
@@ -4308,6 +4372,8 @@ package body Sem_Ch6 is
       if Has_Aspects (N) then
          Analyze_Aspect_Specifications (N, Designator);
       end if;
+
+      Restore_Globals;
    end Analyze_Subprogram_Declaration;
 
    --------------------------------------
@@ -9374,6 +9440,12 @@ package body Sem_Ch6 is
 
             Check_Overriding_Indicator
               (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
+
+            --  The Ghost policy in effect at the point of declaration of a
+            --  parent subprogram and an overriding subprogram must match
+            --  (SPARK RM 6.9(17)).
+
+            Check_Ghost_Overriding (S, Overridden_Subp);
          end if;
 
       --  If there is a homonym that is not overloadable, then we have an
@@ -9526,6 +9598,12 @@ package body Sem_Ch6 is
 
                   if Comes_From_Source (E) then
                      Check_Overriding_Indicator (E, S, Is_Primitive => False);
+
+                     --  The Ghost policy in effect at the point of declaration
+                     --  of a parent subprogram and an overriding subprogram
+                     --  must match (SPARK RM 6.9(17)).
+
+                     Check_Ghost_Overriding (E, S);
                   end if;
 
                   return;
@@ -9721,6 +9799,12 @@ package body Sem_Ch6 is
 
                      Check_Overriding_Indicator (S, E, Is_Primitive => True);
 
+                     --  The Ghost policy in effect at the point of declaration
+                     --  of a parent subprogram and an overriding subprogram
+                     --  must match (SPARK RM 6.9(17)).
+
+                     Check_Ghost_Overriding (S, E);
+
                      --  If S is a user-defined subprogram or a null procedure
                      --  expanded to override an inherited null procedure, or a
                      --  predefined dispatching primitive then indicate that E
@@ -9857,6 +9941,12 @@ package body Sem_Ch6 is
          Check_Overriding_Indicator
            (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
 
+         --  The Ghost policy in effect at the point of declaration of a parent
+         --  subprogram and an overriding subprogram must match
+         --  (SPARK RM 6.9(17)).
+
+         Check_Ghost_Overriding (S, Overridden_Subp);
+
          --  Overloading is not allowed in SPARK, except for operators
 
          if Nkind (S) /= N_Defining_Operator_Symbol then