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, 374 insertions, 332 deletions

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 7abf871..8db5b50 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -34,6 +34,7 @@ with Exp_Disp; use Exp_Disp;
 with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Freeze;   use Freeze;
+with Ghost;    use Ghost;
 with Lib;      use Lib;
 with Lib.Xref; use Lib.Xref;
 with Namet;    use Namet;
@@ -7762,21 +7763,25 @@ package body Sem_Ch13 is
    function Build_Invariant_Procedure_Declaration
      (Typ : Entity_Id) return Node_Id
    is
-      Loc           : constant Source_Ptr := Sloc (Typ);
-      Object_Entity : constant Entity_Id :=
-        Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
-      Spec          : Node_Id;
-      SId           : Entity_Id;
+      GM     : constant Ghost_Mode_Type := Ghost_Mode;
+      Loc    : constant Source_Ptr := Sloc (Typ);
+      Decl   : Node_Id;
+      Obj_Id : Entity_Id;
+      SId    : Entity_Id;
 
    begin
-      Set_Etype (Object_Entity, Typ);
-
-      --  Check for duplicate definiations.
+      --  Check for duplicate definiations
 
       if Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)) then
          return Empty;
       end if;
 
+      --  The related type may be subject to pragma Ghost with policy Ignore.
+      --  Set the mode now to ensure that the predicate functions are properly
+      --  flagged as ignored Ghost.
+
+      Set_Ghost_Mode_From_Entity (Typ);
+
       SId :=
         Make_Defining_Identifier (Loc,
           Chars => New_External_Name (Chars (Typ), "Invariant"));
@@ -7786,15 +7791,31 @@ package body Sem_Ch13 is
       Set_Is_Invariant_Procedure (SId);
       Set_Invariant_Procedure (Typ, SId);
 
-      Spec :=
-        Make_Procedure_Specification (Loc,
-          Defining_Unit_Name       => SId,
-          Parameter_Specifications => New_List (
-            Make_Parameter_Specification (Loc,
-              Defining_Identifier => Object_Entity,
-              Parameter_Type      => New_Occurrence_Of (Typ, Loc))));
+      --  Mark the invariant procedure explicitly as Ghost because it does not
+      --  come from source.
+
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (SId);
+      end if;
+
+      Obj_Id := Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
+      Set_Etype (Obj_Id, Typ);
+
+      Decl :=
+        Make_Subprogram_Declaration (Loc,
+          Make_Procedure_Specification (Loc,
+            Defining_Unit_Name       => SId,
+            Parameter_Specifications => New_List (
+              Make_Parameter_Specification (Loc,
+                Defining_Identifier => Obj_Id,
+                Parameter_Type      => New_Occurrence_Of (Typ, Loc)))));
+
+      --  Restore the original Ghost mode once analysis and expansion have
+      --  taken place.
+
+      Ghost_Mode := GM;
 
-      return Make_Subprogram_Declaration (Loc, Specification => Spec);
+      return Decl;
    end Build_Invariant_Procedure_Declaration;
 
    -------------------------------
@@ -7813,6 +7834,9 @@ package body Sem_Ch13 is
    --  end typInvariant;
 
    procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
+      Priv_Decls : constant List_Id := Private_Declarations (N);
+      Vis_Decls  : constant List_Id := Visible_Declarations (N);
+
       Loc   : constant Source_Ptr := Sloc (Typ);
       Stmts : List_Id;
       Spec  : Node_Id;
@@ -7820,13 +7844,11 @@ package body Sem_Ch13 is
       PDecl : Node_Id;
       PBody : Node_Id;
 
-      Nam : Name_Id;
-      --  Name for Check pragma, usually Invariant, but might be Type_Invariant
-      --  if we come from a Type_Invariant aspect, we make sure to build the
-      --  Check pragma with the right name, so that Check_Policy works right.
+      Object_Entity : Node_Id;
+      --  The entity of the formal for the procedure
 
-      Visible_Decls : constant List_Id := Visible_Declarations (N);
-      Private_Decls : constant List_Id := Private_Declarations (N);
+      Object_Name : Name_Id;
+      --  Name for argument of invariant procedure
 
       procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
       --  Appends statements to Stmts for any invariants in the rep item chain
@@ -7836,246 +7858,229 @@ package body Sem_Ch13 is
       --  "inherited" to the exception message and generating an informational
       --  message about the inheritance of an invariant.
 
