]> gcc.gnu.org Git - gcc.git/blobdiff - gcc/ada/sem_ch7.adb
ada: Implement change to SPARK RM rule on state refinement
[gcc.git] / gcc / ada / sem_ch7.adb
index 8c318fddc73d8d9fc3a3540359a9550944c24ca6..284706981d65d2b5a1f339a679ea1b08fb5760e2 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2022, 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- --
 --  handling of private and full declarations, and the construction of dispatch
 --  tables for tagged types.
 
-with Aspects;   use Aspects;
-with Atree;     use Atree;
-with Contracts; use Contracts;
-with Debug;     use Debug;
-with Einfo;     use Einfo;
-with Elists;    use Elists;
-with Errout;    use Errout;
-with Exp_Disp;  use Exp_Disp;
-with Exp_Dist;  use Exp_Dist;
-with Exp_Dbug;  use Exp_Dbug;
-with Ghost;     use Ghost;
-with Lib;       use Lib;
-with Lib.Xref;  use Lib.Xref;
-with Namet;     use Namet;
-with Nmake;     use Nmake;
-with Nlists;    use Nlists;
-with Opt;       use Opt;
-with Output;    use Output;
-with Restrict;  use Restrict;
-with Rtsfind;   use Rtsfind;
-with Sem;       use Sem;
-with Sem_Aux;   use Sem_Aux;
-with Sem_Cat;   use Sem_Cat;
-with Sem_Ch3;   use Sem_Ch3;
-with Sem_Ch6;   use Sem_Ch6;
-with Sem_Ch8;   use Sem_Ch8;
-with Sem_Ch10;  use Sem_Ch10;
-with Sem_Ch12;  use Sem_Ch12;
-with Sem_Ch13;  use Sem_Ch13;
-with Sem_Disp;  use Sem_Disp;
-with Sem_Eval;  use Sem_Eval;
-with Sem_Prag;  use Sem_Prag;
-with Sem_Util;  use Sem_Util;
-with Sem_Warn;  use Sem_Warn;
-with Snames;    use Snames;
-with Stand;     use Stand;
-with Sinfo;     use Sinfo;
-with Sinput;    use Sinput;
+with Aspects;        use Aspects;
+with Atree;          use Atree;
+with Contracts;      use Contracts;
+with Debug;          use Debug;
+with Einfo;          use Einfo;
+with Einfo.Entities; use Einfo.Entities;
+with Einfo.Utils;    use Einfo.Utils;
+with Elists;         use Elists;
+with Errout;         use Errout;
+with Exp_Disp;       use Exp_Disp;
+with Exp_Dist;       use Exp_Dist;
+with Exp_Dbug;       use Exp_Dbug;
+with Freeze;         use Freeze;
+with Ghost;          use Ghost;
+with Lib;            use Lib;
+with Lib.Xref;       use Lib.Xref;
+with Namet;          use Namet;
+with Nmake;          use Nmake;
+with Nlists;         use Nlists;
+with Opt;            use Opt;
+with Output;         use Output;
+with Rtsfind;        use Rtsfind;
+with Sem;            use Sem;
+with Sem_Aux;        use Sem_Aux;
+with Sem_Cat;        use Sem_Cat;
+with Sem_Ch3;        use Sem_Ch3;
+with Sem_Ch6;        use Sem_Ch6;
+with Sem_Ch8;        use Sem_Ch8;
+with Sem_Ch10;       use Sem_Ch10;
+with Sem_Ch12;       use Sem_Ch12;
+with Sem_Ch13;       use Sem_Ch13;
+with Sem_Disp;       use Sem_Disp;
+with Sem_Eval;       use Sem_Eval;
+with Sem_Prag;       use Sem_Prag;
+with Sem_Util;       use Sem_Util;
+with Sem_Warn;       use Sem_Warn;
+with Snames;         use Snames;
+with Stand;          use Stand;
+with Sinfo;          use Sinfo;
+with Sinfo.Nodes;    use Sinfo.Nodes;
+with Sinfo.Utils;    use Sinfo.Utils;
+with Sinput;         use Sinput;
 with Style;
-with Uintp;     use Uintp;
+with Uintp;          use Uintp;
+with Warnsw;         use Warnsw;
+
+with GNAT.HTable;
 
 package body Sem_Ch7 is
 
@@ -186,17 +193,63 @@ package body Sem_Ch7 is
       end if;
    end Analyze_Package_Body;
 
+   ------------------------------------------------------
+   -- Analyze_Package_Body_Helper Data and Subprograms --
+   ------------------------------------------------------
+
+   Entity_Table_Size : constant := 4093;
+   --  Number of headers in hash table
+
+   subtype Entity_Header_Num is Integer range 0 .. Entity_Table_Size - 1;
+   --  Range of headers in hash table
+
+   function Node_Hash (Id : Entity_Id) return Entity_Header_Num;
+   --  Simple hash function for Entity_Ids
+
+   package Subprogram_Table is new GNAT.Htable.Simple_HTable
+     (Header_Num => Entity_Header_Num,
+      Element    => Boolean,
+      No_Element => False,
+      Key        => Entity_Id,
+      Hash       => Node_Hash,
+      Equal      => "=");
+   --  Hash table to record which subprograms are referenced. It is declared
+   --  at library level to avoid elaborating it for every call to Analyze.
+
+   package Traversed_Table is new GNAT.Htable.Simple_HTable
+     (Header_Num => Entity_Header_Num,
+      Element    => Boolean,
+      No_Element => False,
+      Key        => Node_Id,
+      Hash       => Node_Hash,
+      Equal      => "=");
+   --  Hash table to record which nodes we have traversed, so we can avoid
+   --  traversing the same nodes repeatedly.
+
+   -----------------
+   -- Node_Hash --
+   -----------------
+
+   function Node_Hash (Id : Entity_Id) return Entity_Header_Num is
+   begin
+      return Entity_Header_Num (Id mod Entity_Table_Size);
+   end Node_Hash;
+
    ---------------------------------
    -- Analyze_Package_Body_Helper --
    ---------------------------------
 
+   --  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.
+
    procedure Analyze_Package_Body_Helper (N : Node_Id) is
       procedure Hide_Public_Entities (Decls : List_Id);
       --  Attempt to hide all public entities found in declarative list Decls
       --  by resetting their Is_Public flag to False depending on whether the
       --  entities are not referenced by inlined or generic bodies. This kind
-      --  of processing is a conservative approximation and may still leave
-      --  certain entities externally visible.
+      --  of processing is a conservative approximation and will still leave
+      --  entities externally visible if the package is not simple enough.
 
       procedure Install_Composite_Operations (P : Entity_Id);
       --  Composite types declared in the current scope may depend on types
@@ -209,108 +262,89 @@ package body Sem_Ch7 is
       --------------------------
 
       procedure Hide_Public_Entities (Decls : List_Id) is
-         function Contains_Subp_Or_Const_Refs (N : Node_Id) return Boolean;
-         --  Subsidiary to routine Has_Referencer. Determine whether a node
-         --  contains a reference to a subprogram or a non-static constant.
-         --  WARNING: this is a very expensive routine as it performs a full
-         --  tree traversal.
-
          function Has_Referencer
-           (Decls     : List_Id;
-            Top_Level : Boolean := False) return Boolean;
+           (Decls                                   : List_Id;
+            In_Nested_Instance                      : Boolean;
+            Has_Outer_Referencer_Of_Non_Subprograms : Boolean) return Boolean;
          --  A "referencer" is a construct which may reference a previous
          --  declaration. Examine all declarations in list Decls in reverse
-         --  and determine whether once such referencer exists. All entities
+         --  and determine whether one such referencer exists. All entities
          --  in the range Last (Decls) .. Referencer are hidden from external
-         --  visibility.
-
-         ---------------------------------
-         -- Contains_Subp_Or_Const_Refs --
-         ---------------------------------
-
-         function Contains_Subp_Or_Const_Refs (N : Node_Id) return Boolean is
-            Reference_Seen : Boolean := False;
-
-            function Is_Subp_Or_Const_Ref
-              (N : Node_Id) return Traverse_Result;
-            --  Determine whether a node denotes a reference to a subprogram or
-            --  a non-static constant.
-
-            --------------------------
-            -- Is_Subp_Or_Const_Ref --
-            --------------------------
-
-            function Is_Subp_Or_Const_Ref
-              (N : Node_Id) return Traverse_Result
-            is
-               Val : Node_Id;
-
-            begin
-               --  Detect a reference of the form
-               --    Subp_Call
-
-               if Nkind (N) in N_Subprogram_Call
-                 and then Is_Entity_Name (Name (N))
-               then
-                  Reference_Seen := True;
-                  return Abandon;
-
-               --  Detect a reference of the form
-               --    Subp'Some_Attribute
-
-               elsif Nkind (N) = N_Attribute_Reference
-                 and then Is_Entity_Name (Prefix (N))
-                 and then Present (Entity (Prefix (N)))
-                 and then Is_Subprogram (Entity (Prefix (N)))
-               then
-                  Reference_Seen := True;
-                  return Abandon;
-
-               --  Detect the use of a non-static constant
+         --  visibility. In_Nested_Instance is true if we are inside a package
+         --  instance that has a body.
 
-               elsif Is_Entity_Name (N)
-                 and then Present (Entity (N))
-                 and then Ekind (Entity (N)) = E_Constant
-               then
-                  Val := Constant_Value (Entity (N));
+         function Scan_Subprogram_Ref (N : Node_Id) return Traverse_Result;
+         --  Determine whether a node denotes a reference to a subprogram
 
-                  if Present (Val)
-                    and then not Compile_Time_Known_Value (Val)
-                  then
-                     Reference_Seen := True;
-                     return Abandon;
-                  end if;
-               end if;
-
-               return OK;
-            end Is_Subp_Or_Const_Ref;
-
-            procedure Find_Subp_Or_Const_Ref is
-              new Traverse_Proc (Is_Subp_Or_Const_Ref);
-
-         --  Start of processing for Contains_Subp_Or_Const_Refs
-
-         begin
-            Find_Subp_Or_Const_Ref (N);
+         procedure Traverse_And_Scan_Subprogram_Refs is
+           new Traverse_Proc (Scan_Subprogram_Ref);
+         --  Subsidiary to routine Has_Referencer. Determine whether a node
+         --  contains references to a subprogram and record them.
+         --  WARNING: this is a very expensive routine as it performs a full
+         --  tree traversal.
 
-            return Reference_Seen;
-         end Contains_Subp_Or_Const_Refs;
+         procedure Scan_Subprogram_Refs (Node : Node_Id);
+         --  If we haven't already traversed Node, then mark and traverse it.
 
          --------------------
          -- Has_Referencer --
          --------------------
 
          function Has_Referencer