-      Object_Name : Name_Id;
-      --  Name for argument of invariant procedure
-
-      Object_Entity : Node_Id;
-      --  The entity of the formal for the procedure
-
       --------------------
       -- Add_Invariants --
       --------------------
 
       procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
-         Ritem : Node_Id;
-         Arg1  : Node_Id;
-         Arg2  : Node_Id;
-         Arg3  : Node_Id;
-         Exp   : Node_Id;
-         Loc   : Source_Ptr;
-         Assoc : List_Id;
-         Str   : String_Id;
-
-         procedure Replace_Type_Reference (N : Node_Id);
-         --  Replace a single occurrence N of the subtype name with a reference
-         --  to the formal of the predicate function. N can be an identifier
-         --  referencing the subtype, or a selected component, representing an
-         --  appropriately qualified occurrence of the subtype name.
-
-         procedure Replace_Type_References is
-           new Replace_Type_References_Generic (Replace_Type_Reference);
-         --  Traverse an expression replacing all occurrences of the subtype
-         --  name with appropriate references to the object that is the formal
-         --  parameter of the predicate function. Note that we must ensure
-         --  that the type and entity information is properly set in the
-         --  replacement node, since we will do a Preanalyze call of this
-         --  expression without proper visibility of the procedure argument.
+         procedure Add_Invariant (Prag : Node_Id);
+         --  Create a runtime check to verify the exression of invariant pragma
+         --  Prag. All generated code is added to list Stmts.
 
-         ----------------------------
-         -- Replace_Type_Reference --
-         ----------------------------
+         -------------------
+         -- Add_Invariant --
+         -------------------
 
-         --  Note: See comments in Add_Predicates.Replace_Type_Reference
-         --  regarding handling of Sloc and Comes_From_Source.
+         procedure Add_Invariant (Prag : Node_Id) is
+            procedure Replace_Type_Reference (N : Node_Id);
+            --  Replace a single occurrence N of the subtype name with a
+            --  reference to the formal of the predicate function. N can be an
+            --  identifier referencing the subtype, or a selected component,
+            --  representing an appropriately qualified occurrence of the
+            --  subtype name.
+
+            procedure Replace_Type_References is
+              new Replace_Type_References_Generic (Replace_Type_Reference);
+            --  Traverse an expression replacing all occurrences of the subtype
+            --  name with appropriate references to the formal of the predicate
+            --  function. Note that we must ensure that the type and entity
+            --  information is properly set in the replacement node, since we
+            --  will do a Preanalyze call of this expression without proper
+            --  visibility of the procedure argument.
+
+            ----------------------------
+            -- Replace_Type_Reference --
+            ----------------------------
+
+            --  Note: See comments in Add_Predicates.Replace_Type_Reference
+            --  regarding handling of Sloc and Comes_From_Source.
+
+            procedure Replace_Type_Reference (N : Node_Id) is
+               Nloc : constant Source_Ptr := Sloc (N);
 
-         procedure Replace_Type_Reference (N : Node_Id) is
-         begin
+            begin
+               --  Add semantic information to node to be rewritten, for ASIS
+               --  navigation needs.
 
-            --  Add semantic information to node to be rewritten, for ASIS
-            --  navigation needs.
+               if Nkind (N) = N_Identifier then
+                  Set_Entity (N, T);
+                  Set_Etype  (N, T);
 
-            if Nkind (N) = N_Identifier then
-               Set_Entity (N, T);
-               Set_Etype  (N, T);
+               elsif Nkind (N) = N_Selected_Component then
+                  Analyze (Prefix (N));
+                  Set_Entity (Selector_Name (N), T);
+                  Set_Etype  (Selector_Name (N), T);
+               end if;
 
-            elsif Nkind (N) = N_Selected_Component then
-               Analyze (Prefix (N));
-               Set_Entity (Selector_Name (N), T);
-               Set_Etype  (Selector_Name (N), T);
-            end if;
+               --  Invariant'Class, replace with T'Class (obj)
 
-            --  Invariant'Class, replace with T'Class (obj)
-            --  In ASIS mode, an inherited item is analyzed already, and the
-            --  replacement has been done, so do not repeat transformation
-            --  to prevent ill-formed tree.
+               if Class_Present (Prag) then
 
-            if Class_Present (Ritem) then
-               if ASIS_Mode
-                 and then Nkind (Parent (N)) = N_Attribute_Reference
-                 and then Attribute_Name (Parent (N)) = Name_Class
-               then
-                  null;
+                  --  In ASIS mode, an inherited item is already analyzed,
+                  --  and the replacement has been done, so do not repeat
+                  --  the transformation to prevent a malformed tree.
 
-               else
-                  Rewrite (N,
-                    Make_Type_Conversion (Sloc (N),
-                      Subtype_Mark =>
-                        Make_Attribute_Reference (Sloc (N),
-                          Prefix         => New_Occurrence_Of (T, Sloc (N)),
-                          Attribute_Name => Name_Class),
-                      Expression   =>
-                         Make_Identifier (Sloc (N), Object_Name)));
+                  if ASIS_Mode
+                    and then Nkind (Parent (N)) = N_Attribute_Reference
+                    and then Attribute_Name (Parent (N)) = Name_Class
+                  then
+                     null;
 
-                  Set_Entity (Expression (N), Object_Entity);
-                  Set_Etype  (Expression (N), Typ);
-               end if;
+                  else
+                     Rewrite (N,
+                       Make_Type_Conversion (Nloc,
+                         Subtype_Mark =>
+                           Make_Attribute_Reference (Nloc,
+                             Prefix         => New_Occurrence_Of (T, Nloc),
+                             Attribute_Name => Name_Class),
+                         Expression   => Make_Identifier (Nloc, Object_Name)));
+
+                     Set_Entity (Expression (N), Object_Entity);
+                     Set_Etype  (Expression (N), Typ);
+                  end if;
 
-            --  Invariant, replace with obj
+               --  Invariant, replace with obj
 
-            else
-               Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
-               Set_Entity (N, Object_Entity);
-               Set_Etype  (N, Typ);
-            end if;
+               else
+                  Rewrite (N, Make_Identifier (Nloc, Object_Name));
+                  Set_Entity (N, Object_Entity);
+                  Set_Etype  (N, Typ);
+               end if;
 
-            Set_Comes_From_Source (N, True);
-         end Replace_Type_Reference;
+               Set_Comes_From_Source (N, True);
+            end Replace_Type_Reference;
 
-      --  Start of processing for Add_Invariants
+            --  Local variables
 
-      begin
-         Ritem := First_Rep_Item (T);
-         while Present (Ritem) loop
-            if Nkind (Ritem) = N_Pragma
-              and then Pragma_Name (Ritem) = Name_Invariant
-            then
-               Arg1 := First (Pragma_Argument_Associations (Ritem));
-               Arg2 := Next (Arg1);
-               Arg3 := Next (Arg2);
+            Asp   : constant Node_Id    := Corresponding_Aspect (Prag);
+            Nam   : constant Name_Id    := Original_Aspect_Pragma_Name (Prag);
+            Ploc  : constant Source_Ptr := Sloc (Prag);
+            Arg1  : Node_Id;
+            Arg2  : Node_Id;
+            Arg3  : Node_Id;
+            Assoc : List_Id;
+            Expr  : Node_Id;
+            Str   : String_Id;
 
-               Arg1 := Get_Pragma_Arg (Arg1);
-               Arg2 := Get_Pragma_Arg (Arg2);
+         --  Start of processing for Add_Invariant
 
-               --  For Inherit case, ignore Invariant, process only Class case
+         begin
+            --  Extract the arguments of the invariant pragma
 
-               if Inherit then
-                  if not Class_Present (Ritem) then
-                     goto Continue;
-                  end if;
+            Arg1 := First (Pragma_Argument_Associations (Prag));
+            Arg2 := Next (Arg1);
+            Arg3 := Next (Arg2);
 
-               --  For Inherit false, process only item for right type
+            Arg1 := Get_Pragma_Arg (Arg1);
+            Arg2 := Get_Pragma_Arg (Arg2);
 
-               else
-                  if Entity (Arg1) /= Typ then
-                     goto Continue;
-                  end if;
-               end if;
+            --  The caller requests processing of all Invariant'Class pragmas,
+            --  but the current pragma does not fall in this category. Return
+            --  as there is nothing left to do.
 
-               if No (Stmts) then
-                  Stmts := Empty_List;
+            if Inherit then
+               if not Class_Present (Prag) then
+                  return;
                end if;
 
-               Exp := New_Copy_Tree (Arg2);
+            --  Otherwise the pragma must apply to the current type
 