-           (Decls     : List_Id;
-            Top_Level : Boolean := False) return Boolean
+           (Decls                                   : List_Id;
+            In_Nested_Instance                      : Boolean;
+            Has_Outer_Referencer_Of_Non_Subprograms : Boolean) return Boolean
          is
-            Decl    : Node_Id;
-            Decl_Id : Entity_Id;
-            Spec    : Node_Id;
+            Has_Referencer_Of_Non_Subprograms : Boolean :=
+                                       Has_Outer_Referencer_Of_Non_Subprograms;
+            --  Set if an inlined subprogram body was detected as a referencer.
+            --  In this case, we do not return True immediately but keep hiding
+            --  subprograms from external visibility.
+
+            Decl        : Node_Id;
+            Decl_Id     : Entity_Id;
+            In_Instance : Boolean;
+            Spec        : Node_Id;
+            Ignore      : Boolean;
+
+            function Set_Referencer_Of_Non_Subprograms return Boolean;
+            --  Set Has_Referencer_Of_Non_Subprograms and call
+            --  Scan_Subprogram_Refs if relevant.
+            --  Return whether Scan_Subprogram_Refs was called.
+
+            ---------------------------------------
+            -- Set_Referencer_Of_Non_Subprograms --
+            ---------------------------------------
+
+            function Set_Referencer_Of_Non_Subprograms return Boolean is
+            begin
+               --  An inlined subprogram body acts as a referencer
+               --  unless we generate C code since inlining is then
+               --  handled by the C compiler.
+
+               --  Note that we test Has_Pragma_Inline here in addition
+               --  to Is_Inlined. We are doing this for a client, since
+               --  we are computing which entities should be public, and
+               --  it is the client who will decide if actual inlining
+               --  should occur, so we need to catch all cases where the
+               --  subprogram may be inlined by the client.
+
+               if (not CCG_Mode or else Has_Pragma_Inline_Always (Decl_Id))
+                 and then (Is_Inlined (Decl_Id)
+                            or else Has_Pragma_Inline (Decl_Id))
+               then
+                  Has_Referencer_Of_Non_Subprograms := True;
 
-            Has_Non_Subp_Const_Referencer : Boolean := False;
-            --  Flag set for inlined subprogram bodies that do not contain
-            --  references to other subprograms or non-static constants.
+                  --  Inspect the statements of the subprogram body
+                  --  to determine whether the body references other
+                  --  subprograms.
+
+                  Scan_Subprogram_Refs (Decl);
+                  return True;
+               else
+                  return False;
+               end if;
+            end Set_Referencer_Of_Non_Subprograms;
 
          begin
             if No (Decls) then
@@ -331,17 +365,31 @@ package body Sem_Ch7 is
 
                --  Package declaration
 
-               elsif Nkind (Decl) = N_Package_Declaration
-                 and then not Has_Non_Subp_Const_Referencer
-               then
+               elsif Nkind (Decl) = N_Package_Declaration then
                   Spec := Specification (Decl);
+                  Decl_Id := Defining_Entity (Spec);
 
                   --  Inspect the declarations of a non-generic package to try
                   --  and hide more entities from external visibility.
 
-                  if not Is_Generic_Unit (Defining_Entity (Spec)) then
-                     if Has_Referencer (Private_Declarations (Spec))
-                       or else Has_Referencer (Visible_Declarations (Spec))
+                  if not Is_Generic_Unit (Decl_Id) then
+                     if In_Nested_Instance then
+                        In_Instance := True;
+                     elsif Is_Generic_Instance (Decl_Id) then
+                        In_Instance :=
+                          Has_Completion (Decl_Id)
+                            or else Unit_Requires_Body (Generic_Parent (Spec));
+                     else
+                        In_Instance := False;
+                     end if;
+
+                     if Has_Referencer (Private_Declarations (Spec),
+                                        In_Instance,
+                                        Has_Referencer_Of_Non_Subprograms)
+                       or else
+                        Has_Referencer (Visible_Declarations (Spec),
+                                        In_Instance,
+                                        Has_Referencer_Of_Non_Subprograms)
                      then
                         return True;
                      end if;
@@ -370,8 +418,11 @@ package body Sem_Ch7 is
                   --  Inspect the declarations of a non-generic package body to
                   --  try and hide more entities from external visibility.
 
-                  elsif not Has_Non_Subp_Const_Referencer
-                    and then Has_Referencer (Declarations (Decl))
+                  elsif Has_Referencer (Declarations (Decl),
+                                        In_Nested_Instance
+                                          or else
+                                        Is_Generic_Instance (Decl_Id),
+                                        Has_Referencer_Of_Non_Subprograms)
                   then
                      return True;
                   end if;
@@ -388,87 +439,177 @@ package body Sem_Ch7 is
                         return True;
                      end if;
 
-                     --  An inlined subprogram body acts as a referencer
-
-                     if Is_Inlined (Decl_Id)
-                       or else Has_Pragma_Inline (Decl_Id)
-                     then
-                        --  Inspect the statements of the subprogram body
-                        --  to determine whether the body references other
-                        --  subprograms and/or non-static constants.
-
-                        if Top_Level
-                          and then not Contains_Subp_Or_Const_Refs (Decl)
-                        then
-                           Has_Non_Subp_Const_Referencer := True;
-                        else
-                           return True;
-                        end if;
-                     end if;
+                     Ignore := Set_Referencer_Of_Non_Subprograms;
 
                   --  Otherwise this is a stand alone subprogram body
 
                   else
                      Decl_Id := Defining_Entity (Decl);
 
-                     --  An inlined body acts as a referencer. Note that an
-                     --  inlined subprogram remains Is_Public as gigi requires
-                     --  the flag to be set.
-
-                     --  Note that we test Has_Pragma_Inline here rather than
-                     --  Is_Inlined. We are compiling this for a client, and
-                     --  it is the client who will decide if actual inlining
-                     --  should occur, so we need to assume that the procedure
-                     --  could be inlined for the purpose of accessing global
-                     --  entities.
-
-                     if Has_Pragma_Inline (Decl_Id) then
-                        if Top_Level
-                          and then not Contains_Subp_Or_Const_Refs (Decl)
-                        then
-                           Has_Non_Subp_Const_Referencer := True;
-                        else
-                           return True;
-                        end if;
-                     else
+                     if not Set_Referencer_Of_Non_Subprograms
+                       and then not Subprogram_Table.Get (Decl_Id)
+                     then
+                        --  We can reset Is_Public right away
                         Set_Is_Public (Decl_Id, False);
                      end if;
                   end if;
 
+               --  Freeze node
+
+               elsif Nkind (Decl) = N_Freeze_Entity then
+                  declare
+                     Discard : Boolean;
+                     pragma Unreferenced (Discard);
+                  begin
+                     --  Inspect the actions to find references to subprograms.
+                     --  We assume that the actions do not contain other kinds
+                     --  of references and, therefore, we do not stop the scan
+                     --  or set Has_Referencer_Of_Non_Subprograms here. Doing
+                     --  it would pessimize common cases for which the actions
+                     --  contain the declaration of an init procedure, since
+                     --  such a procedure is automatically marked inline.
+
+                     Discard :=
+                       Has_Referencer (Actions (Decl),
+                                       In_Nested_Instance,
+                                       Has_Referencer_Of_Non_Subprograms);
+                  end;
+
                --  Exceptions, objects and renamings do not need to be public
                --  if they are not followed by a construct which can reference
-               --  and export them. The Is_Public flag is reset on top level
-               --  entities only as anything nested is local to its context.
-
-               elsif Nkind_In (Decl, N_Exception_Declaration,
-                                     N_Object_Declaration,
-                                     N_Object_Renaming_Declaration,
-                                     N_Subprogram_Declaration,
-                                     N_Subprogram_Renaming_Declaration)
+               --  and export them.
+
+               elsif Nkind (Decl) in N_Exception_Declaration
+                                   | N_Object_Declaration
+                                   | N_Object_Renaming_Declaration
                then
                   Decl_Id := Defining_Entity (Decl);
 
-                  if Top_Level
+                  --  We cannot say anything for objects declared in nested
+                  --  instances because instantiations are not done yet so the
+                  --  bodies are not visible and could contain references to
+                  --  them.
+
+                  if not In_Nested_Instance
                     and then not Is_Imported (Decl_Id)
                     and then not Is_Exported (Decl_Id)
                     and then No (Interface_Name (Decl_Id))
-                    and then
-                      (not Has_Non_Subp_Const_Referencer
-                        or else Nkind (Decl) = N_Subprogram_Declaration)
+                    and then not Has_Referencer_Of_Non_Subprograms
                   then
                      Set_Is_Public (Decl_Id, False);
                   end if;
+
+               --  Likewise for subprograms and renamings, but we work harder
+               --  for them to see whether they are referenced on an individual
+               --  basis by looking into the table of referenced subprograms.
+
+               elsif Nkind (Decl) in N_Subprogram_Declaration
+                                   | N_Subprogram_Renaming_Declaration
+               then
+                  Decl_Id := Defining_Entity (Decl);
+
+                  --  We cannot say anything for subprograms declared in nested
+                  --  instances because instantiations are not done yet so the
+                  --  bodies are not visible and could contain references to
+                  --  them, except if we still have no subprograms at all which
+                  --  are referenced by an inlined body.
+
+                  if (not In_Nested_Instance
+                       or else not Subprogram_Table.Get_First)
+                    and then not Is_Imported (Decl_Id)
+                    and then not Is_Exported (Decl_Id)
+                    and then No (Interface_Name (Decl_Id))
+                    and then not Subprogram_Table.Get (Decl_Id)
+                  then
+                     Set_Is_Public (Decl_Id, False);
+                  end if;
+
+                  --  For a subprogram renaming, if the entity is referenced,
+                  --  then so is the renamed subprogram. But there is an issue
+                  --  with generic bodies because instantiations are not done
+                  --  yet and, therefore, cannot be scanned for referencers.
+                  --  That's why we use an approximation and test that we have
+                  --  at least one subprogram referenced by an inlined body
+                  --  instead of precisely the entity of this renaming.
+
+                  if Nkind (Decl) = N_Subprogram_Renaming_Declaration
+                    and then Subprogram_Table.Get_First
+                    and then Is_Entity_Name (Name (Decl))
+                    and then Present (Entity (Name (Decl)))
+                    and then Is_Subprogram (Entity (Name (Decl)))
+                  then
+                     Subprogram_Table.Set (Entity (Name (Decl)), True);
+                  end if;
                end if;
 
                Prev (Decl);
             end loop;
 