-               --  Preserve sloc of original pragma Invariant
+            elsif Entity (Arg1) /= T then
+               return;
+            end if;
 
-               Loc := Sloc (Ritem);
+            Expr := New_Copy_Tree (Arg2);
 
-               --  We need to replace any occurrences of the name of the type
-               --  with references to the object, converted to type'Class in
-               --  the case of Invariant'Class aspects.
+            --  Replace all occurrences of the type's name with references to
+            --  the formal parameter of the invariant procedure.
 
-               Replace_Type_References (Exp, T);
+            Replace_Type_References (Expr, T);
 
-               --  If this invariant comes from an aspect, find the aspect
-               --  specification, and replace the saved expression because
-               --  we need the subtype references replaced for the calls to
-               --  Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
-               --  and Check_Aspect_At_End_Of_Declarations.
+            --  If the invariant pragma comes from an aspect, replace the saved
+            --  expression because we need the subtype references replaced for
+            --  the calls to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
+            --  routines.
 
-               if From_Aspect_Specification (Ritem) then
-                  declare
-                     Aitem : Node_Id;
+            if Present (Asp) then
+               Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
+            end if;
 
-                  begin
-                     --  Loop to find corresponding aspect, note that this
-                     --  must be present given the pragma is marked delayed.
+            --  Preanalyze the invariant expression to capture the visibility
+            --  of the proper package part. In general the expression is not
+            --  fully analyzed until the body of the invariant procedure is
+            --  analyzed at the end of the private part, but that yields the
+            --  wrong visibility.
 
-                     --  Note: in practice Next_Rep_Item (Ritem) is Empty so
-                     --  this loop does nothing. Furthermore, why isn't this
-                     --  simply Corresponding_Aspect ???
+            --  Historic note: we used to set N as the parent, but a package
+            --  specification as the parent of an expression is bizarre.
 
-                     Aitem := Next_Rep_Item (Ritem);
-                     while Present (Aitem) loop
-                        if Nkind (Aitem) = N_Aspect_Specification
-                          and then Aspect_Rep_Item (Aitem) = Ritem
-                        then
-                           Set_Entity
-                             (Identifier (Aitem), New_Copy_Tree (Exp));
-                           exit;
-                        end if;
+            Set_Parent (Expr, Parent (Arg2));
+            Preanalyze_Assert_Expression (Expr, Any_Boolean);
 
-                        Aitem := Next_Rep_Item (Aitem);
-                     end loop;
-                  end;
-               end if;
-
-               --  Now we need to preanalyze the expression to properly capture
-               --  the visibility in the visible part. The expression will not
-               --  be analyzed for real until the body is analyzed, but that is
-               --  at the end of the private part and has the wrong visibility.
+            --  A class-wide invariant may be inherited in a separate unit,
+            --  where the corresponding expression cannot be resolved by
+            --  visibility, because it refers to a local function. Propagate
+            --  semantic information to the original representation item, to
+            --  be used when an invariant procedure for a derived type is
+            --  constructed.
 
-               Set_Parent (Exp, N);
-               Preanalyze_Assert_Expression (Exp, Any_Boolean);
+            --  ??? Unclear how to handle class-wide invariants that are not
+            --  function calls.
 
-               --  A class-wide invariant may be inherited in a separate unit,
-               --  where the corresponding expression cannot be resolved by
-               --  visibility, because it refers to a local function. Propagate
-               --  semantic information to the original representation item, to
-               --  be used when an invariant procedure for a derived type is
-               --  constructed.
+            if not Inherit
+              and then Class_Present (Prag)
+              and then Nkind (Expr) = N_Function_Call
+              and then Nkind (Arg2) = N_Indexed_Component
+            then
+               Rewrite (Arg2,
+                 Make_Function_Call (Ploc,
+                   Name                   =>
+                     New_Occurrence_Of (Entity (Name (Expr)), Ploc),
+                   Parameter_Associations =>
+                     New_Copy_List (Expressions (Arg2))));
+            end if;
 
-               --  Unclear how to handle class-wide invariants that are not
-               --  function calls ???
+            --  In ASIS mode, even if assertions are not enabled, we must
+            --  analyze the original expression in the aspect specification
+            --  because it is part of the original tree.
 
-               if not Inherit
-                 and then Class_Present (Ritem)
-                 and then Nkind (Exp) = N_Function_Call
-                 and then Nkind (Arg2) = N_Indexed_Component
-               then
-                  Rewrite (Arg2,
-                    Make_Function_Call (Loc,
-                      Name                   =>
-                        New_Occurrence_Of (Entity (Name (Exp)), Loc),
-                      Parameter_Associations =>
-                        New_Copy_List (Expressions (Arg2))));
-               end if;
-
-               --  In ASIS mode, even if assertions are not enabled, we must
-               --  analyze the original expression in the aspect specification
-               --  because it is part of the original tree.
+            if ASIS_Mode and then Present (Asp) then
+               declare
+                  Orig_Expr : constant Node_Id := Expression (Asp);
+               begin
+                  Replace_Type_References (Orig_Expr, T);
+                  Preanalyze_Assert_Expression (Orig_Expr, Any_Boolean);
+               end;
+            end if;
 
-               if ASIS_Mode and then From_Aspect_Specification (Ritem) then
-                  declare
-                     Inv : constant Node_Id :=
-                             Expression (Corresponding_Aspect (Ritem));
-                  begin
-                     Replace_Type_References (Inv, T);
-                     Preanalyze_Assert_Expression (Inv, Standard_Boolean);
-                  end;
-               end if;
+            --  An ignored invariant must not generate a runtime check. Add a
+            --  null statement to ensure that the invariant procedure does get
+            --  a completing body.
 
-               --  Get name to be used for Check pragma. Using the original
-               --  name ensures that 'Class case is properly handled.
+            if No (Stmts) then
+               Stmts := Empty_List;
+            end if;
 
-               Nam := Original_Aspect_Pragma_Name (Ritem);
+            if Is_Ignored (Prag) then
+               Append_To (Stmts, Make_Null_Statement (Ploc));
 
-               --  Build first two arguments for Check pragma
+            --  Otherwise the invariant is checked. Build a Check pragma to
+            --  verify the expression at runtime.
 
-               Assoc :=
-                 New_List (
-                   Make_Pragma_Argument_Association (Loc,
-                     Expression => Make_Identifier (Loc, Chars => Nam)),
-                   Make_Pragma_Argument_Association (Loc,
-                     Expression => Exp));
+            else
+               Assoc := New_List (
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Make_Identifier (Ploc, Nam)),
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Expr));
 
-               --  Add message if present in Invariant pragma
+               --  Handle the String argument (if any)
 
                if Present (Arg3) then
                   Str := Strval (Get_Pragma_Arg (Arg3));
 
-                  --  If inherited case, and message starts "failed invariant",
-                  --  change it to be "failed inherited invariant".
+                  --  When inheriting an invariant, modify the message from
+                  --  "failed invariant" to "failed inherited invariant".
 
                   if Inherit then
                      String_To_Name_Buffer (Str);
@@ -8087,30 +8092,45 @@ package body Sem_Ch13 is
                   end if;
 
                   Append_To (Assoc,
-                    Make_Pragma_Argument_Association (Loc,
-                      Expression => Make_String_Literal (Loc, Str)));
+                    Make_Pragma_Argument_Association (Ploc,
+                      Expression => Make_String_Literal (Ploc, Str)));
                end if;
 