-            return Has_Non_Subp_Const_Referencer;
+            return Has_Referencer_Of_Non_Subprograms;
          end Has_Referencer;
 
+         -------------------------
+         -- Scan_Subprogram_Ref --
+         -------------------------
+
+         function Scan_Subprogram_Ref (N : Node_Id) return Traverse_Result is
+         begin
+            --  Detect a reference of the form
+            --    Subp_Call
+
+            if Nkind (N) in N_Subprogram_Call
+              and then Is_Entity_Name (Name (N))
+              and then Present (Entity (Name (N)))
+              and then Is_Subprogram (Entity (Name (N)))
+            then
+               Subprogram_Table.Set (Entity (Name (N)), True);
+
+            --  Detect a reference of the form
+            --    Subp'Some_Attribute
+
+            elsif Nkind (N) = N_Attribute_Reference
+              and then Is_Entity_Name (Prefix (N))
+              and then Present (Entity (Prefix (N)))
+              and then Is_Subprogram (Entity (Prefix (N)))
+            then
+               Subprogram_Table.Set (Entity (Prefix (N)), True);
+
+            --  Constants can be substituted by their value in gigi, which may
+            --  contain a reference, so scan the value recursively.
+
+            elsif Is_Entity_Name (N)
+              and then Present (Entity (N))
+              and then Ekind (Entity (N)) = E_Constant
+            then
+               declare
+                  Val : constant Node_Id := Constant_Value (Entity (N));
+               begin
+                  if Present (Val)
+                    and then not Compile_Time_Known_Value (Val)
+                  then
+                     Scan_Subprogram_Refs (Val);
+                  end if;
+               end;
+            end if;
+
+            return OK;
+         end Scan_Subprogram_Ref;
+
+         --------------------------
+         -- Scan_Subprogram_Refs --
+         --------------------------
+
+         procedure Scan_Subprogram_Refs (Node : Node_Id) is
+         begin
+            if not Traversed_Table.Get (Node) then
+               Traversed_Table.Set (Node, True);
+               Traverse_And_Scan_Subprogram_Refs (Node);
+            end if;
+         end Scan_Subprogram_Refs;
+
          --  Local variables
 
-         Discard : Boolean := True;
+         Discard : Boolean;
          pragma Unreferenced (Discard);
 
       --  Start of processing for Hide_Public_Entities
@@ -506,7 +647,39 @@ package body Sem_Ch7 is
          --  not always be the case. The algorithm takes a conservative stance
          --  and leaves entity External_Obj public.
 
-         Discard := Has_Referencer (Decls, Top_Level => True);
+         --  This very conservative algorithm is supplemented by a more precise
+         --  processing for inlined bodies. For them, we traverse the syntactic
+         --  tree and record which subprograms are actually referenced from it.
+         --  This makes it possible to compute a much smaller set of externally
+         --  visible subprograms in the absence of generic bodies, which can
+         --  have a significant impact on the inlining decisions made in the
+         --  back end and the removal of out-of-line bodies from the object
+         --  code. We do it only for inlined bodies because they are supposed
+         --  to be reasonably small and tree traversal is very expensive.
+
+         --  Note that even this special processing is not optimal for inlined
+         --  bodies, because we treat all inlined subprograms alike. An optimal
+         --  algorithm would require computing the transitive closure of the
+         --  inlined subprograms that can really be referenced from other units
+         --  in the source code.
+
+         --  We could extend this processing for inlined bodies and record all
+         --  entities, not just subprograms, referenced from them, which would
+         --  make it possible to compute a much smaller set of all externally
+         --  visible entities in the absence of generic bodies. But this would
+         --  mean implementing a more thorough tree traversal of the bodies,
+         --  i.e. not just syntactic, and the gain would very likely be worth
+         --  neither the hassle nor the slowdown of the compiler.
+
+         --  Finally, an important thing to be aware of is that, at this point,
+         --  instantiations are not done yet so we cannot directly see inlined
+         --  bodies coming from them. That's not catastrophic because only the
+         --  actual parameters of the instantiations matter here, and they are
+         --  present in the declarations list of the instantiated packages.
+
+         Traversed_Table.Reset;
+         Subprogram_Table.Reset;
+         Discard := Has_Referencer (Decls, False, False);
       end Hide_Public_Entities;
 
       ----------------------------------
@@ -534,7 +707,13 @@ package body Sem_Ch7 is
 
       --  Local variables
 
-      Save_Ghost_Mode  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_GM   : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR  : constant Node_Id         := Ignored_Ghost_Region;
+      Saved_EA   : constant Boolean         := Expander_Active;
+      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;
@@ -596,13 +775,15 @@ package body Sem_Ch7 is
                  ("optional package body (not allowed in Ada 95)??", N);
             else
                Error_Msg_N ("spec of this package does not allow a body", N);
+               Error_Msg_N ("\either remove the body or add pragma "
+                            & "Elaborate_Body in the spec", N);
             end if;
          end if;
       end if;
 
-      --  A [generic] package body "freezes" the contract of the nearest
-      --  enclosing package body and all other contracts encountered in the
-      --  same declarative part up to and excluding the package body:
+      --  A [generic] package body freezes the contract of the nearest
+      --  enclosing package body and all other contracts encountered in
+      --  the same declarative part up to and excluding the package body:
 
       --    package body Nearest_Enclosing_Package
       --      with Refined_State => (State => Constit)
@@ -619,28 +800,46 @@ package body Sem_Ch7 is
 
       --  This ensures that any annotations referenced by the contract of a
       --  [generic] subprogram body declared within the current package body
-      --  are available. This form of "freezing" is decoupled from the usual
+      --  are available. This form of freezing is decoupled from the usual
       --  Freeze_xxx mechanism because it must also work in the context of
       --  generics where normal freezing is disabled.
 
-      --  Only bodies coming from source should cause this type of "freezing".
+      --  Only bodies coming from source should cause this type of freezing.
       --  Instantiated generic bodies are excluded because their processing is
       --  performed in a separate compilation pass which lacks enough semantic
       --  information with respect to contract analysis. It is safe to suppress
-      --  the "freezing" of contracts in this case because this action already
+      --  the freezing of contracts in this case because this action already
       --  took place at the end of the enclosing declarative part.
 
       if Comes_From_Source (N)
         and then not Is_Generic_Instance (Spec_Id)
       then
-         Analyze_Previous_Contracts (N);
+         Freeze_Previous_Contracts (N);
       end if;
 
       --  A package body is Ghost when the corresponding spec is Ghost. Set
       --  the mode now to ensure that any nodes generated during analysis and
       --  expansion are properly flagged as ignored Ghost.
 
-      Set_Ghost_Mode (N, Spec_Id);
+      Mark_And_Set_Ghost_Body (N, Spec_Id);
+
+      --  Deactivate expansion inside the body of ignored Ghost entities,
+      --  as this code will ultimately be ignored. This avoids requiring the
+      --  presence of run-time units which are not needed. Only do this for
+      --  user entities, as internally generated entities might still need
+      --  to be expanded (e.g. those generated for types).
+
+      if Present (Ignored_Ghost_Region)
+        and then Comes_From_Source (Body_Id)
+      then
+         Expander_Active := False;
+      end if;
+
+      --  If the body completes the initial declaration of a compilation unit
+      --  which is subject to pragma Elaboration_Checks, set the model of the
+      --  pragma because it applies to all parts of the unit.
+
+      Install_Elaboration_Model (Spec_Id);
 
       Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
       Style.Check_Identifier (Body_Id, Spec_Id);
@@ -662,7 +861,7 @@ package body Sem_Ch7 is
          --  unannotated body will be used in all instantiations.
 
          Body_Id := Defining_Entity (N);
-         Set_Ekind (Body_Id, E_Package_Body);
+         Mutate_Ekind (Body_Id, E_Package_Body);
          Set_Scope (Body_Id, Scope (Spec_Id));
          Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
          Set_Body_Entity (Spec_Id, Body_Id);
@@ -694,7 +893,7 @@ package body Sem_Ch7 is
       --  current node otherwise. Note that N was rewritten above, so we must
       --  be sure to get the latest Body_Id value.
 
-      Set_Ekind (Body_Id, E_Package_Body);
+      Mutate_Ekind (Body_Id, E_Package_Body);
       Set_Body_Entity (Spec_Id, Body_Id);
       Set_Spec_Entity (Body_Id, Spec_Id);
 