-               --  Add Check pragma to list of statements
+               --  Generate:
+               --    pragma Check (Nam, Expr, Str);
 
                Append_To (Stmts,
-                 Make_Pragma (Loc,
+                 Make_Pragma (Ploc,
                    Pragma_Identifier            =>
-                     Make_Identifier (Loc, Name_Check),
+                     Make_Identifier (Ploc, Name_Check),
                    Pragma_Argument_Associations => Assoc));
+            end if;
 
-               --  If Inherited case and option enabled, output info msg. Note
-               --  that we know this is a case of Invariant'Class.
+            --  Output an info message when inheriting an invariant and the
+            --  listing option is enabled.
 
-               if Inherit and Opt.List_Inherited_Aspects then
-                  Error_Msg_Sloc := Sloc (Ritem);
-                  Error_Msg_N
-                    ("info: & inherits `Invariant''Class` aspect from #?L?",
-                     Typ);
-               end if;
+            if Inherit and Opt.List_Inherited_Aspects then
+               Error_Msg_Sloc := Sloc (Prag);
+               Error_Msg_N
+                 ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
+            end if;
+         end Add_Invariant;
+
+         --  Local variables
+
+         Ritem : Node_Id;
+
+      --  Start of processing for Add_Invariants
+
+      begin
+         Ritem := First_Rep_Item (T);
+         while Present (Ritem) loop
+            if Nkind (Ritem) = N_Pragma
+              and then Pragma_Name (Ritem) = Name_Invariant
+            then
+               Add_Invariant (Ritem);
             end if;
 
-         <<Continue>>
             Next_Rep_Item (Ritem);
          end loop;
       end Add_Invariants;
@@ -8228,13 +8248,13 @@ package body Sem_Ch13 is
          --  If declaration is already analyzed, it was processed by the
          --  generated pragma.
 
-         if Present (Private_Decls) then
+         if Present (Priv_Decls) then
 
             --  The spec goes at the end of visible declarations, but they have
             --  already been analyzed, so we need to explicitly do the analyze.
 
             if not Analyzed (PDecl) then
-               Append_To (Visible_Decls, PDecl);
+               Append_To (Vis_Decls, PDecl);
                Analyze (PDecl);
             end if;
 
@@ -8243,7 +8263,7 @@ package body Sem_Ch13 is
             --  analyze call. We skip this if there are no private declarations
             --  (this is an error that will be caught elsewhere);
 
-            Append_To (Private_Decls, PBody);
+            Append_To (Priv_Decls, PBody);
 
             --  If the invariant appears on the full view of a type, the
             --  analysis of the private part is complete, and we must
@@ -8261,8 +8281,8 @@ package body Sem_Ch13 is
          --  that the type is about to be frozen.
 
          elsif not Is_Private_Type (Typ) then
-            Append_To (Visible_Decls, PDecl);
-            Append_To (Visible_Decls, PBody);
+            Append_To (Vis_Decls, PDecl);
+            Append_To (Vis_Decls, PBody);
             Analyze (PDecl);
             Analyze (PBody);
          end if;
@@ -8332,13 +8352,6 @@ package body Sem_Ch13 is
       --  Inheritance of predicates for the parent type is done by calling the
       --  Predicate_Function of the parent type, using Add_Call above.
 
-      function Test_RE (N : Node_Id) return Traverse_Result;
-      --  Used in Test_REs, tests one node for being a raise expression, and if
-      --  so sets Raise_Expression_Present True.
-
-      procedure Test_REs is new Traverse_Proc (Test_RE);
-      --  Tests to see if Expr contains any raise expressions
-
       function Process_RE (N : Node_Id) return Traverse_Result;
       --  Used in Process REs, tests if node N is a raise expression, and if
       --  so, marks it to be converted to return False.
@@ -8346,6 +8359,13 @@ package body Sem_Ch13 is
       procedure Process_REs is new Traverse_Proc (Process_RE);
       --  Marks any raise expressions in Expr_M to return False
 
+      function Test_RE (N : Node_Id) return Traverse_Result;
+      --  Used in Test_REs, tests one node for being a raise expression, and if
+      --  so sets Raise_Expression_Present True.
+
+      procedure Test_REs is new Traverse_Proc (Test_RE);
+      --  Tests to see if Expr contains any raise expressions
+
       --------------
       -- Add_Call --
       --------------
@@ -8399,128 +8419,121 @@ package body Sem_Ch13 is
       --------------------
 
       procedure Add_Predicates is
-         Ritem : Node_Id;
-         Arg1  : Node_Id;
-         Arg2  : Node_Id;
-
-         procedure Replace_Type_Reference (N : Node_Id);
-         --  Replace a single occurrence N of the subtype name with a reference
-         --  to the formal of the predicate function. N can be an identifier
-         --  referencing the subtype, or a selected component, representing an
-         --  appropriately qualified occurrence of the subtype name.
+         procedure Add_Predicate (Prag : Node_Id);
+         --  Concatenate the expression of predicate pragma Prag to Expr by
+         --  using a short circuit "and then" operator.
 
-         procedure Replace_Type_References is
-           new Replace_Type_References_Generic (Replace_Type_Reference);
-         --  Traverse an expression changing every occurrence of an identifier
-         --  whose name matches the name of the subtype with a reference to
-         --  the formal parameter of the predicate function.
+         -------------------
+         -- Add_Predicate --
+         -------------------
 
-         ----------------------------
-         -- Replace_Type_Reference --
-         ----------------------------
+         procedure Add_Predicate (Prag : Node_Id) is
+            procedure Replace_Type_Reference (N : Node_Id);
+            --  Replace a single occurrence N of the subtype name with a
+            --  reference to the formal of the predicate function. N can be an
+            --  identifier referencing the subtype, or a selected component,
+            --  representing an appropriately qualified occurrence of the
+            --  subtype name.
+
+            procedure Replace_Type_References is
+              new Replace_Type_References_Generic (Replace_Type_Reference);
+            --  Traverse an expression changing every occurrence of an
+            --  identifier whose name matches the name of the subtype with a
+            --  reference to the formal parameter of the predicate function.
+
+            ----------------------------
+            -- Replace_Type_Reference --
+            ----------------------------
+
+            procedure Replace_Type_Reference (N : Node_Id) is
+            begin
+               Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
+               --  Use the Sloc of the usage name, not the defining name
 
-         procedure Replace_Type_Reference (N : Node_Id) is
-         begin
-            Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
-            --  Use the Sloc of the usage name, not the defining name
+               Set_Etype (N, Typ);
+               Set_Entity (N, Object_Entity);
 
-            Set_Etype (N, Typ);
-            Set_Entity (N, Object_Entity);
+               --  We want to treat the node as if it comes from source, so
+               --  that ASIS will not ignore it.
 
-            --  We want to treat the node as if it comes from source, so that
-            --  ASIS will not ignore it
+               Set_Comes_From_Source (N, True);
+            end Replace_Type_Reference;
 
-            Set_Comes_From_Source (N, True);
-         end Replace_Type_Reference;
+            --  Local variables
 
-      --  Start of processing for Add_Predicates
+            Asp  : constant Node_Id := Corresponding_Aspect (Prag);
+            Arg1 : Node_Id;
+            Arg2 : Node_Id;
 
-      begin
-         Ritem := First_Rep_Item (Typ);
+         --  Start of processing for Add_Predicate
 
-         while Present (Ritem) loop
-            if Nkind (Ritem) = N_Pragma
-              and then Pragma_Name (Ritem) = Name_Predicate
-            then
-               --  Acquire arguments. The expression itself is copied for use
-               --  in the predicate function, to preserve the original version
-               --  for ASIS use.
-
-               Arg1 := First (Pragma_Argument_Associations (Ritem));
-               Arg2 := Next (Arg1);
+         begin
+            --  Extract the arguments of the pragma. The expression itself
+            --  is copied for use in the predicate function, to preserve the
+            --  original version for ASIS use.
 
-               Arg1 := Get_Pragma_Arg (Arg1);
-               Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
+            Arg1 := First (Pragma_Argument_Associations (Prag));
+            Arg2 := Next (Arg1);
 
-               --  See if this predicate pragma is for the current type or for
-               --  its full view. A predicate on a private completion is placed
-               --  on the partial view beause this is the visible entity that
-               --  is frozen.
+            Arg1 := Get_Pragma_Arg (Arg1);
+            Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
 
-               if Entity (Arg1) = Typ
-                 or else Full_View (Entity (Arg1)) = Typ
-               then
-                  --  We have a match, this entry is for our subtype
+            --  When the predicate pragma applies to the current type or its
+            --  full view, replace all occurrences of the subtype name with
+            --  references to the formal parameter of the predicate function.
 
-                  --  We need to replace any occurrences of the name of the
-                  --  type with references to the object.
+            if Entity (Arg1) = Typ
+              or else Full_View (Entity (Arg1)) = Typ
+            then
+               Replace_Type_References (Arg2, Typ);
 
-                  Replace_Type_References (Arg2, Typ);
+               --  If the predicate pragma comes from an aspect, replace the
+               --  saved expression because we need the subtype references
+               --  replaced for the calls to Preanalyze_Spec_Expression in
+               --  Check_Aspect_At_xxx routines.
 
-                  --  If this predicate comes from an aspect, find the aspect
-                  --  specification, and replace the saved expression because
-                  --  we need the subtype references replaced for the calls to
-                  --  Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
-                  --  and Check_Aspect_At_End_Of_Declarations.
+               if Present (Asp) then
 
-                  if From_Aspect_Specification (Ritem) then
-                     declare
-                        Aitem     : Node_Id;
-                        Orig_Expr : constant Node_Id :=
-                           Expression (Corresponding_Aspect (Ritem));
+                  --  For ASIS use, perform semantic analysis of the original
+                  --  predicate expression, which is otherwise not utilized.
 
-                     begin
+                  if ASIS_Mode then
+                     Preanalyze_And_Resolve (Expression (Asp));
+                  end if;
 
-                        --  For ASIS use, perform semantic analysis of the
-                        --  original predicate expression, which is otherwise
-                        --  not utilized.
+                  Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2));
+               end if;
 
-                        if ASIS_Mode then
-                           Preanalyze_And_Resolve (Orig_Expr);
-                        end if;
+               --  Concatenate to the existing predicate expressions by using
+               --  "and then".
 
-                        --  Loop to find corresponding aspect, note that this
-                        --  must be present given the pragma is marked delayed.
+               if Present (Expr) then
+                  Expr :=
+                    Make_And_Then (Loc,
+                      Left_Opnd  => Relocate_Node (Expr),
+                      Right_Opnd => Relocate_Node (Arg2));
 
-                        Aitem := Next_Rep_Item (Ritem);
-                        loop
-                           if Nkind (Aitem) = N_Aspect_Specification
-                             and then Aspect_Rep_Item (Aitem) = Ritem
-                           then
-                              Set_Entity
-                                (Identifier (Aitem), New_Copy_Tree (Arg2));
-                              exit;
-                           end if;
+               --  Otherwise this is the first predicate expression
 
-                           Aitem := Next_Rep_Item (Aitem);
-                        end loop;
-                     end;
-                  end if;
+               else
+                  Expr := Relocate_Node (Arg2);
+               end if;
+            end if;
+         end Add_Predicate;
 
-                  --  Now we can add the expression
+         --  Local variables
 
-                  if No (Expr) then
-                     Expr := Relocate_Node (Arg2);
+         Ritem : Node_Id;
 