@@ -733,19 +932,14 @@ package body Sem_Ch7 is
          Set_SPARK_Aux_Pragma           (Body_Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited     (Body_Id);
          Set_SPARK_Aux_Pragma_Inherited (Body_Id);
-      end if;
-
-      --  Inherit the "ghostness" of the package spec. Note that this property
-      --  is not directly inherited as the body may be subject to a different
-      --  Ghost assertion policy.
-
-      if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then
-         Set_Is_Ghost_Entity (Body_Id);
 
-         --  The Ghost policy in effect at the point of declaration and at the
-         --  point of completion must match (SPARK RM 6.9(14)).
+         --  A package body may be instantiated or inlined at a later pass.
+         --  Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when
+         --  it applied to the package spec.
 
-         Check_Ghost_Completion (Spec_Id, Body_Id);
+         if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+         end if;
       end if;
 
       Set_Categorization_From_Pragmas (N);
@@ -767,17 +961,16 @@ package body Sem_Ch7 is
       --  This is a nested package, so it may be necessary to declare certain
       --  inherited subprograms that are not yet visible because the parent
       --  type's subprograms are now visible.
+      --  Note that for child units these operations were generated when
+      --  analyzing the package specification.
 
       if Ekind (Scope (Spec_Id)) = E_Package
         and then Scope (Spec_Id) /= Standard_Standard
+        and then not Is_Child_Unit (Spec_Id)
       then
          Declare_Inherited_Private_Subprograms (Spec_Id);
       end if;
 
-      --  A package body "freezes" the contract of its initial declaration.
-      --  This analysis depends on attribute Corresponding_Spec being set. Only
-      --  bodies coming from source shuld cause this type of "freezing".
-
       if Present (Declarations (N)) then
          Analyze_Declarations (Declarations (N));
          Inspect_Deferred_Constant_Completion (Declarations (N));
@@ -799,6 +992,15 @@ package body Sem_Ch7 is
                  ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
             end if;
 
+         --  SPARK_Mode Off could complete no SPARK_Mode in a generic, either
+         --  as specified in source code, or because SPARK_Mode On is ignored
+         --  in an instance where the context is SPARK_Mode Off/Auto.
+
+         elsif Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = Off
+           and then (Is_Generic_Unit (Spec_Id) or else In_Instance)
+         then
+            null;
+
          else
             Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
             Error_Msg_N ("incorrect application of SPARK_Mode#", N);
@@ -870,6 +1072,7 @@ package body Sem_Ch7 is
          Set_Last_Entity  (Spec_Id, Empty);
       end if;
 
+      Update_Use_Clause_Chain;
       End_Package_Scope (Spec_Id);
 
       --  All entities declared in body are not visible
@@ -908,16 +1111,20 @@ package body Sem_Ch7 is
       --  to the linker as their Is_Public flag is set to True. This proactive
       --  approach is necessary because an inlined or a generic body for which
       --  code is generated in other units may need to see these entities. Cut
-      --  down the number of global symbols that do not neet public visibility
+      --  down the number of global symbols that do not need public visibility
       --  as this has two beneficial effects:
       --    (1) It makes the compilation process more efficient.
-      --    (2) It gives the code generatormore freedom to optimize within each
+      --    (2) It gives the code generator more leeway to optimize within each
       --        unit, especially subprograms.
 
-      --  This is done only for top level library packages or child units as
-      --  the algorithm does a top down traversal of the package body.
+      --  This is done only for top-level library packages or child units as
+      --  the algorithm does a top-down traversal of the package body. This is
+      --  also done for instances because instantiations are still pending by
+      --  the time the enclosing package body is analyzed.
 
-      if (Scope (Spec_Id) = Standard_Standard or else Is_Child_Unit (Spec_Id))
+      if (Scope (Spec_Id) = Standard_Standard
+           or else Is_Child_Unit (Spec_Id)
+           or else Is_Generic_Instance (Spec_Id))
         and then not Is_Generic_Unit (Spec_Id)
       then
          Hide_Public_Entities (Declarations (N));
@@ -939,7 +1146,12 @@ package body Sem_Ch7 is
          end if;
       end if;
 
-      Ghost_Mode := Save_Ghost_Mode;
+      if Present (Ignored_Ghost_Region) then
+         Expander_Active := Saved_EA;
+      end if;
+
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Package_Body_Helper;
 
    ---------------------------------
@@ -948,7 +1160,6 @@ package body Sem_Ch7 is
 
    procedure Analyze_Package_Declaration (N : Node_Id) is
       Id  : constant Node_Id := Defining_Entity (N);
-      Par : constant Node_Id := Parent_Spec (N);
 
       Is_Comp_Unit : constant Boolean :=
                        Nkind (Parent (N)) = N_Compilation_Unit;
@@ -968,26 +1179,23 @@ package body Sem_Ch7 is
 
       Generate_Definition (Id);
       Enter_Name (Id);
-      Set_Ekind  (Id, E_Package);
+      Mutate_Ekind  (Id, E_Package);
       Set_Etype  (Id, Standard_Void_Type);
 
-      --  Set SPARK_Mode from context only for non-generic package
+      --  Set SPARK_Mode from context
 
-      if Ekind (Id) = E_Package then
-         Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
-         Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
-         Set_SPARK_Pragma_Inherited     (Id);
-         Set_SPARK_Aux_Pragma_Inherited (Id);
-      end if;
+      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited     (Id);
+      Set_SPARK_Aux_Pragma_Inherited (Id);
 
-      --  A package declared within a Ghost refion is automatically Ghost. A
-      --  child package is Ghost when its parent is Ghost (SPARK RM 6.9(2)).
+      --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+      --  the body of this package is instantiated or inlined later and out of
+      --  context. The body uses this attribute to restore the value of the
+      --  global flag.
 
-      if Ghost_Mode > None
-        or else (Present (Par)
-                  and then Is_Ghost_Entity (Defining_Entity (Unit (Par))))
-      then
-         Set_Is_Ghost_Entity (Id);
+      if Ignore_SPARK_Mode_Pragmas_In_Instance then
+         Set_Ignore_SPARK_Mode_Pragmas (Id);
       end if;
 
       --  Analyze aspect specifications immediately, since we need to recognize
@@ -1035,27 +1243,32 @@ package body Sem_Ch7 is
          Check_Completion;
 
          --  If the package spec does not require an explicit body, then all
-         --  abstract states declared in nested packages cannot possibly get
-         --  a proper refinement (SPARK RM 7.2.2(3)). This check is performed
-         --  only when the compilation unit is the main unit to allow for
-         --  modular SPARK analysis where packages do not necessarily have
-         --  bodies.
+         --  abstract states declared in nested packages cannot possibly get a
+         --  proper refinement (SPARK RM 7.1.4(4) and SPARK RM 7.2.2(3)). This
+         --  check is performed only when the compilation unit is the main
+         --  unit to allow for modular SPARK analysis where packages do not
+         --  necessarily have bodies.
 
          if Is_Comp_Unit then
             Check_State_Refinements
               (Context      => N,
                Is_Main_Unit => Parent (N) = Cunit (Main_Unit));
          end if;
-      end if;
 
-      if Is_Comp_Unit then
+         --  Warn about references to unset objects, which is straightforward
+         --  for packages with no bodies. For packages with bodies this is more
+         --  complicated, because some of the objects might be set between spec
+         --  and body elaboration, in nested or child packages, etc.
 
-         --  Set Body_Required indication on the compilation unit node, and
-         --  determine whether elaboration warnings may be meaningful on it.
+         Check_References (Id);
+      end if;
 
+      --  Set Body_Required indication on the compilation unit node
+
+      if Is_Comp_Unit then
          Set_Body_Required (Parent (N), Body_Required);
 
-         if not Body_Required then
+         if Legacy_Elaboration_Checks and not Body_Required then
             Set_Suppress_Elaboration_Warnings (Id);
          end if;
       end if;
@@ -1105,19 +1318,14 @@ package body Sem_Ch7 is
       --  private_with_clauses, and remove them at the end of the nested
       --  package.
 
-      procedure Check_One_Tagged_Type_Or_Extension_At_Most;
-      --  Issue an error in SPARK mode if a package specification contains
-      --  more than one tagged type or type extension.
-
-      procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-      --  Clears constant indications (Never_Set_In_Source, Constant_Value, and
-      --  Is_True_Constant) on all variables that are entities of Id, and on
-      --  the chain whose first element is FE. A recursive call is made for all
-      --  packages and generic packages.
+      procedure Clear_Constants (Id : Entity_Id);
+      --  Clears constant indications (Never_Set_In_Source, Constant_Value,
+      --  and Is_True_Constant) on all variables that are entities of Id.
+      --  A recursive call is made for all packages and generic packages.
 
       procedure Generate_Parent_References;
       --  For a child unit, generate references to parent units, for
-      --  GPS navigation purposes.
+      --  GNAT Studio navigation purposes.
 
       function Is_Public_Child (Child, Unit : Entity_Id) return Boolean;
       --  Child and Unit are entities of compilation units. True if Child
@@ -1127,6 +1335,11 @@ package body Sem_Ch7 is
       --  Reject completion of an incomplete or private type declarations
       --  having a known discriminant part by an unchecked union.
 
+      procedure Inspect_Untagged_Record_Completion (Decls : List_Id);
+      --  Find out whether a nonlimited untagged record completion has got a
+      --  primitive equality operator and, if so, make it so that it will be
+      --  used as the predefined operator of the private view of the record.
+
       procedure Install_Parent_Private_Declarations (Inst_Id : Entity_Id);
       --  Given the package entity of a generic package instantiation or
       --  formal package whose corresponding generic is a child unit, installs
@@ -1135,63 +1348,11 @@ package body Sem_Ch7 is
       --  private part rather than being done in Sem_Ch12.Install_Parent
       --  (which is where the parents' visible declarations are installed).
 
-      ------------------------------------------------
-      -- Check_One_Tagged_Type_Or_Extension_At_Most --
-      ------------------------------------------------
-
-      procedure Check_One_Tagged_Type_Or_Extension_At_Most is
-         Previous : Node_Id;
-
-         procedure Check_Decls (Decls : List_Id);
-         --  Check that either Previous is Empty and Decls does not contain
-         --  more than one tagged type or type extension, or Previous is
-         --  already set and Decls contains no tagged type or type extension.
-
-         -----------------
-         -- Check_Decls --
-         -----------------
-
-         procedure Check_Decls (Decls : List_Id) is
-            Decl : Node_Id;
-
-         begin
-            Decl := First (Decls);
-            while Present (Decl) loop
-               if Nkind (Decl) = N_Full_Type_Declaration
-                 and then Is_Tagged_Type (Defining_Identifier (Decl))
-               then
-                  if No (Previous) then
-                     Previous := Decl;
-
-                  else
-                     Error_Msg_Sloc := Sloc (Previous);
-                     Check_SPARK_05_Restriction
-                       ("at most one tagged type or type extension allowed",
-                        "\\ previous declaration#",
-                        Decl);
-                  end if;
-               end if;
-
-               Next (Decl);
-            end loop;
-         end Check_Decls;
-
-      --  Start of processing for Check_One_Tagged_Type_Or_Extension_At_Most
-
-      begin
-         Previous := Empty;
-         Check_Decls (Vis_Decls);
-
-         if Present (Priv_Decls) then
-            Check_Decls (Priv_Decls);
-         end if;
-      end Check_One_Tagged_Type_Or_Extension_At_Most;
-
       ---------------------
       -- Clear_Constants --
       ---------------------
 
-      procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id) is
+      procedure Clear_Constants (Id : Entity_Id) is
          E : Entity_Id;
 
       begin
@@ -1207,9 +1368,9 @@ package body Sem_Ch7 is
          --  package can contain a renaming declaration to itself, and such
          --  renamings are generated automatically within package instances.
 
-         E := FE;
+         E := First_Entity (Id);
          while Present (E) and then E /= Id loop
-            if Is_Assignable (E) then
+            if Ekind (E) = E_Variable then
                Set_Never_Set_In_Source (E, False);
                Set_Is_True_Constant    (E, False);
                Set_Current_Value       (E, Empty);
@@ -1221,8 +1382,7 @@ package body Sem_Ch7 is
                end if;
 
             elsif Is_Package_Or_Generic_Package (E) then
-               Clear_Constants (E, First_Entity (E));
-               Clear_Constants (E, First_Private_Entity (E));
+               Clear_Constants (E);
             end if;
 
             Next_Entity (E);
@@ -1242,8 +1402,8 @@ package body Sem_Ch7 is
          then
             Generate_Reference (Id, Scope (Id), 'k', False);
 
-         elsif not Nkind_In (Unit (Cunit (Main_Unit)), N_Subprogram_Body,
-                                                       N_Subunit)
+         elsif Nkind (Unit (Cunit (Main_Unit))) not in
+                 N_Subprogram_Body | N_Subunit
          then
             --  If current unit is an ancestor of main unit, generate a
             --  reference to its own parent.
@@ -1303,12 +1463,15 @@ package body Sem_Ch7 is
          Decl := First (Decls);
          while Present (Decl) loop
 
-            --  We are looking at an incomplete or private type declaration
+            --  We are looking for an incomplete or private type declaration
             --  with a known_discriminant_part whose full view is an
-            --  Unchecked_Union.
+            --  Unchecked_Union. The seemingly useless check with Is_Type
+            --  prevents cascaded errors when routines defined only for type
+            --  entities are called with non-type entities.
 
-            if Nkind_In (Decl, N_Incomplete_Type_Declaration,
-                               N_Private_Type_Declaration)
+            if Nkind (Decl) in N_Incomplete_Type_Declaration
+                             | N_Private_Type_Declaration
+              and then Is_Type (Defining_Identifier (Decl))
               and then Has_Discriminants (Defining_Identifier (Decl))
               and then Present (Full_View (Defining_Identifier (Decl)))
               and then
@@ -1324,6 +1487,103 @@ package body Sem_Ch7 is
          end loop;
       end Inspect_Unchecked_Union_Completion;
 
+      ----------------------------------------
+      -- Inspect_Untagged_Record_Completion --
+      ----------------------------------------
+
+      procedure Inspect_Untagged_Record_Completion (Decls : List_Id) is
+         Decl : Node_Id;
+
+      begin
+         Decl := First (Decls);
+         while Present (Decl) loop
+
+            --  We are looking for a full type declaration of an untagged
+            --  record with a private declaration and primitive operations.
+
+            if Nkind (Decl) in N_Full_Type_Declaration
+              and then Is_Record_Type (Defining_Identifier (Decl))
+              and then not Is_Limited_Type (Defining_Identifier (Decl))
+              and then not Is_Tagged_Type (Defining_Identifier (Decl))
+              and then Has_Private_Declaration (Defining_Identifier (Decl))
+              and then Has_Primitive_Operations (Defining_Identifier (Decl))
+            then
+               declare
+                  Prim_List : constant Elist_Id :=
+                     Collect_Primitive_Operations (Defining_Identifier (Decl));
+
+                  E       : Entity_Id;
+                  Ne_Id   : Entity_Id;
+                  Op_Decl : Node_Id;
+                  Op_Id   : Entity_Id;
+                  Prim    : Elmt_Id;
+
+               begin
+                  Prim := First_Elmt (Prim_List);
+                  while Present (Prim) loop
+                     Op_Id   := Node (Prim);
+                     Op_Decl := Declaration_Node (Op_Id);
+                     if Nkind (Op_Decl) in N_Subprogram_Specification then
+                        Op_Decl := Parent (Op_Decl);
+                     end if;
+
+                     --  We are looking for an equality operator immediately
+                     --  visible and declared in the private part followed by
+                     --  the synthesized inequality operator.
+
+                     if Is_User_Defined_Equality (Op_Id)
+                       and then Is_Immediately_Visible (Op_Id)
+                       and then List_Containing (Op_Decl) = Decls
+                     then
+                        Ne_Id := Next_Entity (Op_Id);
+                        pragma Assert (Ekind (Ne_Id) = E_Function
+                          and then Corresponding_Equality (Ne_Id) = Op_Id);
+
+                        E := First_Private_Entity (Id);
+
+                        --  Move them from the private part of the entity list
+                        --  up to the end of the visible part of the same list.
+
+                        Remove_Entity (Op_Id);
+                        Remove_Entity (Ne_Id);
+
+                        Link_Entities (Prev_Entity (E), Op_Id);
+                        Link_Entities (Op_Id, Ne_Id);
+                        Link_Entities (Ne_Id, E);
+
+                        --  And if the private part contains another equality
+                        --  operator, move the equality operator to after it
+                        --  in the homonym chain, so that all its next homonyms
+                        --  in the same scope, if any, also are in the visible
+                        --  part. This is relied upon to resolve expanded names
+                        --  in Collect_Interps for example.
+
+                        while Present (E) loop
+                           exit when Ekind (E) = E_Function
+                             and then Chars (E) = Name_Op_Eq;
+
+                           Next_Entity (E);
+                        end loop;
+
+                        if Present (E) then
+                           Remove_Homonym (Op_Id);
+
+                           Set_Homonym (Op_Id, Homonym (E));
+                           Set_Homonym (E, Op_Id);
+                        end if;
+
+                        exit;
+                     end if;
+
+                     Next_Elmt (Prim);
+                  end loop;
+               end;
+            end if;
+
+            Next (Decl);
+         end loop;
+      end Inspect_Untagged_Record_Completion;
+
       -----------------------------------------
       -- Install_Parent_Private_Declarations --
       -----------------------------------------
@@ -1339,10 +1599,10 @@ package body Sem_Ch7 is
          Gen_Par :=
            Generic_Parent (Specification (Unit_Declaration_Node (Inst_Par)));
          while Present (Gen_Par) and then Is_Child_Unit (Gen_Par) loop
-            Inst_Node := Get_Package_Instantiation_Node (Inst_Par);
+            Inst_Node := Get_Unit_Instantiation_Node (Inst_Par);
 
-            if Nkind_In (Inst_Node, N_Package_Instantiation,
-                                    N_Formal_Package_Declaration)
+            if Nkind (Inst_Node) in
+                 N_Package_Instantiation | N_Formal_Package_Declaration
               and then Nkind (Name (Inst_Node)) = N_Expanded_Name
             then
                Inst_Par := Entity (Prefix (Name (Inst_Node)));
@@ -1351,9 +1611,21 @@ package body Sem_Ch7 is
                   Inst_Par := Renamed_Entity (Inst_Par);
                end if;
 
-               Gen_Par :=
-                 Generic_Parent
-                   (Specification (Unit_Declaration_Node (Inst_Par)));
+               --  The instance may appear in a sibling generic unit, in
+               --  which case the prefix must include the common (generic)
+               --  ancestor, which is treated as a current instance.
+
+               if Inside_A_Generic
+                 and then Ekind (Inst_Par) = E_Generic_Package
+               then
+                  Gen_Par := Inst_Par;
+                  pragma Assert (In_Open_Scopes (Gen_Par));
+
+               else
+                  Gen_Par :=
+                    Generic_Parent
+                      (Specification (Unit_Declaration_Node (Inst_Par)));
+               end if;
 
                --  Install the private declarations and private use clauses
                --  of a parent instance of the child instance, unless the
@@ -1391,7 +1663,7 @@ package body Sem_Ch7 is
                --  If one of the non-generic parents is itself on the scope
                --  stack, do not install its private declarations: they are
                --  installed in due time when the private part of that parent
-               --  is analyzed. This is delicate ???
+               --  is analyzed.
 
                else
                   while Present (Inst_Par)
@@ -1399,11 +1671,20 @@ package body Sem_Ch7 is
                     and then (not In_Open_Scopes (Inst_Par)
                                or else not In_Private_Part (Inst_Par))
                   loop
-                     Install_Private_Declarations (Inst_Par);
-                     Set_Use (Private_Declarations
-                                (Specification
-                                   (Unit_Declaration_Node (Inst_Par))));
-                     Inst_Par := Scope (Inst_Par);
+                     if Nkind (Inst_Node) = N_Formal_Package_Declaration
+                       or else
+                         not Is_Ancestor_Package
+                               (Inst_Par, Cunit_Entity (Current_Sem_Unit))
+                     then
+                        Install_Private_Declarations (Inst_Par);
+                        Set_Use
+                          (Private_Declarations
+                            (Specification
+                              (Unit_Declaration_Node (Inst_Par))));
+                        Inst_Par := Scope (Inst_Par);
+                     else
+                        exit;
+                     end if;
                   end loop;
 
                   exit;
@@ -1431,49 +1712,23 @@ package body Sem_Ch7 is
 
          --  Check on incomplete types
 
-         --  AI05-0213: A formal incomplete type has no completion
+         --  AI05-0213: A formal incomplete type has no completion, and neither
+         --  does the corresponding subtype in an instance.
 
-         if Ekind (E) = E_Incomplete_Type
+         if Is_Incomplete_Type (E)
            and then No (Full_View (E))
            and then not Is_Generic_Type (E)
+           and then not From_Limited_With (E)
+           and then not Is_Generic_Actual_Type (E)
          then
             Error_Msg_N ("no declaration in visible part for incomplete}", E);
          end if;
 
-         if Is_Type (E) then
-
-            --  Each private type subject to pragma Default_Initial_Condition
-            --  declares a specialized procedure which verifies the assumption
-            --  of the pragma. The declaration appears in the visible part of
-            --  the package to allow for being called from the outside.
-
-            if Has_Default_Init_Cond (E) then
-               Build_Default_Init_Cond_Procedure_Declaration (E);
-
-            --  A private extension inherits the default initial condition
-            --  procedure from its parent type.
-
-            elsif Has_Inherited_Default_Init_Cond (E) then
-               Inherit_Default_Init_Cond_Procedure (E);
-            end if;
-
-            --  If invariants are present, build the invariant procedure for a
-            --  private type, but not any of its subtypes or interface types.
-
-            if Has_Invariants (E) then
-               if Ekind (E) = E_Private_Subtype then
-                  null;
-               else
-                  Build_Invariant_Procedure (E, N);
-               end if;
-            end if;
-         end if;
-
          Next_Entity (E);
       end loop;
 
       if Is_Remote_Call_Interface (Id)
-         and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
+        and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
       then
          Validate_RCI_Declarations (Id);
       end if;
@@ -1490,7 +1745,20 @@ package body Sem_Ch7 is
          declare
             Orig_Spec : constant Node_Id := Specification (Orig_Decl);
             Save_Priv : constant List_Id := Private_Declarations (Orig_Spec);
+
          begin
+            --  Insert the freezing nodes after the visible declarations to
+            --  ensure that we analyze its aspects; needed to ensure that
+            --  global entities referenced in the aspects are properly handled.
+
+            if Ada_Version >= Ada_2012
+              and then Is_Non_Empty_List (Vis_Decls)
+              and then Is_Empty_List (Priv_Decls)
+            then
+               Insert_List_After_And_Analyze
+                 (Last (Vis_Decls), Freeze_Entity (Id, Last (Vis_Decls)));
+            end if;
+
             Set_Private_Declarations (Orig_Spec, Empty_List);
             Save_Global_References   (Orig_Decl);
             Set_Private_Declarations (Orig_Spec, Save_Priv);
@@ -1544,7 +1812,6 @@ package body Sem_Ch7 is
       if Is_Compilation_Unit (Id) then
          Install_Private_With_Clauses (Id);
       else
-
          --  The current compilation unit may include private with_clauses,
          --  which are visible in the private part of the current nested
          --  package, and have to be installed now. This is not done for
@@ -1567,14 +1834,18 @@ package body Sem_Ch7 is
 
       --  If this is a package associated with a generic instance or formal
       --  package, then the private declarations of each of the generic's
-      --  parents must be installed at this point.
+      --  parents must be installed at this point, but not if this is the
+      --  abbreviated instance created to check a formal package, see the
+      --  same condition in Analyze_Package_Instantiation.
 
-      if Is_Generic_Instance (Id) then
+      if Is_Generic_Instance (Id)
+        and then not Is_Abbreviated_Instance (Id)
+      then
          Install_Parent_Private_Declarations (Id);
       end if;
 
       --  Analyze private part if present. The flag In_Private_Part is reset
-      --  in End_Package_Scope.
+      --  in Uninstall_Declarations.
 
       L := Last_Entity (Id);
 
@@ -1605,7 +1876,7 @@ package body Sem_Ch7 is
          end if;
 
       --  There may be inherited private subprograms that need to be declared,
-      --  even in the absence of an explicit private part.  If there are any
+      --  even in the absence of an explicit private part. If there are any
       --  public declarations in the package and the package is a public child
       --  unit, then an implicit private part is assumed.
 
@@ -1626,56 +1897,32 @@ package body Sem_Ch7 is
          end if;
 
          --  Check preelaborable initialization for full type completing a
-         --  private type for which pragma Preelaborable_Initialization given.
-
-         if Is_Type (E)
-           and then Must_Have_Preelab_Init (E)
-           and then not Has_Preelaborable_Initialization (E)
-         then
-            Error_Msg_N
-              ("full view of & does not have preelaborable initialization", E);
-         end if;
-
-         --  An invariant may appear on a full view of a type
-
-         if Is_Type (E)
-           and then Has_Private_Declaration (E)
-           and then Nkind (Parent (E)) = N_Full_Type_Declaration
-         then
+         --  private type when aspect Preelaborable_Initialization is True
+         --  or is specified by Preelaborable_Initialization attributes
+         --  (in the case of a private type in a generic unit). We pass
+         --  the expression of the aspect (when present) to the parameter
+         --  Preelab_Init_Expr to take into account the rule that presumes
+         --  that subcomponents of generic formal types mentioned in the
+         --  type's P_I aspect have preelaborable initialization (see
+         --  AI12-0409 and RM 10.2.1(11.8/5)).
+
+         if Is_Type (E) and then Must_Have_Preelab_Init (E) then
             declare