-                  --  There already was a predicate, so add to it
+      --  Start of processing for Add_Predicates
 
-                  else
-                     Expr :=
-                       Make_And_Then (Loc,
-                         Left_Opnd  => Relocate_Node (Expr),
-                         Right_Opnd => Relocate_Node (Arg2));
-                  end if;
-               end if;
+      begin
+         Ritem := First_Rep_Item (Typ);
+         while Present (Ritem) loop
+            if Nkind (Ritem) = N_Pragma
+              and then Pragma_Name (Ritem) = Name_Predicate
+            then
+               Add_Predicate (Ritem);
             end if;
 
             Next_Rep_Item (Ritem);
@@ -8555,6 +8568,10 @@ package body Sem_Ch13 is
          end if;
       end Test_RE;
 
+      --  Local variables
+
+      GM : constant Ghost_Mode_Type := Ghost_Mode;
+
    --  Start of processing for Build_Predicate_Functions
 
    begin
@@ -8566,6 +8583,12 @@ package body Sem_Ch13 is
          return;
       end if;
 
+      --  The related type may be subject to pragma Ghost with policy Ignore.
+      --  Set the mode now to ensure that the predicate functions are properly
+      --  flagged as ignored Ghost.
+
+      Set_Ghost_Mode_From_Entity (Typ);
+
       --  Prepare to construct predicate expression
 
       Expr := Empty;
@@ -8670,6 +8693,13 @@ package body Sem_Ch13 is
                Set_Predicate_Function (Full_View (Typ), SId);
             end if;
 
+            --  Mark the predicate function explicitly as Ghost because it does
+            --  not come from source.
+
+            if Ghost_Mode > None then
+               Set_Is_Ghost_Entity (SId);
+            end if;
+
             Spec :=
               Make_Function_Specification (Loc,
                 Defining_Unit_Name       => SId,
@@ -8750,6 +8780,13 @@ package body Sem_Ch13 is
                   Set_Predicate_Function_M (Full_View (Typ), SId);
                end if;
 
+               --  Mark the predicate function explicitly as Ghost because it
+               --  does not come from source.
+
+               if Ghost_Mode > None then
+                  Set_Is_Ghost_Entity (SId);
+               end if;
+
                Spec :=
                  Make_Function_Specification (Loc,
                    Defining_Unit_Name       => SId,
@@ -8896,6 +8933,11 @@ package body Sem_Ch13 is
             end if;
          end;
       end if;
+
+      --  Restore the original Ghost mode once analysis and expansion have
+      --  taken place.
+
+      Ghost_Mode := GM;
    end Build_Predicate_Functions;
 
    -----------------------------------------