-               IP_Built : Boolean := False;
-
+               PI_Aspect : constant Node_Id :=
+                             Find_Aspect
+                               (E, Aspect_Preelaborable_Initialization);
+               PI_Expr   : Node_Id := Empty;
             begin
-               if Has_Aspects (Parent (E)) then
-                  declare
-                     ASN : Node_Id;
-
-                  begin
-                     ASN := First (Aspect_Specifications (Parent (E)));
-                     while Present (ASN) loop
-                        if Nam_In (Chars (Identifier (ASN)),
-                             Name_Invariant,
-                             Name_Type_Invariant)
-                        then
-                           Build_Invariant_Procedure (E, N);
-                           IP_Built := True;
-                           exit;
-                        end if;
-
-                        Next (ASN);
-                     end loop;
-                  end;
+               if Present (PI_Aspect) then
+                  PI_Expr := Expression (PI_Aspect);
                end if;
 
-               --  Invariants may have been inherited from progenitors
-
-               if not IP_Built
-                 and then Has_Interfaces (E)
-                 and then Has_Inheritable_Invariants (E)
-                 and then not Is_Interface (E)
-                 and then not Is_Class_Wide_Type (E)
+               if not Has_Preelaborable_Initialization
+                        (E, Preelab_Init_Expr => PI_Expr)
                then
-                  Build_Invariant_Procedure (E, N);
+                  Error_Msg_N
+                    ("full view of & does not have "
+                     & "preelaborable initialization", E);
                end if;
             end;
          end if;
@@ -1695,6 +1942,14 @@ package body Sem_Ch7 is
          Inspect_Unchecked_Union_Completion (Priv_Decls);
       end if;
 
+      --  Implement AI12-0101 (which only removes a legality rule) and then
+      --  AI05-0123 (which directly applies in the previously illegal case)
+      --  in Ada 2012. Note that AI12-0101 is a binding interpretation.
+
+      if Present (Priv_Decls) and then Ada_Version >= Ada_2012 then
+         Inspect_Untagged_Record_Completion (Priv_Decls);
+      end if;
+
       if Ekind (Id) = E_Generic_Package
         and then Nkind (Orig_Decl) = N_Generic_Package_Declaration
         and then Present (Priv_Decls)
@@ -1709,6 +1964,17 @@ package body Sem_Ch7 is
                           Generic_Formal_Declarations (Orig_Decl);
 
          begin
+            --  Insert the freezing nodes after the private declarations to
+            --  ensure that we analyze its aspects; needed to ensure that
+            --  global entities referenced in the aspects are properly handled.
+
+            if Ada_Version >= Ada_2012
+              and then Is_Non_Empty_List (Priv_Decls)
+            then
+               Insert_List_After_And_Analyze
+                 (Last (Priv_Decls), Freeze_Entity (Id, Last (Priv_Decls)));
+            end if;
+
             Set_Visible_Declarations        (Orig_Spec, Empty_List);
             Set_Generic_Formal_Declarations (Orig_Decl, Empty_List);
             Save_Global_References          (Orig_Decl);
@@ -1742,23 +2008,32 @@ package body Sem_Ch7 is
       if Is_Library_Level_Entity (Id)
         or else Is_Generic_Instance (Id)
       then
-         Clear_Constants (Id, First_Entity (Id));
-         Clear_Constants (Id, First_Private_Entity (Id));
+         Clear_Constants (Id);
       end if;
 
-      --  Issue an error in SPARK mode if a package specification contains
-      --  more than one tagged type or type extension.
-
-      Check_One_Tagged_Type_Or_Extension_At_Most;
-
-      --  If switch set, output information on why body required
+      --  Output relevant information as to why the package requires a body.
+      --  Do not consider generated packages as this exposes internal symbols
+      --  and leads to confusing messages.
 
       if List_Body_Required_Info
         and then In_Extended_Main_Source_Unit (Id)
         and then Unit_Requires_Body (Id)
+        and then Comes_From_Source (Id)
       then
          Unit_Requires_Body_Info (Id);
       end if;
+
+      --  Nested package specs that do not require bodies are not checked for
+      --  ineffective use clauses due to the possibility of subunits. This is
+      --  because at this stage it is impossible to tell whether there will be
+      --  a separate body.
+
+      if not Unit_Requires_Body (Id)
+        and then Is_Compilation_Unit (Id)
+        and then not Is_Private_Descendant (Id)
+      then
+         Update_Use_Clause_Chain;
+      end if;
    end Analyze_Package_Specification;
 
    --------------------------------------
@@ -1772,7 +2047,7 @@ package body Sem_Ch7 is
    begin
       Generate_Definition (Id);
       Set_Is_Pure         (Id, PF);
-      Init_Size_Align     (Id);
+      Reinit_Size_Align   (Id);
 
       if not Is_Package_Or_Generic_Package (Current_Scope)
         or else In_Private_Part (Current_Scope)
@@ -1783,12 +2058,10 @@ package body Sem_Ch7 is
       New_Private_Type (N, Id, N);
       Set_Depends_On_Private (Id);
 
-      --  A type declared within a Ghost region is automatically Ghost
-      --  (SPARK RM 6.9(2)).
+      --  Set the SPARK mode from the current context
 
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (Id);
-      end if;
+      Set_SPARK_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (Id);
 
       if Has_Aspects (N) then
          Analyze_Aspect_Specifications (N, Id);
@@ -1944,6 +2217,8 @@ package body Sem_Ch7 is
                            Replace_Elmt (Op_Elmt, New_Op);
                            Remove_Elmt  (Op_List, Op_Elmt_2);
                            Set_Overridden_Operation (New_Op, Parent_Subp);
+                           Set_Is_Ada_2022_Only     (New_Op,
+                             Is_Ada_2022_Only (Parent_Subp));
 
                            --  We don't need to inherit its dispatching slot.
                            --  Set_All_DT_Position has previously ensured that
@@ -2031,9 +2306,8 @@ package body Sem_Ch7 is
                   --  a derived scalar type). Further declarations cannot
                   --  include inherited operations of the type.
 
-                  if Present (Prim_Op) then
-                     exit when Ekind (Prim_Op) not in Overloadable_Kind;
-                  end if;
+                  exit when Present (Prim_Op)
+                    and then not Is_Overloadable (Prim_Op);
                end loop;
             end if;
          end if;
@@ -2080,12 +2354,12 @@ package body Sem_Ch7 is
 
       Exchange_Entities (Id, Full_Id);
 
-      Set_Next_Entity (Id, Next1);
-      Set_Homonym     (Id, H1);
+      Link_Entities (Id, Next1);
+      Set_Homonym   (Id, H1);
 
-      Set_Full_View   (Full_Id, Id);
-      Set_Next_Entity (Full_Id, Next2);
-      Set_Homonym     (Full_Id, H2);
+      Set_Full_View (Full_Id, Id);
+      Link_Entities (Full_Id, Next2);
+      Set_Homonym   (Full_Id, H2);
    end Exchange_Declarations;
 
    ----------------------------
@@ -2129,13 +2403,14 @@ package body Sem_Ch7 is
       procedure Swap_Private_Dependents (Priv_Deps : Elist_Id);
       --  When the full view of a private type is made available, we do the
       --  same for its private dependents under proper visibility conditions.
-      --  When compiling a grand-chid unit this needs to be done recursively.
+      --  When compiling a child unit this needs to be done recursively.
 
       -----------------------------
       -- Swap_Private_Dependents --
       -----------------------------
 
       procedure Swap_Private_Dependents (Priv_Deps : Elist_Id) is
+         Cunit     : Entity_Id;
          Deps      : Elist_Id;
          Priv      : Entity_Id;
          Priv_Elmt : Elmt_Id;
@@ -2153,6 +2428,7 @@ package body Sem_Ch7 is
             if Present (Full_View (Priv)) and then Is_Visible_Dependent (Priv)
             then
                if Is_Private_Type (Priv) then
+                  Cunit := Cunit_Entity (Current_Sem_Unit);
                   Deps := Private_Dependents (Priv);
                   Is_Priv := True;
                else
@@ -2180,11 +2456,14 @@ package body Sem_Ch7 is
                Set_Is_Potentially_Use_Visible
                  (Priv, Is_Potentially_Use_Visible (Node (Priv_Elmt)));
 
-               --  Within a child unit, recurse, except in generic child unit,
-               --  which (unfortunately) handle private_dependents separately.
+               --  Recurse for child units, except in generic child units,
+               --  which unfortunately handle private_dependents separately.
+               --  Note that the current unit may not have been analyzed,
+               --  for example a package body, so we cannot rely solely on
+               --  the Is_Child_Unit flag, but that's only an optimization.
 
                if Is_Priv
-                 and then Is_Child_Unit (Cunit_Entity (Current_Sem_Unit))
+                 and then (No (Etype (Cunit)) or else Is_Child_Unit (Cunit))
                  and then not Is_Empty_Elmt_List (Deps)
                  and then not Inside_A_Generic
                then
@@ -2245,6 +2524,7 @@ package body Sem_Ch7 is
                then
                   Set_Full_View (Id, Underlying_Full_View (Full));
                   Set_Underlying_Full_View (Id, Full);
+                  Set_Is_Underlying_Full_View (Full);
 
                   Set_Underlying_Full_View (Full, Empty);
                   Set_Is_Frozen (Full_View (Id));
@@ -2269,6 +2549,34 @@ package body Sem_Ch7 is
          Next_Entity (Id);
       end loop;
 
+      --  An abstract state is partially refined when it has at least one
+      --  Part_Of constituent. Since these constituents are being installed
+      --  into visibility, update the partial refinement status of any state
+      --  defined in the associated package, subject to at least one Part_Of
+      --  constituent.
+
+      if Is_Package_Or_Generic_Package (P) then
+         declare
+            States     : constant Elist_Id := Abstract_States (P);
+            State_Elmt : Elmt_Id;
+            State_Id   : Entity_Id;
+
+         begin
+            if Present (States) then
+               State_Elmt := First_Elmt (States);
+               while Present (State_Elmt) loop
+                  State_Id := Node (State_Elmt);
+
+                  if Present (Part_Of_Constituents (State_Id)) then
+                     Set_Has_Partial_Visible_Refinement (State_Id);
+                  end if;
+
+                  Next_Elmt (State_Elmt);
+               end loop;
+            end if;
+         end;
+      end if;
+
       --  Indicate that the private part is currently visible, so it can be
       --  properly reset on exit.
 
@@ -2407,15 +2715,15 @@ package body Sem_Ch7 is
       end if;
 
       if Limited_Present (Def) then
-         Set_Ekind (Id, E_Limited_Private_Type);
+         Mutate_Ekind (Id, E_Limited_Private_Type);
       else
-         Set_Ekind (Id, E_Private_Type);
+         Mutate_Ekind (Id, E_Private_Type);
       end if;
 
       Set_Etype              (Id, Id);
       Set_Has_Delayed_Freeze (Id);
       Set_Is_First_Subtype   (Id);
-      Init_Size_Align        (Id);
+      Reinit_Size_Align      (Id);
 
       Set_Is_Constrained (Id,
         No (Discriminant_Specifications (N))
@@ -2441,7 +2749,7 @@ package body Sem_Ch7 is
       Set_Private_Dependents (Id, New_Elmt_List);
 
       if Tagged_Present (Def) then
-         Set_Ekind                       (Id, E_Record_Type_With_Private);
+         Mutate_Ekind                    (Id, E_Record_Type_With_Private);
          Set_Direct_Primitive_Operations (Id, New_Elmt_List);
          Set_Is_Abstract_Type            (Id, Abstract_Present (Def));
          Set_Is_Limited_Record           (Id, Limited_Present (Def));
@@ -2459,6 +2767,15 @@ package body Sem_Ch7 is
 
       elsif Abstract_Present (Def) then
          Error_Msg_N ("only a tagged type can be abstract", N);
+
+      --  We initialize the primitive operations list of an untagged private
+      --  type to an empty element list. Do this even when Extensions_Allowed
+      --  is False to issue better error messages. (Note: This could be done
+      --  for all private types and shared with the tagged case above, but
+      --  for now we do it separately.)
+
+      else
+         Set_Direct_Primitive_Operations (Id, New_Elmt_List);
       end if;
    end New_Private_Type;
 
@@ -2493,7 +2810,7 @@ package body Sem_Ch7 is
       --  implicit completion at some point.
 
       elsif (Is_Overloadable (Id)
-              and then not Ekind_In (Id, E_Enumeration_Literal, E_Operator)
+              and then Ekind (Id) not in E_Enumeration_Literal | E_Operator
               and then not Is_Abstract_Subprogram (Id)
               and then not Has_Completion (Id)
               and then Comes_From_Source (Parent (Id)))
@@ -2510,7 +2827,7 @@ package body Sem_Ch7 is
             and then not Is_Generic_Type (Id))
 
         or else
-          (Ekind_In (Id, E_Task_Type, E_Protected_Type)
+          (Ekind (Id) in E_Task_Type | E_Protected_Type
             and then not Has_Completion (Id))
 
         or else
@@ -2540,13 +2857,16 @@ package body Sem_Ch7 is
       Decl      : constant Node_Id := Unit_Declaration_Node (P);
       Id        : Entity_Id;
       Full      : Entity_Id;
-      Priv_Elmt : Elmt_Id;
-      Priv_Sub  : Entity_Id;
 
-      procedure Preserve_Full_Attributes (Priv, Full : Entity_Id);
+      procedure Preserve_Full_Attributes (Priv : Entity_Id; Full : Entity_Id);
       --  Copy to the private declaration the attributes of the full view that
       --  need to be available for the partial view also.
 
+      procedure Swap_Private_Dependents (Priv_Deps : Elist_Id);
+      --  When the full view of a private type is made unavailable, we do the
+      --  same for its private dependents under proper visibility conditions.
+      --  When compiling a child unit this needs to be done recursively.
+
       function Type_In_Use (T : Entity_Id) return Boolean;
       --  Check whether type or base type appear in an active use_type clause
 
@@ -2554,53 +2874,75 @@ package body Sem_Ch7 is
       -- Preserve_Full_Attributes --
       ------------------------------
 
-      procedure Preserve_Full_Attributes (Priv, Full : Entity_Id) is
-         Priv_Is_Base_Type : constant Boolean := Is_Base_Type (Priv);
+      procedure Preserve_Full_Attributes
+        (Priv : Entity_Id;
+         Full : Entity_Id)
+      is
+         Full_Base         : constant Entity_Id := Base_Type (Full);
+         Priv_Is_Base_Type : constant Boolean   := Is_Base_Type (Priv);
 
       begin
-         Set_Size_Info (Priv, (Full));
-         Set_RM_Size                 (Priv, RM_Size (Full));
+         Set_Size_Info               (Priv,                             Full);
+         Copy_RM_Size                (To => Priv, From => Full);
          Set_Size_Known_At_Compile_Time
                                      (Priv, Size_Known_At_Compile_Time (Full));
          Set_Is_Volatile             (Priv, Is_Volatile                (Full));
          Set_Treat_As_Volatile       (Priv, Treat_As_Volatile          (Full));
+         Set_Is_Atomic               (Priv, Is_Atomic                  (Full));
          Set_Is_Ada_2005_Only        (Priv, Is_Ada_2005_Only           (Full));
          Set_Is_Ada_2012_Only        (Priv, Is_Ada_2012_Only           (Full));
+         Set_Is_Ada_2022_Only        (Priv, Is_Ada_2022_Only           (Full));
          Set_Has_Pragma_Unmodified   (Priv, Has_Pragma_Unmodified      (Full));
          Set_Has_Pragma_Unreferenced (Priv, Has_Pragma_Unreferenced    (Full));
          Set_Has_Pragma_Unreferenced_Objects
                                      (Priv, Has_Pragma_Unreferenced_Objects
                                                                        (Full));
+         Set_Predicates_Ignored      (Priv, Predicates_Ignored         (Full));
          if Is_Unchecked_Union (Full) then
             Set_Is_Unchecked_Union (Base_Type (Priv));
          end if;
-         --  Why is atomic not copied here ???
 
          if Referenced (Full) then
             Set_Referenced (Priv);
          end if;
 
          if Priv_Is_Base_Type then
-            Set_Is_Controlled (Priv, Is_Controlled (Base_Type (Full)));
+            Set_Is_Controlled_Active
+                              (Priv, Is_Controlled_Active     (Full_Base));
             Set_Finalize_Storage_Only
-                              (Priv, Finalize_Storage_Only
-                                                   (Base_Type (Full)));
-            Propagate_Type_Has_Flags
-                              (Priv,                Base_Type (Full));
+                              (Priv, Finalize_Storage_Only    (Full_Base));
             Set_Has_Controlled_Component
-                              (Priv, Has_Controlled_Component
-                                                   (Base_Type (Full)));
+                              (Priv, Has_Controlled_Component (Full_Base));
+
+            Propagate_Concurrent_Flags (Priv, Base_Type (Full));
          end if;
 
+         --  As explained in Freeze_Entity, private types are required to point
+         --  to the same freeze node as their corresponding full view, if any.
+         --  But we ought not to overwrite a node already inserted in the tree.
+
+         pragma Assert
+           (Serious_Errors_Detected /= 0
+             or else No (Freeze_Node (Priv))
+             or else No (Parent (Freeze_Node (Priv)))
+             or else Freeze_Node (Priv) = Freeze_Node (Full));
+
          Set_Freeze_Node (Priv, Freeze_Node (Full));
 
-         --  Propagate information of type invariants, which may be specified
-         --  for the full view.
+         --  Propagate Default_Initial_Condition-related attributes from the
+         --  full view to the private view.
 
-         if Has_Invariants (Full) and not Has_Invariants (Priv) then
-            Set_Has_Invariants (Priv);
-            Set_Subprograms_For_Type (Priv, Subprograms_For_Type (Full));
-         end if;
+         Propagate_DIC_Attributes (Priv, From_Typ => Full);
+
+         --  Propagate invariant-related attributes from the full view to the
+         --  private view.
+
+         Propagate_Invariant_Attributes (Priv, From_Typ => Full);
+
+         --  Propagate predicate-related attributes from the full view to the
+         --  private view.
+
+         Propagate_Predicate_Attributes (Priv, From_Typ => Full);
 
          if Is_Tagged_Type (Priv)
            and then Is_Tagged_Type (Full)
@@ -2631,6 +2973,66 @@ package body Sem_Ch7 is
          end if;
       end Preserve_Full_Attributes;
 
+      -----------------------------
+      -- Swap_Private_Dependents --
+      -----------------------------
+
+      procedure Swap_Private_Dependents (Priv_Deps : Elist_Id) is
+         Cunit     : Entity_Id;
+         Deps      : Elist_Id;
+         Priv      : Entity_Id;
+         Priv_Elmt : Elmt_Id;
+         Is_Priv   : Boolean;
+
+      begin
+         Priv_Elmt := First_Elmt (Priv_Deps);
+         while Present (Priv_Elmt) loop
+            Priv := Node (Priv_Elmt);
+
+            --  Before we do the swap, we verify the presence of the Full_View
+            --  field, which may be empty due to a swap by a previous call to
+            --  End_Package_Scope (e.g. from the freezing mechanism).
+
+            if Present (Full_View (Priv)) then
+               if Is_Private_Type (Priv) then
+                  Cunit := Cunit_Entity (Current_Sem_Unit);
+                  Deps := Private_Dependents (Priv);
+                  Is_Priv := True;
+               else
+                  Is_Priv := False;
+               end if;
+
+               if Scope (Priv) = P
+                 or else not In_Open_Scopes (Scope (Priv))
+               then
+                  Set_Is_Immediately_Visible (Priv, False);
+               end if;
+
+               if Is_Visible_Dependent (Priv) then
+                  Preserve_Full_Attributes (Priv, Full_View (Priv));
+                  Replace_Elmt (Priv_Elmt, Full_View (Priv));
+                  Exchange_Declarations (Priv);
+
+                  --  Recurse for child units, except in generic child units,
+                  --  which unfortunately handle private_dependents separately.
+                  --  Note that the current unit may not have been analyzed,
+                  --  for example a package body, so we cannot rely solely on
+                  --  the Is_Child_Unit flag, but that's only an optimization.
+
+                  if Is_Priv
+                    and then (No (Etype (Cunit)) or else Is_Child_Unit (Cunit))
+                    and then not Is_Empty_Elmt_List (Deps)
+                    and then not Inside_A_Generic
+                  then
+                     Swap_Private_Dependents (Deps);
+                  end if;
+               end if;
+            end if;
+
+            Next_Elmt (Priv_Elmt);
+         end loop;
+      end Swap_Private_Dependents;
+
       -----------------
       -- Type_In_Use --
       -----------------
@@ -2658,8 +3060,9 @@ package body Sem_Ch7 is
          --  a) If the entity is an operator, it may be a primitive operator of
          --  a type for which there is a visible use-type clause.
 
-         --  b) for other entities, their use-visibility is determined by a
-         --  visible use clause for the package itself. For a generic instance,
+         --  b) For other entities, their use-visibility is determined by a
+         --  visible use clause for the package itself or a use-all-type clause
+         --  applied directly to the entity's type. For a generic instance,
          --  the instantiation of the formals appears in the visible part,
          --  but the formals are private and remain so.
 
@@ -2692,6 +3095,21 @@ package body Sem_Ch7 is
                   Set_Is_Potentially_Use_Visible (Id);
                end if;
 
+            --  Avoid crash caused by previous errors
+
+            elsif No (Etype (Id)) and then Serious_Errors_Detected /= 0 then
+               null;
+
+            --  We need to avoid incorrectly marking enumeration literals as
+            --  non-visible when a visible use-all-type clause is in effect.
+
+            elsif Type_In_Use (Etype (Id))
+              and then Nkind (Current_Use_Clause (Etype (Id))) =
+                         N_Use_Type_Clause
+              and then All_Present (Current_Use_Clause (Etype (Id)))
+            then
+               null;
+
             else
                Set_Is_Potentially_Use_Visible (Id, False);
             end if;
@@ -2718,7 +3136,7 @@ package body Sem_Ch7 is
             Check_Conventions (Id);
          end if;
 
-         if Ekind_In (Id, E_Private_Type, E_Limited_Private_Type)
+         if Ekind (Id) in E_Private_Type | E_Limited_Private_Type
            and then No (Full_View (Id))
            and then not Is_Generic_Type (Id)
            and then not Is_Derived_Type (Id)
@@ -2808,10 +3226,12 @@ package body Sem_Ch7 is
 
       if not In_Private_Part (P) then
          return;
-      else
-         Set_In_Private_Part (P, False);
       end if;
 
+      --  Reset the flag now
+
+      Set_In_Private_Part (P, False);
+
       --  Make private entities invisible and exchange full and private
       --  declarations for private types. Id is now the first private entity
       --  in the package.
@@ -2871,31 +3291,7 @@ package body Sem_Ch7 is
             --  were compiled in this scope, or installed previously
             --  by Install_Private_Declarations.
 
-            --  Before we do the swap, we verify the presence of the Full_View
-            --  field which may be empty due to a swap by a previous call to
-            --  End_Package_Scope (e.g. from the freezing mechanism).
-
-            Priv_Elmt := First_Elmt (Private_Dependents (Id));
-            while Present (Priv_Elmt) loop
-               Priv_Sub := Node (Priv_Elmt);
-
-               if Present (Full_View (Priv_Sub)) then
-                  if Scope (Priv_Sub) = P
-                     or else not In_Open_Scopes (Scope (Priv_Sub))
-                  then
-                     Set_Is_Immediately_Visible (Priv_Sub, False);
-                  end if;
-
-                  if Is_Visible_Dependent (Priv_Sub) then
-                     Preserve_Full_Attributes
-                       (Priv_Sub, Full_View (Priv_Sub));
-                     Replace_Elmt (Priv_Elmt, Full_View (Priv_Sub));
-                     Exchange_Declarations (Priv_Sub);
-                  end if;
-               end if;
-
-               Next_Elmt (Priv_Elmt);
-            end loop;
+            Swap_Private_Dependents (Private_Dependents (Id));
 
             --  Now restore the type itself to its private view
 
@@ -2943,7 +3339,7 @@ package body Sem_Ch7 is
                   if Is_Overloadable (Subp) and then Is_Primitive (Subp) then
                      Error_Msg_NE
                        ("type& must be completed in the private part",
-                         Parent (Subp), Id);
+                        Parent (Subp), Id);
 
                   --  The result type of an access-to-function type cannot be a
                   --  Taft-amendment type, unless the version is Ada 2012 or
@@ -2967,6 +3363,25 @@ package body Sem_Ch7 is
                end loop;
             end;
 
+         --  For subtypes of private types the frontend generates two entities:
+         --  one associated with the partial view and the other associated with
+         --  the full view. When the subtype declaration is public the frontend
+         --  places the former entity in the list of public entities of the
+         --  package and the latter entity in the private part of the package.
+         --  When the subtype declaration is private it generates these two
+         --  entities but both are placed in the private part of the package
+         --  (and the full view has the same source location as the partial
+         --  view and no parent; see Prepare_Private_Subtype_Completion).
+
+         elsif Ekind (Id) in E_Private_Subtype
+                           | E_Limited_Private_Subtype
+           and then Present (Full_View (Id))
+           and then Sloc (Id) = Sloc (Full_View (Id))
+           and then No (Parent (Full_View (Id)))
+         then
+            Set_Is_Hidden (Id);
+            Set_Is_Potentially_Use_Visible (Id, False);
+
          elsif not Is_Child_Unit (Id)
            and then (not Is_Private_Type (Id) or else No (Full_View (Id)))
          then
@@ -2990,7 +3405,7 @@ package body Sem_Ch7 is
       E : Entity_Id;
 
       Requires_Body : Boolean := False;
-      --  Flag set when the unit has at least one construct that requries
+      --  Flag set when the unit has at least one construct that requires
       --  completion in a body.
 
    begin
@@ -3053,11 +3468,11 @@ package body Sem_Ch7 is
 
       --  A [generic] package that defines at least one non-null abstract state
       --  requires a completion only when at least one other construct requires
-      --  a completion in a body (SPARK RM 7.1.4(4) and (6)). This check is not
+      --  a completion in a body (SPARK RM 7.1.4(4) and (5)). This check is not
       --  performed if the caller requests this behavior.
 
       if Do_Abstract_States
-        and then Ekind_In (Pack_Id, E_Generic_Package, E_Package)
+        and then Is_Package_Or_Generic_Package (Pack_Id)
         and then Has_Non_Null_Abstract_State (Pack_Id)
         and then Requires_Body
       then
@@ -3085,12 +3500,12 @@ package body Sem_Ch7 is
       --  Body required if library package with pragma Elaborate_Body
 
       elsif Has_Pragma_Elaborate_Body (Pack_Id) then
-         Error_Msg_N ("info: & requires body (Elaborate_Body)?Y?", Pack_Id);
+         Error_Msg_N ("info: & requires body (Elaborate_Body)?.y?", Pack_Id);
 
       --  Body required if subprogram
 
       elsif Is_Subprogram_Or_Generic_Subprogram (Pack_Id) then
-         Error_Msg_N ("info: & requires body (subprogram case)?Y?", Pack_Id);
+         Error_Msg_N ("info: & requires body (subprogram case)?.y?", Pack_Id);
 
       --  Body required if generic parent has Elaborate_Body
 
@@ -3103,7 +3518,7 @@ package body Sem_Ch7 is
          begin
             if Has_Pragma_Elaborate_Body (G_P) then
                Error_Msg_N
-                 ("info: & requires body (generic parent Elaborate_Body)?Y?",
+                 ("info: & requires body (generic parent Elaborate_Body)?.y?",
                   Pack_Id);
             end if;
          end;
@@ -3115,13 +3530,13 @@ package body Sem_Ch7 is
       --  provided). If Ignore_Abstract_State is True, we don't do this check
       --  (so we can use Unit_Requires_Body to check for some other reason).
 
-      elsif Ekind_In (Pack_Id, E_Generic_Package, E_Package)
+      elsif Is_Package_Or_Generic_Package (Pack_Id)
         and then Present (Abstract_States (Pack_Id))
         and then not Is_Null_State
                        (Node (First_Elmt (Abstract_States (Pack_Id))))
       then
          Error_Msg_N
-           ("info: & requires body (non-null abstract state aspect)?Y?",
+           ("info: & requires body (non-null abstract state aspect)?.y?",
             Pack_Id);
       end if;
 
@@ -3132,10 +3547,12 @@ package body Sem_Ch7 is
          if Requires_Completion_In_Body (E, Pack_Id) then
             Error_Msg_Node_2 := E;
             Error_Msg_NE
-              ("info: & requires body (& requires completion)?Y?", E, Pack_Id);
+              ("info: & requires body (& requires completion)?.y?", E,
+               Pack_Id);
          end if;
 
          Next_Entity (E);
       end loop;
    end Unit_Requires_Body_Info;
+
 end Sem_Ch7;
This page took 0.092009 seconds and 5 git commands to generate.