]> gcc.gnu.org Git - gcc.git/blobdiff - gcc/ada/sem_util.adb
[multiple changes]
[gcc.git] / gcc / ada / sem_util.adb
index da7d00a5b65fd6a4f936d136cf7710981826b9da..58a157bdd5aea571e5e325f1f62af7225694feab 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -37,7 +37,6 @@ with Exp_Disp; use Exp_Disp;
 with Exp_Util; use Exp_Util;
 with Fname;    use Fname;
 with Freeze;   use Freeze;
-with Ghost;    use Ghost;
 with Lib;      use Lib;
 with Lib.Xref; use Lib.Xref;
 with Namet.Sp; use Namet.Sp;
@@ -52,7 +51,6 @@ with Sem_Aux;  use Sem_Aux;
 with Sem_Attr; use Sem_Attr;
 with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
 with Sem_Prag; use Sem_Prag;
@@ -286,11 +284,54 @@ package body Sem_Util is
       end if;
    end Address_Integer_Convert_OK;
 
+   -------------------
+   -- Address_Value --
+   -------------------
+
+   function Address_Value (N : Node_Id) return Node_Id is
+      Expr : Node_Id := N;
+
+   begin
+      loop
+         --  For constant, get constant expression
+
+         if Is_Entity_Name (Expr)
+           and then Ekind (Entity (Expr)) = E_Constant
+         then
+            Expr := Constant_Value (Entity (Expr));
+
+         --  For unchecked conversion, get result to convert
+
+         elsif Nkind (Expr) = N_Unchecked_Type_Conversion then
+            Expr := Expression (Expr);
+
+         --  For (common case) of To_Address call, get argument
+
+         elsif Nkind (Expr) = N_Function_Call
+           and then Is_Entity_Name (Name (Expr))
+           and then Is_RTE (Entity (Name (Expr)), RE_To_Address)
+         then
+            Expr := First (Parameter_Associations (Expr));
+
+            if Nkind (Expr) = N_Parameter_Association then
+               Expr := Explicit_Actual_Parameter (Expr);
+            end if;
+
+         --  We finally have the real expression
+
+         else
+            exit;
+         end if;
+      end loop;
+
+      return Expr;
+   end Address_Value;
+
    -----------------
    -- Addressable --
    -----------------
 
-   --  For now, just 8/16/32/64. but analyze later if AAMP is special???
+   --  For now, just 8/16/32/64
 
    function Addressable (V : Uint) return Boolean is
    begin
@@ -326,21 +367,19 @@ package body Sem_Util is
       --  Ada 2005 (AI-230): Generate a conversion to an anonymous access
       --  component's type to force the appropriate accessibility checks.
 
-      --  Ada 2005 (AI-231): Generate conversion to the null-excluding
-      --  type to force the corresponding run-time check
+      --  Ada 2005 (AI-231): Generate conversion to the null-excluding type to
+      --  force the corresponding run-time check
 
       if Is_Access_Type (Check_Typ)
-        and then ((Is_Local_Anonymous_Access (Check_Typ))
-                    or else (Can_Never_Be_Null (Check_Typ)
-                              and then not Can_Never_Be_Null (Exp_Typ)))
+        and then Is_Local_Anonymous_Access (Check_Typ)
       then
          Rewrite (Exp, Convert_To (Check_Typ, Relocate_Node (Exp)));
          Analyze_And_Resolve (Exp, Check_Typ);
          Check_Unset_Reference (Exp);
       end if;
 
-      --  This is really expansion activity, so make sure that expansion is
-      --  on and is allowed. In GNATprove mode, we also want check flags to
+      --  What follows is really expansion activity, so check that expansion
+      --  is on and is allowed. In GNATprove mode, we also want check flags to
       --  be added in the tree, so that the formal verification can rely on
       --  those to be present. In GNATprove mode for formal verification, some
       --  treatment typically only done during expansion needs to be performed
@@ -353,6 +392,13 @@ package body Sem_Util is
          return;
       end if;
 
+      if Is_Access_Type (Check_Typ)
+        and then Can_Never_Be_Null (Check_Typ)
+        and then not Can_Never_Be_Null (Exp_Typ)
+      then
+         Install_Null_Excluding_Check (Exp);
+      end if;
+
       --  First check if we have to insert discriminant checks
 
       if Has_Discriminants (Exp_Typ) then
@@ -1146,273 +1192,6 @@ package body Sem_Util is
       return Decl;
    end Build_Component_Subtype;
 
-   ----------------------------------
-   -- Build_Default_Init_Cond_Call --
-   ----------------------------------
-
-   function Build_Default_Init_Cond_Call
-     (Loc    : Source_Ptr;
-      Obj_Id : Entity_Id;
-      Typ    : Entity_Id) return Node_Id
-   is
-      Proc_Id    : constant Entity_Id := Default_Init_Cond_Procedure (Typ);
-      Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id));
-
-   begin
-      return
-        Make_Procedure_Call_Statement (Loc,
-          Name                   => New_Occurrence_Of (Proc_Id, Loc),
-          Parameter_Associations => New_List (
-            Make_Unchecked_Type_Conversion (Loc,
-              Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc),
-              Expression   => New_Occurrence_Of (Obj_Id, Loc))));
-   end Build_Default_Init_Cond_Call;
-
-   ----------------------------------------------
-   -- Build_Default_Init_Cond_Procedure_Bodies --
-   ----------------------------------------------
-
-   procedure Build_Default_Init_Cond_Procedure_Bodies (Priv_Decls : List_Id) is
-      procedure Build_Default_Init_Cond_Procedure_Body (Typ : Entity_Id);
-      --  If type Typ is subject to pragma Default_Initial_Condition, build the
-      --  body of the procedure which verifies the assumption of the pragma at
-      --  run time. The generated body is added after the type declaration.
-
-      --------------------------------------------
-      -- Build_Default_Init_Cond_Procedure_Body --
-      --------------------------------------------
-
-      procedure Build_Default_Init_Cond_Procedure_Body (Typ : Entity_Id) is
-         Param_Id : Entity_Id;
-         --  The entity of the sole formal parameter of the default initial
-         --  condition procedure.
-
-         procedure Replace_Type_Reference (N : Node_Id);
-         --  Replace a single reference to type Typ with a reference to formal
-         --  parameter Param_Id.
-
-         ----------------------------
-         -- Replace_Type_Reference --
-         ----------------------------
-
-         procedure Replace_Type_Reference (N : Node_Id) is
-         begin
-            Rewrite (N, New_Occurrence_Of (Param_Id, Sloc (N)));
-         end Replace_Type_Reference;
-
-         procedure Replace_Type_References is
-           new Replace_Type_References_Generic (Replace_Type_Reference);
-
-         --  Local variables
-
-         Loc       : constant Source_Ptr := Sloc (Typ);
-         Prag      : constant Node_Id    :=
-                       Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-         Proc_Id   : constant Entity_Id  := Default_Init_Cond_Procedure (Typ);
-         Spec_Decl : constant Node_Id    := Unit_Declaration_Node (Proc_Id);
-         Body_Decl : Node_Id;
-         Expr      : Node_Id;
-         Stmt      : Node_Id;
-
-         Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-      --  Start of processing for Build_Default_Init_Cond_Procedure_Body
-
-      begin
-         --  The procedure should be generated only for [sub]types subject to
-         --  pragma Default_Initial_Condition. Types that inherit the pragma do
-         --  not get this specialized procedure.
-
-         pragma Assert (Has_Default_Init_Cond (Typ));
-         pragma Assert (Present (Prag));
-         pragma Assert (Present (Proc_Id));
-
-         --  Nothing to do if the body was already built
-
-         if Present (Corresponding_Body (Spec_Decl)) then
-            return;
-         end if;
-
-         --  The related type may be subject to pragma Ghost. Set the mode now
-         --  to ensure that the analysis and expansion produce Ghost nodes.
-
-         Set_Ghost_Mode_From_Entity (Typ);
-
-         Param_Id := First_Formal (Proc_Id);
-
-         --  The pragma has an argument. Note that the argument is analyzed
-         --  after all references to the current instance of the type are
-         --  replaced.
-
-         if Present (Pragma_Argument_Associations (Prag)) then
-            Expr :=
-              Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
-
-            if Nkind (Expr) = N_Null then
-               Stmt := Make_Null_Statement (Loc);
-
-            --  Preserve the original argument of the pragma by replicating it.
-            --  Replace all references to the current instance of the type with
-            --  references to the formal parameter.
-
-            else
-               Expr := New_Copy_Tree (Expr);
-               Replace_Type_References (Expr, Typ);
-
-               --  Generate:
-               --    pragma Check (Default_Initial_Condition, <Expr>);
-
-               Stmt :=
-                 Make_Pragma (Loc,
-                   Pragma_Identifier            =>
-                     Make_Identifier (Loc, Name_Check),
-
-                   Pragma_Argument_Associations => New_List (
-                     Make_Pragma_Argument_Association (Loc,
-                       Expression =>
-                         Make_Identifier (Loc,
-                           Chars => Name_Default_Initial_Condition)),
-                     Make_Pragma_Argument_Association (Loc,
-                       Expression => Expr)));
-            end if;
-
-         --  Otherwise the pragma appears without an argument
-
-         else
-            Stmt := Make_Null_Statement (Loc);
-         end if;
-
-         --  Generate:
-         --    procedure <Typ>Default_Init_Cond (I : <Typ>) is
-         --    begin
-         --       <Stmt>;
-         --    end <Typ>Default_Init_Cond;
-
-         Body_Decl :=
-           Make_Subprogram_Body (Loc,
-             Specification              =>
-               Copy_Separate_Tree (Specification (Spec_Decl)),
-             Declarations               => Empty_List,
-             Handled_Statement_Sequence =>
-               Make_Handled_Sequence_Of_Statements (Loc,
-                 Statements => New_List (Stmt)));
-
-         --  Link the spec and body of the default initial condition procedure
-         --  to prevent the generation of a duplicate body.
-
-         Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl));
-         Set_Corresponding_Spec (Body_Decl, Proc_Id);
-
-         Insert_After_And_Analyze (Declaration_Node (Typ), Body_Decl);
-         Ghost_Mode := Save_Ghost_Mode;
-      end Build_Default_Init_Cond_Procedure_Body;
-
-      --  Local variables
-
-      Decl : Node_Id;
-      Typ  : Entity_Id;
-
-   --  Start of processing for Build_Default_Init_Cond_Procedure_Bodies
-
-   begin
-      --  Inspect the private declarations looking for [sub]type declarations
-
-      Decl := First (Priv_Decls);
-      while Present (Decl) loop
-         if Nkind_In (Decl, N_Full_Type_Declaration,
-                            N_Subtype_Declaration)
-         then
-            Typ := Defining_Entity (Decl);
-
-            --  Guard against partially decorate types due to previous errors
-
-            if Is_Type (Typ) then
-
-               --  If the type is subject to pragma Default_Initial_Condition,
-               --  generate the body of the internal procedure which verifies
-               --  the assertion of the pragma at run time.
-
-               if Has_Default_Init_Cond (Typ) then
-                  Build_Default_Init_Cond_Procedure_Body (Typ);
-
-               --  A derived type inherits the default initial condition
-               --  procedure from its parent type.
-
-               elsif Has_Inherited_Default_Init_Cond (Typ) then
-                  Inherit_Default_Init_Cond_Procedure (Typ);
-               end if;
-            end if;
-         end if;
-
-         Next (Decl);
-      end loop;
-   end Build_Default_Init_Cond_Procedure_Bodies;
-
-   ---------------------------------------------------
-   -- Build_Default_Init_Cond_Procedure_Declaration --
-   ---------------------------------------------------
-
-   procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is
-      Loc  : constant Source_Ptr := Sloc (Typ);
-      Prag : constant Node_Id    :=
-                  Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-      Proc_Id : Entity_Id;
-
-   begin
-      --  The procedure should be generated only for types subject to pragma
-      --  Default_Initial_Condition. Types that inherit the pragma do not get
-      --  this specialized procedure.
-
-      pragma Assert (Has_Default_Init_Cond (Typ));
-      pragma Assert (Present (Prag));
-
-      --  Nothing to do if default initial condition procedure already built
-
-      if Present (Default_Init_Cond_Procedure (Typ)) then
-         return;
-      end if;
-
-      --  The related type may be subject to pragma Ghost. Set the mode now to
-      --  ensure that the analysis and expansion produce Ghost nodes.
-
-      Set_Ghost_Mode_From_Entity (Typ);
-
-      Proc_Id :=
-        Make_Defining_Identifier (Loc,
-          Chars => New_External_Name (Chars (Typ), "Default_Init_Cond"));
-
-      --  Associate default initial condition procedure with the private type
-
-      Set_Ekind (Proc_Id, E_Procedure);
-      Set_Is_Default_Init_Cond_Procedure (Proc_Id);
-      Set_Default_Init_Cond_Procedure (Typ, Proc_Id);
-
-      --  Mark the default initial condition procedure explicitly as Ghost
-      --  because it does not come from source.
-
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (Proc_Id);
-      end if;
-
-      --  Generate:
-      --    procedure <Typ>Default_Init_Cond (Inn : <Typ>);
-
-      Insert_After_And_Analyze (Prag,
-        Make_Subprogram_Declaration (Loc,
-          Specification =>
-            Make_Procedure_Specification (Loc,
-              Defining_Unit_Name       => Proc_Id,
-              Parameter_Specifications => New_List (
-                Make_Parameter_Specification (Loc,
-                  Defining_Identifier => Make_Temporary (Loc, 'I'),
-                  Parameter_Type      => New_Occurrence_Of (Typ, Loc))))));
-
-      Ghost_Mode := Save_Ghost_Mode;
-   end Build_Default_Init_Cond_Procedure_Declaration;
-
    ---------------------------
    -- Build_Default_Subtype --
    ---------------------------
@@ -3556,8 +3335,8 @@ package body Sem_Util is
 
       Prag := Pre_Post_Conditions (Items);
       while Present (Prag) loop
-         if Nam_In (Pragma_Name (Prag), Name_Postcondition,
-                                        Name_Refined_Post)
+         if Nam_In (Pragma_Name_Unmapped (Prag),
+                    Name_Postcondition, Name_Refined_Post)
            and then not Error_Posted (Prag)
          then
             Post_Prag := Prag;
@@ -3621,6 +3400,172 @@ package body Sem_Util is
       end if;
    end Check_Result_And_Post_State;
 
+   -----------------------------
+   -- Check_State_Refinements --
+   -----------------------------
+
+   procedure Check_State_Refinements
+     (Context      : Node_Id;
+      Is_Main_Unit : Boolean := False)
+   is
+      procedure Check_Package (Pack : Node_Id);
+      --  Verify that all abstract states of a [generic] package denoted by its
+      --  declarative node Pack have proper refinement. Recursively verify the
+      --  visible and private declarations of the [generic] package for other
+      --  nested packages.
+
+      procedure Check_Packages_In (Decls : List_Id);
+      --  Seek out [generic] package declarations within declarative list Decls
+      --  and verify the status of their abstract state refinement.
+
+      function SPARK_Mode_Is_Off (N : Node_Id) return Boolean;
+      --  Determine whether construct N is subject to pragma SPARK_Mode Off
+
+      -------------------
+      -- Check_Package --
+      -------------------
+
+      procedure Check_Package (Pack : Node_Id) is
+         Body_Id : constant Entity_Id := Corresponding_Body (Pack);
+         Spec    : constant Node_Id   := Specification (Pack);
+         States  : constant Elist_Id  :=
+                     Abstract_States (Defining_Entity (Pack));
+
+         State_Elmt : Elmt_Id;
+         State_Id   : Entity_Id;
+
+      begin
+         --  Do not verify proper state refinement when the package is subject
+         --  to pragma SPARK_Mode Off because this disables the requirement for
+         --  state refinement.
+
+         if SPARK_Mode_Is_Off (Pack) then
+            null;
+
+         --  State refinement can only occur in a completing packge body. Do
+         --  not verify proper state refinement when the body is subject to
+         --  pragma SPARK_Mode Off because this disables the requirement for
+         --  state refinement.
+
+         elsif Present (Body_Id)
+           and then SPARK_Mode_Is_Off (Unit_Declaration_Node (Body_Id))
+         then
+            null;
+
+         --  Do not verify proper state refinement when the package is an
+         --  instance as this check was already performed in the generic.
+
+         elsif Present (Generic_Parent (Spec)) then
+            null;
+
+         --  Otherwise examine the contents of the package
+
+         else
+            if Present (States) then
+               State_Elmt := First_Elmt (States);
+               while Present (State_Elmt) loop
+                  State_Id := Node (State_Elmt);
+
+                  --  Emit an error when a non-null state lacks any form of
+                  --  refinement.
+
+                  if not Is_Null_State (State_Id)
+                    and then not Has_Null_Refinement (State_Id)
+                    and then not Has_Non_Null_Refinement (State_Id)
+                  then
+                     Error_Msg_N ("state & requires refinement", State_Id);
+                  end if;
+
+                  Next_Elmt (State_Elmt);
+               end loop;
+            end if;
+
+            Check_Packages_In (Visible_Declarations (Spec));
+            Check_Packages_In (Private_Declarations (Spec));
+         end if;
+      end Check_Package;
+
+      -----------------------
+      -- Check_Packages_In --
+      -----------------------
+
+      procedure Check_Packages_In (Decls : List_Id) is
+         Decl : Node_Id;
+
+      begin
+         if Present (Decls) then
+            Decl := First (Decls);
+            while Present (Decl) loop
+               if Nkind_In (Decl, N_Generic_Package_Declaration,
+                                  N_Package_Declaration)
+               then
+                  Check_Package (Decl);
+               end if;
+
+               Next (Decl);
+            end loop;
+         end if;
+      end Check_Packages_In;
+
+      -----------------------
+      -- SPARK_Mode_Is_Off --
+      -----------------------
+
+      function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
+         Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
+
+      begin
+         return
+           Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+      end SPARK_Mode_Is_Off;
+
+   --  Start of processing for Check_State_Refinements
+
+   begin
+      --  A block may declare a nested package
+
+      if Nkind (Context) = N_Block_Statement then
+         Check_Packages_In (Declarations (Context));
+
+      --  An entry, protected, subprogram, or task body may declare a nested
+      --  package.
+
+      elsif Nkind_In (Context, N_Entry_Body,
+                               N_Protected_Body,
+                               N_Subprogram_Body,
+                               N_Task_Body)
+      then
+         --  Do not verify proper state refinement when the body is subject to
+         --  pragma SPARK_Mode Off because this disables the requirement for
+         --  state refinement.
+
+         if not SPARK_Mode_Is_Off (Context) then
+            Check_Packages_In (Declarations (Context));
+         end if;
+
+      --  A package body may declare a nested package
+
+      elsif Nkind (Context) = N_Package_Body then
+         Check_Package (Unit_Declaration_Node (Corresponding_Spec (Context)));
+
+         --  Do not verify proper state refinement when the body is subject to
+         --  pragma SPARK_Mode Off because this disables the requirement for
+         --  state refinement.
+
+         if not SPARK_Mode_Is_Off (Context) then
+            Check_Packages_In (Declarations (Context));
+         end if;
+
+      --  A library level [generic] package may declare a nested package
+
+      elsif Nkind_In (Context, N_Generic_Package_Declaration,
+                               N_Package_Declaration)
+        and then Is_Main_Unit
+      then
+         Check_Package (Context);
+      end if;
+   end Check_State_Refinements;
+
    ------------------------------
    -- Check_Unprotected_Access --
    ------------------------------
@@ -4068,7 +4013,11 @@ package body Sem_Util is
             Full_T := Full_View (Typ);
 
             if Ekind (Full_T) = E_Record_Subtype then
-               Full_T := Full_View (Etype (Typ));
+               Full_T := Etype (Typ);
+
+               if Present (Full_View (Full_T)) then
+                  Full_T := Full_View (Full_T);
+               end if;
             end if;
          end if;
 
@@ -4624,7 +4573,7 @@ package body Sem_Util is
          Msgl := Msg'Length;
 
          for J in 1 .. Msgl loop
-            if Msg (J) = '?' and then (J = 1 or else Msg (J) /= ''') then
+            if Msg (J) = '?' and then (J = 1 or else Msg (J - 1) /= ''') then
                Msgc (J) := '<';
             else
                Msgc (J) := Msg (J);
@@ -6116,6 +6065,7 @@ package body Sem_Util is
          Encl_Unit := Library_Unit (Encl_Unit);
       end loop;
 
+      pragma Assert (Nkind (Encl_Unit) = N_Compilation_Unit);
       return Encl_Unit;
    end Enclosing_Lib_Unit_Node;
 
@@ -6294,9 +6244,9 @@ package body Sem_Util is
            or else Is_Internal (E)
          then
             declare
+               Decl     : constant Node_Id := Parent (E);
                Prev     : Entity_Id;
                Prev_Vis : Entity_Id;
-               Decl     : constant Node_Id := Parent (E);
 
             begin
                --  If E is an implicit declaration, it cannot be the first
@@ -6987,7 +6937,7 @@ package body Sem_Util is
       end if;
 
       while Present (Old_Disc) and then Present (New_Disc) loop
-         if Old_Disc = Par_Disc  then
+         if Old_Disc = Par_Disc then
             return New_Disc;
          end if;
 
@@ -7622,7 +7572,14 @@ package body Sem_Util is
          end loop Find_Discrete_Value;
       end Search_For_Discriminant_Value;
 
-      if No (Variant) then
+      --  The case statement must include a variant that corresponds to the
+      --  value of the discriminant, unless the discriminant type has a
+      --  static predicate. In that case the absence of an others_choice that
+      --  would cover this value becomes a run-time error (3.8,1 (21.1/2)).
+
+      if No (Variant)
+        and then not Has_Static_Predicate (Etype (Discrim_Name))
+      then
          Error_Msg_NE
            ("value of discriminant & is out of range", Discrim_Value, Discrim);
          Report_Errors := True;
@@ -7633,8 +7590,10 @@ package body Sem_Util is
       --  components to the Into list. The nested components are part of
       --  the same record type.
 
-      Gather_Components
-        (Typ, Component_List (Variant), Governed_By, Into, Report_Errors);
+      if Present (Variant) then
+         Gather_Components
+           (Typ, Component_List (Variant), Governed_By, Into, Report_Errors);
+      end if;
    end Gather_Components;
 
    ------------------------
@@ -7921,6 +7880,7 @@ package body Sem_Util is
    is
       Btyp : Entity_Id := Base_Type (T);
       Lit  : Node_Id;
+      LLoc : Source_Ptr;
 
    begin
       --  In the case where the literal is of type Character, Wide_Character
@@ -7931,6 +7891,7 @@ package body Sem_Util is
 
       if Is_Standard_Character_Type (T) then
          Set_Character_Literal_Name (UI_To_CC (Pos));
+
          return
            Make_Character_Literal (Loc,
              Chars              => Name_Find,
@@ -7948,9 +7909,26 @@ package body Sem_Util is
          Lit := First_Literal (Btyp);
          for J in 1 .. UI_To_Int (Pos) loop
             Next_Literal (Lit);
+
+            --  If Lit is Empty, Pos is not in range, so raise Constraint_Error
+            --  inside the loop to avoid calling Next_Literal on Empty.
+
+            if No (Lit) then
+               raise Constraint_Error;
+            end if;
          end loop;
 
-         return New_Occurrence_Of (Lit, Loc);
+         --  Create a new node from Lit, with source location provided by Loc
+         --  if not equal to No_Location, or by copying the source location of
+         --  Lit otherwise.
+
+         LLoc := Loc;
+
+         if LLoc = No_Location then
+            LLoc := Sloc (Lit);
+         end if;
+
+         return New_Occurrence_Of (Lit, LLoc);
       end if;
    end Get_Enum_Lit_From_Pos;
 
@@ -8109,6 +8087,25 @@ package body Sem_Util is
       pragma Assert (Name_Buffer (Name_Len + 1) = ' ');
    end Get_Library_Unit_Name_String;
 
+   --------------------------
+   -- Get_Max_Queue_Length --
+   --------------------------
+
+   function Get_Max_Queue_Length (Id : Entity_Id) return Uint is
+      pragma Assert (Is_Entry (Id));
+      Prag : constant Entity_Id := Get_Pragma (Id, Pragma_Max_Queue_Length);
+
+   begin
+      --  A value of 0 represents no maximum specified, and entries and entry
+      --  families with no Max_Queue_Length aspect or pragma default to it.
+
+      if not Present (Prag) then
+         return Uint_0;
+      end if;
+
+      return Intval (Expression (First (Pragma_Argument_Associations (Prag))));
+   end Get_Max_Queue_Length;
+
    ------------------------
    -- Get_Name_Entity_Id --
    ------------------------
@@ -8153,9 +8150,76 @@ package body Sem_Util is
 
    function Get_Pragma_Id (N : Node_Id) return Pragma_Id is
    begin
-      return Get_Pragma_Id (Pragma_Name (N));
+      return Get_Pragma_Id (Pragma_Name_Unmapped (N));
    end Get_Pragma_Id;
 
+   ------------------------
+   -- Get_Qualified_Name --
+   ------------------------
+
+   function Get_Qualified_Name
+     (Id     : Entity_Id;
+      Suffix : Entity_Id := Empty) return Name_Id
+   is
+      Suffix_Nam : Name_Id := No_Name;
+
+   begin
+      if Present (Suffix) then
+         Suffix_Nam := Chars (Suffix);
+      end if;
+
+      return Get_Qualified_Name (Chars (Id), Suffix_Nam, Scope (Id));
+   end Get_Qualified_Name;
+
+   function Get_Qualified_Name
+     (Nam    : Name_Id;
+      Suffix : Name_Id   := No_Name;
+      Scop   : Entity_Id := Current_Scope) return Name_Id
+   is
+      procedure Add_Scope (S : Entity_Id);
+      --  Add the fully qualified form of scope S to the name buffer. The
+      --  format is:
+      --    s-1__s__
+
+      ---------------
+      -- Add_Scope --
+      ---------------
+
+      procedure Add_Scope (S : Entity_Id) is
+      begin
+         if S = Empty then
+            null;
+
+         elsif S = Standard_Standard then
+            null;
+
+         else
+            Add_Scope (Scope (S));
+            Get_Name_String_And_Append (Chars (S));
+            Add_Str_To_Name_Buffer ("__");
+         end if;
+      end Add_Scope;
+
+   --  Start of processing for Get_Qualified_Name
+
+   begin
+      Name_Len := 0;
+      Add_Scope (Scop);
+
+      --  Append the base name after all scopes have been chained
+
+      Get_Name_String_And_Append (Nam);
+
+      --  Append the suffix (if present)
+
+      if Suffix /= No_Name then
+         Add_Str_To_Name_Buffer ("__");
+         Get_Name_String_And_Append (Suffix);
+      end if;
+
+      return Name_Find;
+   end Get_Qualified_Name;
+
    -----------------------
    -- Get_Reason_String --
    -----------------------
@@ -8357,6 +8421,71 @@ package body Sem_Util is
       return Empty;
    end Get_User_Defined_Eq;
 
+   ---------------
+   -- Get_Views --
+   ---------------
+
+   procedure Get_Views
+     (Typ       : Entity_Id;
+      Priv_Typ  : out Entity_Id;
+      Full_Typ  : out Entity_Id;
+      Full_Base : out Entity_Id;
+      CRec_Typ  : out Entity_Id)
+   is
+      IP_View : Entity_Id;
+
+   begin
+      --  Assume that none of the views can be recovered
+
+      Priv_Typ  := Empty;
+      Full_Typ  := Empty;
+      Full_Base := Empty;
+      CRec_Typ  := Empty;
+
+      --  The input type is the corresponding record type of a protected or a
+      --  task type.
+
+      if Ekind (Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Typ)
+      then
+         CRec_Typ  := Typ;
+         Full_Typ  := Corresponding_Concurrent_Type (CRec_Typ);
+         Full_Base := Base_Type (Full_Typ);
+         Priv_Typ  := Incomplete_Or_Partial_View (Full_Typ);
+
+      --  Otherwise the input type denotes an arbitrary type
+
+      else
+         IP_View := Incomplete_Or_Partial_View (Typ);
+
+         --  The input type denotes the full view of a private type
+
+         if Present (IP_View) then
+            Priv_Typ := IP_View;
+            Full_Typ := Typ;
+
+         --  The input type is a private type
+
+         elsif Is_Private_Type (Typ) then
+            Priv_Typ := Typ;
+            Full_Typ := Full_View (Priv_Typ);
+
+         --  Otherwise the input type does not have any views
+
+         else
+            Full_Typ := Typ;
+         end if;
+
+         if Present (Full_Typ) then
+            Full_Base := Base_Type (Full_Typ);
+
+            if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then
+               CRec_Typ := Corresponding_Record_Type (Full_Typ);
+            end if;
+         end if;
+      end if;
+   end Get_Views;
+
    -----------------------
    -- Has_Access_Values --
    -----------------------
@@ -8538,7 +8667,6 @@ package body Sem_Util is
          elsif Nkind (Expr) = N_Indexed_Component then
             declare
                Typ : constant Entity_Id := Etype (Prefix (Expr));
-               Ind : constant Node_Id   := First_Index (Typ);
 
             begin
                --  Packing generates unknown alignment if layout is not done
@@ -8547,22 +8675,12 @@ package body Sem_Util is
                   Set_Result (Unknown);
                end if;
 
-               --  Check prefix and component offset
+               --  Check prefix and component offset (or at least size)
 
                Check_Prefix;
-               Offs := Component_Size (Typ);
-
-               --  Small optimization: compute the full offset when possible
-
-               if Offs /= No_Uint
-                 and then Offs > Uint_0
-                 and then Present (Ind)
-                 and then Nkind (Ind) = N_Range
-                 and then Compile_Time_Known_Value (Low_Bound (Ind))
-                 and then Compile_Time_Known_Value (First (Expressions (Expr)))
-               then
-                  Offs := Offs * (Expr_Value (First (Expressions (Expr)))
-                                    - Expr_Value (Low_Bound ((Ind))));
+               Offs := Indexed_Component_Bit_Offset (Expr);
+               if Offs = No_Uint then
+                  Offs := Component_Size (Typ);
                end if;
             end;
          end if;
@@ -9098,39 +9216,20 @@ package body Sem_Util is
    -------------------------------------
 
    function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
-      Arg  : Node_Id;
       Comp : Entity_Id;
       Prag : Node_Id;
 
    begin
-      --  A private type and its full view is fully default initialized when it
-      --  is subject to pragma Default_Initial_Condition without an argument or
-      --  with a non-null argument. Since any type may act as the full view of
-      --  a private type, this check must be performed prior to the specialized
-      --  tests below.
+      --  A type subject to pragma Default_Initial_Condition is fully default
+      --  initialized when the pragma appears with a non-null argument. Since
+      --  any type may act as the full view of a private type, this check must
+      --  be performed prior to the specialized tests below.
 
-      if Has_Default_Init_Cond (Typ)
-        or else Has_Inherited_Default_Init_Cond (Typ)
-      then
+      if Has_DIC (Typ) then
          Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-
-         --  Pragma Default_Initial_Condition must be present if one of the
-         --  related entity flags is set.
-
          pragma Assert (Present (Prag));
-         Arg := First (Pragma_Argument_Associations (Prag));
-
-         --  A non-null argument guarantees full default initialization
 
-         if Present (Arg) then
-            return Nkind (Arg) /= N_Null;
-
-         --  Otherwise the missing argument defaults the pragma to "True" which
-         --  is considered a non-null argument (see above).
-
-         else
-            return True;
-         end if;
+         return Is_Verifiable_DIC_Pragma (Prag);
       end if;
 
       --  A scalar type is fully default initialized if it is subject to aspect
@@ -9148,7 +9247,7 @@ package body Sem_Util is
            Has_Default_Aspect (Typ)
              or else Has_Full_Default_Initialization (Component_Type (Typ));
 
-      --  A protected type, record type or type extension is fully default
+      --  A protected type, record type, or type extension is fully default
       --  initialized if all its components either carry an initialization
       --  expression or have a type that is fully default initialized. The
       --  parent type of a type extension must be fully default initialized.
@@ -9280,15 +9379,25 @@ package body Sem_Util is
       return False;
    end Has_Interfaces;
 
+   --------------------------
+   -- Has_Max_Queue_Length --
+   --------------------------
+
+   function Has_Max_Queue_Length (Id : Entity_Id) return Boolean is
+   begin
+      return
+        Ekind (Id) = E_Entry
+          and then Present (Get_Pragma (Id, Pragma_Max_Queue_Length));
+   end Has_Max_Queue_Length;
+
    ---------------------------------
    -- Has_No_Obvious_Side_Effects --
    ---------------------------------
 
    function Has_No_Obvious_Side_Effects (N : Node_Id) return Boolean is
    begin
-      --  For now, just handle literals, constants, and non-volatile
-      --  variables and expressions combining these with operators or
-      --  short circuit forms.
+      --  For now handle literals, constants, and non-volatile variables and
+      --  expressions combining these with operators or short circuit forms.
 
       if Nkind (N) in N_Numeric_Or_String_Literal then
          return True;
@@ -9329,19 +9438,78 @@ package body Sem_Util is
    -----------------------------
 
    function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean is
+      Constits : Elist_Id;
+
    begin
       pragma Assert (Ekind (Id) = E_Abstract_State);
+      Constits := Refinement_Constituents (Id);
 
       --  For a refinement to be non-null, the first constituent must be
       --  anything other than null.
 
-      if Present (Refinement_Constituents (Id)) then
-         return
-           Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
+      return
+        Present (Constits)
+          and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
+   end Has_Non_Null_Refinement;
+
+   -------------------
+   -- Has_Null_Body --
+   -------------------
+
+   function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
+      Body_Id : Entity_Id;
+      Decl    : Node_Id;
+      Spec    : Node_Id;
+      Stmt1   : Node_Id;
+      Stmt2   : Node_Id;
+
+   begin
+      Spec := Parent (Proc_Id);
+      Decl := Parent (Spec);
+
+      --  Retrieve the entity of the procedure body (e.g. invariant proc).
+
+      if Nkind (Spec) = N_Procedure_Specification
+        and then Nkind (Decl) = N_Subprogram_Declaration
+      then
+         Body_Id := Corresponding_Body (Decl);
+
+      --  The body acts as a spec
+
+      else
+         Body_Id := Proc_Id;
+      end if;
+
+      --  The body will be generated later
+
+      if No (Body_Id) then
+         return False;
+      end if;
+
+      Spec := Parent (Body_Id);
+      Decl := Parent (Spec);
+
+      pragma Assert
+        (Nkind (Spec) = N_Procedure_Specification
+          and then Nkind (Decl) = N_Subprogram_Body);
+
+      Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
+
+      --  Look for a null statement followed by an optional return
+      --  statement.
+
+      if Nkind (Stmt1) = N_Null_Statement then
+         Stmt2 := Next (Stmt1);
+
+         if Present (Stmt2) then
+            return Nkind (Stmt2) = N_Simple_Return_Statement;
+         else
+            return True;
+         end if;
       end if;
 
       return False;
-   end Has_Non_Null_Refinement;
+   end Has_Null_Body;
 
    ------------------------
    -- Has_Null_Exclusion --
@@ -9438,18 +9606,18 @@ package body Sem_Util is
    -------------------------
 
    function Has_Null_Refinement (Id : Entity_Id) return Boolean is
+      Constits : Elist_Id;
+
    begin
       pragma Assert (Ekind (Id) = E_Abstract_State);
+      Constits := Refinement_Constituents (Id);
 
       --  For a refinement to be null, the state's sole constituent must be a
       --  null.
 
-      if Present (Refinement_Constituents (Id)) then
-         return
-           Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
-      end if;
-
-      return False;
+      return
+        Present (Constits)
+          and then Nkind (Node (First_Elmt (Constits))) = N_Null;
    end Has_Null_Refinement;
 
    -------------------------------
@@ -10085,6 +10253,58 @@ package body Sem_Util is
       return Name_Find;
    end Remove_Suffix;
 
+   ----------------------------------
+   -- Replace_Null_By_Null_Address --
+   ----------------------------------
+
+   procedure Replace_Null_By_Null_Address (N : Node_Id) is
+      procedure Replace_Null_Operand (Op : Node_Id; Other_Op : Node_Id);
+      --  Replace operand Op with a reference to Null_Address when the operand
+      --  denotes a null Address. Other_Op denotes the other operand.
+
+      --------------------------
+      -- Replace_Null_Operand --
+      --------------------------
+
+      procedure Replace_Null_Operand (Op : Node_Id; Other_Op : Node_Id) is
+      begin
+         --  Check the type of the complementary operand since the N_Null node
+         --  has not been decorated yet.
+
+         if Nkind (Op) = N_Null
+           and then Is_Descendant_Of_Address (Etype (Other_Op))
+         then
+            Rewrite (Op, New_Occurrence_Of (RTE (RE_Null_Address), Sloc (Op)));
+         end if;
+      end Replace_Null_Operand;
+
+   --  Start of processing for Replace_Null_By_Null_Address
+
+   begin
+      pragma Assert (Relaxed_RM_Semantics);
+      pragma Assert (Nkind_In (N, N_Null,
+                                  N_Op_Eq,
+                                  N_Op_Ge,
+                                  N_Op_Gt,
+                                  N_Op_Le,
+                                  N_Op_Lt,
+                                  N_Op_Ne));
+
+      if Nkind (N) = N_Null then
+         Rewrite (N, New_Occurrence_Of (RTE (RE_Null_Address), Sloc (N)));
+
+      else
+         declare
+            L : constant Node_Id := Left_Opnd  (N);
+            R : constant Node_Id := Right_Opnd (N);
+
+         begin
+            Replace_Null_Operand (L, Other_Op => R);
+            Replace_Null_Operand (R, Other_Op => L);
+         end;
+      end if;
+   end Replace_Null_By_Null_Address;
+
    --------------------------
    -- Has_Tagged_Component --
    --------------------------
@@ -10298,6 +10518,26 @@ package body Sem_Util is
           and then Assertion_Expression_Pragma (Get_Pragma_Id (Prag));
    end In_Assertion_Expression_Pragma;
 
+   ----------------------
+   -- In_Generic_Scope --
+   ----------------------
+
+   function In_Generic_Scope (E : Entity_Id) return Boolean is
+      S : Entity_Id;
+
+   begin
+      S := Scope (E);
+      while Present (S) and then S /= Standard_Standard loop
+         if Is_Generic_Unit (S) then
+            return True;
+         end if;
+
+         S := Scope (S);
+      end loop;
+
+      return False;
+   end In_Generic_Scope;
+
    -----------------
    -- In_Instance --
    -----------------
@@ -10474,6 +10714,51 @@ package body Sem_Util is
       end loop;
    end In_Pragma_Expression;
 
+   ---------------------------
+   -- In_Pre_Post_Condition --
+   ---------------------------
+
+   function In_Pre_Post_Condition (N : Node_Id) return Boolean is
+      Par     : Node_Id;
+      Prag    : Node_Id := Empty;
+      Prag_Id : Pragma_Id;
+
+   begin
+      --  Climb the parent chain looking for an enclosing pragma
+
+      Par := N;
+      while Present (Par) loop
+         if Nkind (Par) = N_Pragma then
+            Prag := Par;
+            exit;
+
+         --  Prevent the search from going too far
+
+         elsif Is_Body_Or_Package_Declaration (Par) then
+            exit;
+         end if;
+
+         Par := Parent (Par);
+      end loop;
+
+      if Present (Prag) then
+         Prag_Id := Get_Pragma_Id (Prag);
+
+         return
+           Prag_Id = Pragma_Post
+             or else Prag_Id = Pragma_Post_Class
+             or else Prag_Id = Pragma_Postcondition
+             or else Prag_Id = Pragma_Pre
+             or else Prag_Id = Pragma_Pre_Class
+             or else Prag_Id = Pragma_Precondition;
+
+      --  Otherwise the node is not enclosed by a pre/postcondition pragma
+
+      else
+         return False;
+      end if;
+   end In_Pre_Post_Condition;
+
    -------------------------------------
    -- In_Reverse_Storage_Order_Object --
    -------------------------------------
@@ -10578,20 +10863,31 @@ package body Sem_Util is
          while Present (Decl) loop
             Match := Empty;
 
+            --  The partial view of a Taft-amendment type is an incomplete
+            --  type.
+
             if Taft then
                if Nkind (Decl) = N_Incomplete_Type_Declaration then
                   Match := Defining_Identifier (Decl);
                end if;
 
-            else
-               if Nkind_In (Decl, N_Private_Extension_Declaration,
+            --  Otherwise look for a private type whose full view matches the
+            --  input type. Note that this checks full_type_declaration nodes
+            --  to account for derivations from a private type where the type
+            --  declaration hold the partial view and the full view is an
+            --  itype.
+
+            elsif Nkind_In (Decl, N_Full_Type_Declaration,
+                                  N_Private_Extension_Declaration,
                                   N_Private_Type_Declaration)
-               then
-                  Match := Defining_Identifier (Decl);
-               end if;
+            then
+               Match := Defining_Identifier (Decl);
             end if;
 
+            --  Guard against unanalyzed entities
+
             if Present (Match)
+              and then Is_Type (Match)
               and then Present (Full_View (Match))
               and then Full_View (Match) = Id
             then
@@ -10630,7 +10926,9 @@ package body Sem_Util is
          Pkg_Decl : Node_Id := Pkg;
 
       begin
-         if Present (Pkg) and then Ekind (Pkg) = E_Package then
+         if Present (Pkg)
+           and then Ekind_In (Pkg, E_Generic_Package, E_Package)
+         then
             while Nkind (Pkg_Decl) /= N_Package_Specification loop
                Pkg_Decl := Parent (Pkg_Decl);
             end loop;
@@ -10666,79 +10964,201 @@ package body Sem_Util is
       return Empty;
    end Incomplete_Or_Partial_View;
 
-   -----------------------------------------
-   -- Inherit_Default_Init_Cond_Procedure --
-   -----------------------------------------
+   ----------------------------------
+   -- Indexed_Component_Bit_Offset --
+   ----------------------------------
+
+   function Indexed_Component_Bit_Offset (N : Node_Id) return Uint is
+      Exp : constant Node_Id   := First (Expressions (N));
+      Typ : constant Entity_Id := Etype (Prefix (N));
+      Off : constant Uint      := Component_Size (Typ);
+      Ind : Node_Id;
+
+   begin
+      --  Return early if the component size is not known or variable
+
+      if Off = No_Uint or else Off < Uint_0 then
+         return No_Uint;
+      end if;
+
+      --  Deal with the degenerate case of an empty component
+
+      if Off = Uint_0 then
+         return Off;
+      end if;
+
+      --  Check that both the index value and the low bound are known
+
+      if not Compile_Time_Known_Value (Exp) then
+         return No_Uint;
+      end if;
+
+      Ind := First_Index (Typ);
+      if No (Ind) then
+         return No_Uint;
+      end if;
+
+      if Nkind (Ind) = N_Subtype_Indication then
+         Ind := Constraint (Ind);
 
-   procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id) is
-      Par_Typ : constant Entity_Id := Etype (Typ);
+         if Nkind (Ind) = N_Range_Constraint then
+            Ind := Range_Expression (Ind);
+         end if;
+      end if;
+
+      if Nkind (Ind) /= N_Range
+        or else not Compile_Time_Known_Value (Low_Bound (Ind))
+      then
+         return No_Uint;
+      end if;
 
-   begin
-      --  A derived type inherits the default initial condition procedure of
-      --  its parent type.
+      --  Return the scaled offset
 
-      if No (Default_Init_Cond_Procedure (Typ)) then
-         Set_Default_Init_Cond_Procedure
-           (Typ, Default_Init_Cond_Procedure (Par_Typ));
-      end if;
-   end Inherit_Default_Init_Cond_Procedure;
+      return Off * (Expr_Value (Exp) - Expr_Value (Low_Bound ((Ind))));
+   end Indexed_Component_Bit_Offset;
 
    ----------------------------
    -- Inherit_Rep_Item_Chain --
    ----------------------------
 
    procedure Inherit_Rep_Item_Chain (Typ : Entity_Id; From_Typ : Entity_Id) is
-      From_Item : constant Node_Id := First_Rep_Item (From_Typ);
-      Item      : Node_Id := Empty;
-      Last_Item : Node_Id := Empty;
+      Item      : Node_Id;
+      Next_Item : Node_Id;
 
    begin
-      --  Reach the end of the destination type's chain (if any) and capture
-      --  the last item.
+      --  There are several inheritance scenarios to consider depending on
+      --  whether both types have rep item chains and whether the destination
+      --  type already inherits part of the source type's rep item chain.
 
-      Item := First_Rep_Item (Typ);
-      while Present (Item) loop
+      --  1) The source type lacks a rep item chain
+      --     From_Typ ---> Empty
+      --
+      --     Typ --------> Item (or Empty)
 
-         --  Do not inherit a chain that has been inherited already
+      --  In this case inheritance cannot take place because there are no items
+      --  to inherit.
 
-         if Item = From_Item then
-            return;
-         end if;
+      --  2) The destination type lacks a rep item chain
+      --     From_Typ ---> Item ---> ...
+      --
+      --     Typ --------> Empty
 
-         Last_Item := Item;
-         Item := Next_Rep_Item (Item);
-      end loop;
+      --  Inheritance takes place by setting the First_Rep_Item of the
+      --  destination type to the First_Rep_Item of the source type.
+      --     From_Typ ---> Item ---> ...
+      --                    ^
+      --     Typ -----------+
 
-      Item := First_Rep_Item (From_Typ);
+      --  3.1) Both source and destination types have at least one rep item.
+      --  The destination type does NOT inherit a rep item from the source
+      --  type.
+      --     From_Typ ---> Item ---> Item
+      --
+      --     Typ --------> Item ---> Item
 
-      --  Additional check when both parent and current type have rep.
-      --  items, to prevent circularities when the derivation completes
-      --  a private declaration and inherits from both views of the parent.
-      --  There may be a remaining problem with the proper ordering of
-      --  attribute specifications and aspects on the chains of the four
-      --  entities involved. ???
+      --  Inheritance takes place by setting the Next_Rep_Item of the last item
+      --  of the destination type to the First_Rep_Item of the source type.
+      --     From_Typ -------------------> Item ---> Item
+      --                                    ^
+      --     Typ --------> Item ---> Item --+
 
-      if Present (Item) and then Present (From_Item) then
-         while Present (Item) loop
-            if Item = First_Rep_Item (Typ) then
-               return;
-            end if;
+      --  3.2) Both source and destination types have at least one rep item.
+      --  The destination type DOES inherit part of the rep item chain of the
+      --  source type.
+      --     From_Typ ---> Item ---> Item ---> Item
+      --                              ^
+      --     Typ --------> Item ------+
 
-            Item := Next_Rep_Item (Item);
-         end loop;
-      end if;
+      --  This rare case arises when the full view of a private extension must
+      --  inherit the rep item chain from the full view of its parent type and
+      --  the full view of the parent type contains extra rep items. Currently
+      --  only invariants may lead to such form of inheritance.
+
+      --     type From_Typ is tagged private
+      --       with Type_Invariant'Class => Item_2;
+
+      --     type Typ is new From_Typ with private
+      --       with Type_Invariant => Item_4;
+
+      --  At this point the rep item chains contain the following items
+
+      --     From_Typ -----------> Item_2 ---> Item_3
+      --                            ^
+      --     Typ --------> Item_4 --+
+
+      --  The full views of both types may introduce extra invariants
 
-      --  When the destination type has a rep item chain, the chain of the
-      --  source type is appended to it.
+      --     type From_Typ is tagged null record
+      --       with Type_Invariant => Item_1;
 
-      if Present (Last_Item) then
-         Set_Next_Rep_Item (Last_Item, From_Item);
+      --     type Typ is new From_Typ with null record;
 
-      --  Otherwise the destination type directly inherits the rep item chain
-      --  of the source type (if any).
+      --  The full view of Typ would have to inherit any new rep items added to
+      --  the full view of From_Typ.
+
+      --     From_Typ -----------> Item_1 ---> Item_2 ---> Item_3
+      --                            ^
+      --     Typ --------> Item_4 --+
+
+      --  To achieve this form of inheritance, the destination type must first
+      --  sever the link between its own rep chain and that of the source type,
+      --  then inheritance 3.1 takes place.
+
+      --  Case 1: The source type lacks a rep item chain
+
+      if No (First_Rep_Item (From_Typ)) then
+         return;
+
+      --  Case 2: The destination type lacks a rep item chain
+
+      elsif No (First_Rep_Item (Typ)) then
+         Set_First_Rep_Item (Typ, First_Rep_Item (From_Typ));
+
+      --  Case 3: Both the source and destination types have at least one rep
+      --  item. Traverse the rep item chain of the destination type to find the
+      --  last rep item.
 
       else
-         Set_First_Rep_Item (Typ, From_Item);
+         Item      := Empty;
+         Next_Item := First_Rep_Item (Typ);
+         while Present (Next_Item) loop
+
+            --  Detect a link between the destination type's rep chain and that
+            --  of the source type. There are two possibilities:
+
+            --    Variant 1
+            --                  Next_Item
+            --                      V
+            --       From_Typ ---> Item_1 --->
+            --                      ^
+            --       Typ -----------+
+            --
+            --       Item is Empty
+
+            --    Variant 2
+            --                              Next_Item
+            --                                  V
+            --       From_Typ ---> Item_1 ---> Item_2 --->
+            --                                  ^
+            --       Typ --------> Item_3 ------+
+            --                      ^
+            --                     Item
+
+            if Has_Rep_Item (From_Typ, Next_Item) then
+               exit;
+            end if;
+
+            Item      := Next_Item;
+            Next_Item := Next_Rep_Item (Next_Item);
+         end loop;
+
+         --  Inherit the source type's rep item chain
+
+         if Present (Item) then
+            Set_Next_Rep_Item (Item, First_Rep_Item (From_Typ));
+         else
+            Set_First_Rep_Item (Typ, First_Rep_Item (From_Typ));
+         end if;
       end if;
    end Inherit_Rep_Item_Chain;
 
@@ -10824,7 +11244,7 @@ package body Sem_Util is
    ------------------------------------------
 
    procedure Inspect_Deferred_Constant_Completion (Decls : List_Id) is
-      Decl   : Node_Id;
+      Decl : Node_Id;
 
    begin
       Decl := First (Decls);
@@ -11635,7 +12055,7 @@ package body Sem_Util is
 
             elsif Nkind (P) = N_Pragma
               and then
-                Get_Pragma_Id (Pragma_Name (P)) = Pragma_Predicate_Failure
+                Get_Pragma_Id (P) = Pragma_Predicate_Failure
             then
                return True;
             end if;
@@ -11994,7 +12414,7 @@ package body Sem_Util is
             return True;
 
          --  An array type is effectively volatile when it is subject to pragma
-         --  Atomic_Components or Volatile_Components or its compolent type is
+         --  Atomic_Components or Volatile_Components or its component type is
          --  effectively volatile.
 
          elsif Is_Array_Type (Id) then
@@ -12039,9 +12459,6 @@ package body Sem_Util is
       if Is_Entity_Name (N) then
          return Is_Effectively_Volatile (Entity (N));
 
-      elsif Nkind (N) = N_Expanded_Name then
-         return Is_Effectively_Volatile (Entity (N));
-
       elsif Nkind (N) = N_Indexed_Component then
          return Is_Effectively_Volatile_Object (Prefix (N));
 
@@ -12078,6 +12495,19 @@ package body Sem_Util is
           and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Declaration;
    end Is_Entry_Declaration;
 
+   ------------------------------------
+   -- Is_Expanded_Priority_Attribute --
+   ------------------------------------
+
+   function Is_Expanded_Priority_Attribute (E : Entity_Id) return Boolean is
+   begin
+      return
+        Nkind (E) = N_Function_Call
+          and then not Configurable_Run_Time_Mode
+          and then (Entity (Name (E)) = RTE (RE_Get_Ceiling)
+                     or else Entity (Name (E)) = RTE (RO_PE_Get_Ceiling));
+   end Is_Expanded_Priority_Attribute;
+
    ----------------------------
    -- Is_Expression_Function --
    ----------------------------
@@ -12592,11 +13022,14 @@ package body Sem_Util is
 
       function Denotes_Iterator (Iter_Typ : Entity_Id) return Boolean is
       begin
+         --  Check that the name matches, and that the ultimate ancestor is in
+         --  a predefined unit, i.e the one that declares iterator interfaces.
+
          return
            Nam_In (Chars (Iter_Typ), Name_Forward_Iterator,
                                      Name_Reversible_Iterator)
              and then Is_Predefined_File_Name
-                        (Unit_File_Name (Get_Source_Unit (Iter_Typ)));
+                     (Unit_File_Name (Get_Source_Unit (Root_Type (Iter_Typ))));
       end Denotes_Iterator;
 
       --  Local variables
@@ -12758,20 +13191,16 @@ package body Sem_Util is
       end if;
    end Is_Local_Variable_Reference;
 
-   -----------------------------------------------
-   -- Is_Nontrivial_Default_Init_Cond_Procedure --
-   -----------------------------------------------
+   ---------------------------------
+   -- Is_Nontrivial_DIC_Procedure --
+   ---------------------------------
 
-   function Is_Nontrivial_Default_Init_Cond_Procedure
-     (Id : Entity_Id) return Boolean
-   is
+   function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean is
       Body_Decl : Node_Id;
-      Stmt : Node_Id;
+      Stmt      : Node_Id;
 
    begin
-      if Ekind (Id) = E_Procedure
-        and then Is_Default_Init_Cond_Procedure (Id)
-      then
+      if Ekind (Id) = E_Procedure and then Is_DIC_Procedure (Id) then
          Body_Decl :=
            Unit_Declaration_Node
              (Corresponding_Body (Unit_Declaration_Node (Id)));
@@ -12795,7 +13224,21 @@ package body Sem_Util is
       end if;
 
       return False;
-   end Is_Nontrivial_Default_Init_Cond_Procedure;
+   end Is_Nontrivial_DIC_Procedure;
+
+   -------------------------
+   -- Is_Null_Record_Type --
+   -------------------------
+
+   function Is_Null_Record_Type (T : Entity_Id) return Boolean is
+      Decl : constant Node_Id := Parent (T);
+   begin
+      return Nkind (Decl) = N_Full_Type_Declaration
+        and then Nkind (Type_Definition (Decl)) = N_Record_Definition
+        and then
+          (No (Component_List (Type_Definition (Decl)))
+            or else Null_Present (Component_List (Type_Definition (Decl))));
+   end Is_Null_Record_Type;
 
    -------------------------
    -- Is_Object_Reference --
@@ -12846,7 +13289,7 @@ package body Sem_Util is
             when N_Function_Call =>
                return Etype (N) /= Standard_Void_Type;
 
-            --  Attributes 'Input, 'Loop_Entry, 'Old and 'Result produce
+            --  Attributes 'Input, 'Loop_Entry, 'Old, and 'Result produce
             --  objects.
 
             when N_Attribute_Reference =>
@@ -13033,14 +13476,15 @@ package body Sem_Util is
    is
       function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean;
       --  Determine whether an arbitrary node denotes a call to a protected
-      --  entry, function or procedure in prefixed form where the prefix is
+      --  entry, function, or procedure in prefixed form where the prefix is
       --  Obj_Ref.
 
       function Within_Check (Nod : Node_Id) return Boolean;
       --  Determine whether an arbitrary node appears in a check node
 
       function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
-      --  Determine whether an arbitrary node appears in a procedure call
+      --  Determine whether an arbitrary node appears in an entry, function, or
+      --  procedure call.
 
       function Within_Volatile_Function (Id : Entity_Id) return Boolean;
       --  Determine whether an arbitrary entity appears in a volatile function
@@ -13064,14 +13508,14 @@ package body Sem_Util is
 
             return
               Pref = Obj_Ref
-              and then Present (Etype (Pref))
-              and then Is_Protected_Type (Etype (Pref))
-              and then Is_Entity_Name (Subp)
-              and then Present (Entity (Subp))
-              and then Ekind_In (Entity (Subp), E_Entry,
-                                 E_Entry_Family,
-                                 E_Function,
-                                 E_Procedure);
+                and then Present (Etype (Pref))
+                and then Is_Protected_Type (Etype (Pref))
+                and then Is_Entity_Name (Subp)
+                and then Present (Entity (Subp))
+                and then Ekind_In (Entity (Subp), E_Entry,
+                                                  E_Entry_Family,
+                                                  E_Function,
+                                                  E_Procedure);
          else
             return False;
          end if;
@@ -13092,7 +13536,7 @@ package body Sem_Util is
             if Nkind (Par) in N_Raise_xxx_Error then
                return True;
 
-               --  Prevent the search from going too far
+            --  Prevent the search from going too far
 
             elsif Is_Body_Or_Package_Declaration (Par) then
                exit;
@@ -13122,7 +13566,7 @@ package body Sem_Util is
             then
                return True;
 
-               --  Prevent the search from going too far
+            --  Prevent the search from going too far
 
             elsif Is_Body_Or_Package_Declaration (Par) then
                exit;
@@ -13168,8 +13612,8 @@ package body Sem_Util is
       if Nkind (Context) = N_Assignment_Statement then
          return True;
 
-         --  The volatile object is part of the initialization expression of
-         --  another object.
+      --  The volatile object is part of the initialization expression of
+      --  another object.
 
       elsif Nkind (Context) = N_Object_Declaration
         and then Present (Expression (Context))
@@ -13184,21 +13628,21 @@ package body Sem_Util is
          if Is_Return_Object (Obj_Id) then
             return Within_Volatile_Function (Obj_Id);
 
-            --  Otherwise this is a normal object initialization
+         --  Otherwise this is a normal object initialization
 
          else
             return True;
          end if;
 
-         --  The volatile object acts as the name of a renaming declaration
+      --  The volatile object acts as the name of a renaming declaration
 
       elsif Nkind (Context) = N_Object_Renaming_Declaration
         and then Name (Context) = Obj_Ref
       then
          return True;
 
-         --  The volatile object appears as an actual parameter in a call to an
-         --  instance of Unchecked_Conversion whose result is renamed.
+      --  The volatile object appears as an actual parameter in a call to an
+      --  instance of Unchecked_Conversion whose result is renamed.
 
       elsif Nkind (Context) = N_Function_Call
         and then Is_Entity_Name (Name (Context))
@@ -13207,14 +13651,14 @@ package body Sem_Util is
       then
          return True;
 
-         --  The volatile object is actually the prefix in a protected entry,
-         --  function, or procedure call.
+      --  The volatile object is actually the prefix in a protected entry,
+      --  function, or procedure call.
 
       elsif Is_Protected_Operation_Call (Context) then
          return True;
 
-         --  The volatile object appears as the expression of a simple return
-         --  statement that applies to a volatile function.
+      --  The volatile object appears as the expression of a simple return
+      --  statement that applies to a volatile function.
 
       elsif Nkind (Context) = N_Simple_Return_Statement
         and then Expression (Context) = Obj_Ref
@@ -13222,8 +13666,8 @@ package body Sem_Util is
          return
            Within_Volatile_Function (Return_Statement_Entity (Context));
 
-         --  The volatile object appears as the prefix of a name occurring in a
-         --  non-interfering context.
+      --  The volatile object appears as the prefix of a name occurring in a
+      --  non-interfering context.
 
       elsif Nkind_In (Context, N_Attribute_Reference,
                       N_Explicit_Dereference,
@@ -13237,8 +13681,25 @@ package body Sem_Util is
       then
          return True;
 
-         --  The volatile object appears as the expression of a type conversion
-         --  occurring in a non-interfering context.
+      --  The volatile object appears as the prefix of attributes Address,
+      --  Alignment, Component_Size, First_Bit, Last_Bit, Position, Size,
+      --  Storage_Size.
+
+      elsif Nkind (Context) = N_Attribute_Reference
+        and then Prefix (Context) = Obj_Ref
+        and then Nam_In (Attribute_Name (Context), Name_Address,
+                                                   Name_Alignment,
+                                                   Name_Component_Size,
+                                                   Name_First_Bit,
+                                                   Name_Last_Bit,
+                                                   Name_Position,
+                                                   Name_Size,
+                                                   Name_Storage_Size)
+      then
+         return True;
+
+      --  The volatile object appears as the expression of a type conversion
+      --  occurring in a non-interfering context.
 
       elsif Nkind_In (Context, N_Type_Conversion,
                       N_Unchecked_Type_Conversion)
@@ -13249,21 +13710,22 @@ package body Sem_Util is
       then
          return True;
 
-         --  Allow references to volatile objects in various checks. This is
-         --  not a direct SPARK 2014 requirement.
+      --  Allow references to volatile objects in various checks. This is not a
+      --  direct SPARK 2014 requirement.
 
       elsif Within_Check (Context) then
          return True;
 
-         --  Assume that references to effectively volatile objects that appear
-         --  as actual parameters in a subprogram call are always legal. A full
-         --  legality check is done when the actuals are resolved.
+      --  Assume that references to effectively volatile objects that appear
+      --  as actual parameters in a subprogram call are always legal. A full
+      --  legality check is done when the actuals are resolved (see routine
+      --  Resolve_Actuals).
 
       elsif Within_Subprogram_Call (Context) then
          return True;
 
-         --  Otherwise the context is not suitable for an effectively volatile
-         --  object.
+      --  Otherwise the context is not suitable for an effectively volatile
+      --  object.
 
       else
          return False;
@@ -13575,7 +14037,7 @@ package body Sem_Util is
 
    begin
       --  Verify that prefix is analyzed and has the proper form. Note that
-      --  the attributes Elab_Spec, Elab_Body and Elab_Subp_Body which also
+      --  the attributes Elab_Spec, Elab_Body, and Elab_Subp_Body, which also
       --  produce the address of an entity, do not analyze their prefix
       --  because they denote entities that are not necessarily visible.
       --  Neither of them can apply to a protected type.
@@ -14286,7 +14748,8 @@ package body Sem_Util is
 
    begin
       --  Look for a function whose generic parent is the predefined intrinsic
-      --  function Unchecked_Conversion.
+      --  function Unchecked_Conversion, or for one that renames such an
+      --  instance.
 
       if Ekind (Id) = E_Function then
          Par := Parent (Id);
@@ -14294,12 +14757,17 @@ package body Sem_Util is
          if Nkind (Par) = N_Function_Specification then
             Par := Generic_Parent (Par);
 
-            return
-              Present (Par)
-                and then Chars (Par) = Name_Unchecked_Conversion
-                and then Is_Intrinsic_Subprogram (Par)
-                and then Is_Predefined_File_Name
-                           (Unit_File_Name (Get_Source_Unit (Par)));
+            if Present (Par) then
+               return
+                 Chars (Par) = Name_Unchecked_Conversion
+                   and then Is_Intrinsic_Subprogram (Par)
+                   and then Is_Predefined_File_Name
+                              (Unit_File_Name (Get_Source_Unit (Par)));
+            else
+               return
+                 Present (Alias (Id))
+                   and then Is_Unchecked_Conversion_Instance (Alias (Id));
+            end if;
          end if;
       end if;
 
@@ -14617,6 +15085,21 @@ package body Sem_Util is
       end if;
    end Is_Variable;
 
+   ------------------------------
+   -- Is_Verifiable_DIC_Pragma --
+   ------------------------------
+
+   function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
+      Args : constant List_Id := Pragma_Argument_Associations (Prag);
+
+   begin
+      --  To qualify as verifiable, a DIC pragma must have a non-null argument
+
+      return
+        Present (Args)
+          and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
+   end Is_Verifiable_DIC_Pragma;
+
    ---------------------------
    -- Is_Visibly_Controlled --
    ---------------------------
@@ -14635,17 +15118,11 @@ package body Sem_Util is
 
    function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean is
    begin
-      --  The caller must ensure that Func_Id denotes a function
-
       pragma Assert (Ekind_In (Func_Id, E_Function, E_Generic_Function));
 
-      --  A protected function is automatically volatile
+      --  A function declared within a protected type is volatile
 
-      if Is_Primitive (Func_Id)
-        and then Present (First_Formal (Func_Id))
-        and then Is_Protected_Type (Etype (First_Formal (Func_Id)))
-        and then Etype (First_Formal (Func_Id)) = Scope (Func_Id)
-      then
+      if Is_Protected_Type (Scope (Func_Id)) then
          return True;
 
       --  An instance of Ada.Unchecked_Conversion is a volatile function if
@@ -14908,7 +15385,7 @@ package body Sem_Util is
          when N_Assignment_Statement =>
             return N = Name (P);
 
-            --  Function call arguments are never lvalues
+         --  Function call arguments are never lvalues
 
          when N_Function_Call =>
             return False;
@@ -15157,11 +15634,15 @@ package body Sem_Util is
             return N = Name (P);
 
          --  Test prefix of component or attribute. Note that the prefix of an
-         --  explicit or implicit dereference cannot be an l-value.
+         --  explicit or implicit dereference cannot be an l-value. In the case
+         --  of a 'Read attribute, the reference can be an actual in the
+         --  argument list of the attribute.
 
          when N_Attribute_Reference =>
-            return N = Prefix (P)
-              and then Name_Implies_Lvalue_Prefix (Attribute_Name (P));
+            return (N = Prefix (P)
+                     and then Name_Implies_Lvalue_Prefix (Attribute_Name (P)))
+                 or else
+                   Attribute_Name (P) = Name_Read;
 
          --  For an expanded name, the name is an lvalue if the expanded name
          --  is an lvalue, but the prefix is never an lvalue, since it is just
@@ -15547,9 +16028,9 @@ package body Sem_Util is
 
    function New_Copy_Tree
      (Source    : Node_Id;
-      Map       : Elist_Id := No_Elist;
+      Map       : Elist_Id   := No_Elist;
       New_Sloc  : Source_Ptr := No_Location;
-      New_Scope : Entity_Id := Empty) return Node_Id
+      New_Scope : Entity_Id  := Empty) return Node_Id
    is
       Actual_Map : Elist_Id := Map;
       --  This is the actual map for the copy. It is initialized with the
@@ -15721,7 +16202,7 @@ package body Sem_Util is
 
       procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id) is
       begin
-         --  Translate Next_Entity, Scope and Etype fields, in case they
+         --  Translate Next_Entity, Scope, and Etype fields, in case they
          --  reference entities that have been mapped into copies.
 
          Set_Next_Entity (New_Itype, Assoc (Next_Entity (New_Itype)));
@@ -16759,9 +17240,24 @@ package body Sem_Util is
                  and then Actual /= Last
                  and then No (Next_Named_Actual (Actual))
                then
-                  Error_Msg_N ("unmatched actual & in call",
-                    Selector_Name (Actual));
-                  exit;
+                  --  A validity check may introduce a copy of a call that
+                  --  includes an extra actual (for example for an unrelated
+                  --  accessibility check). Check that the extra actual matches
+                  --  some extra formal, which must exist already because
+                  --  subprogram must be frozen at this point.
+
+                  if Present (Extra_Formals (S))
+                    and then not Comes_From_Source (Actual)
+                    and then Nkind (Actual) = N_Parameter_Association
+                    and then Chars (Extra_Formals (S)) =
+                               Chars (Selector_Name (Actual))
+                  then
+                     null;
+                  else
+                     Error_Msg_N
+                       ("unmatched actual & in call", Selector_Name (Actual));
+                     exit;
+                  end if;
                end if;
 
                Next (Actual);
@@ -16877,11 +17373,20 @@ package body Sem_Util is
                if Comes_From_Source (Exp)
                  or else Modification_Comes_From_Source
                then
-                  --  Give warning if pragma unmodified given and we are
+                  --  Give warning if pragma unmodified is given and we are
                   --  sure this is a modification.
 
                   if Has_Pragma_Unmodified (Ent) and then Sure then
-                     Error_Msg_NE ("??pragma Unmodified given for &!", N, Ent);
+
+                     --  Note that the entity may be present only as a result
+                     --  of pragma Unused.
+
+                     if Has_Pragma_Unused (Ent) then
+                        Error_Msg_NE ("??pragma Unused given for &!", N, Ent);
+                     else
+                        Error_Msg_NE
+                          ("??pragma Unmodified given for &!", N, Ent);
+                     end if;
                   end if;
 
                   Set_Never_Set_In_Source (Ent, False);
@@ -16994,6 +17499,44 @@ package body Sem_Util is
       end loop;
    end Note_Possible_Modification;
 
+   --------------------------------------
+   --  Null_To_Null_Address_Convert_OK --
+   --------------------------------------
+
+   function Null_To_Null_Address_Convert_OK
+     (N   : Node_Id;
+      Typ : Entity_Id := Empty) return Boolean
+   is
+   begin
+      if not Relaxed_RM_Semantics then
+         return False;
+      end if;
+
+      if Nkind (N) = N_Null then
+         return Present (Typ) and then Is_Descendant_Of_Address (Typ);
+
+      elsif Nkind_In (N, N_Op_Eq, N_Op_Ge, N_Op_Gt, N_Op_Le, N_Op_Lt, N_Op_Ne)
+      then
+         declare
+            L : constant Node_Id := Left_Opnd (N);
+            R : constant Node_Id := Right_Opnd (N);
+
+         begin
+            --  We check the Etype of the complementary operand since the
+            --  N_Null node is not decorated at this stage.
+
+            return
+              ((Nkind (L) = N_Null
+                 and then Is_Descendant_Of_Address (Etype (R)))
+              or else
+               (Nkind (R) = N_Null
+                 and then Is_Descendant_Of_Address (Etype (L))));
+         end;
+      end if;
+
+      return False;
+   end Null_To_Null_Address_Convert_OK;
+
    -------------------------
    -- Object_Access_Level --
    -------------------------
@@ -17393,6 +17936,41 @@ package body Sem_Util is
       end if;
    end Original_Corresponding_Operation;
 
+   -------------------
+   -- Output_Entity --
+   -------------------
+
+   procedure Output_Entity (Id : Entity_Id) is
+      Scop : Entity_Id;
+
+   begin
+      Scop := Scope (Id);
+
+      --  The entity may lack a scope when it is in the process of being
+      --  analyzed. Use the current scope as an approximation.
+
+      if No (Scop) then
+         Scop := Current_Scope;
+      end if;
+
+      Output_Name (Chars (Id), Scop);
+   end Output_Entity;
+
+   -----------------
+   -- Output_Name --
+   -----------------
+
+   procedure Output_Name (Nam : Name_Id; Scop : Entity_Id := Current_Scope) is
+   begin
+      Write_Str
+        (Get_Name_String
+          (Get_Qualified_Name
+            (Nam    => Nam,
+             Suffix => No_Name,
+             Scop   => Scop)));
+      Write_Eol;
+   end Output_Name;
+
    ----------------------
    -- Policy_In_Effect --
    ----------------------
@@ -17612,7 +18190,6 @@ package body Sem_Util is
    ---------------------------
 
    function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean is
-
       function Non_Internal_Name (E : Entity_Id) return Name_Id;
       --  Given an internal name, returns the corresponding non-internal name
 
@@ -17832,6 +18409,127 @@ package body Sem_Util is
       Set_Sloc (Endl, Loc);
    end Process_End_Label;
 
+   --------------------------------
+   -- Propagate_Concurrent_Flags --
+   --------------------------------
+
+   procedure Propagate_Concurrent_Flags
+     (Typ      : Entity_Id;
+      Comp_Typ : Entity_Id)
+   is
+   begin
+      if Has_Task (Comp_Typ) then
+         Set_Has_Task (Typ);
+      end if;
+
+      if Has_Protected (Comp_Typ) then
+         Set_Has_Protected (Typ);
+      end if;
+
+      if Has_Timing_Event (Comp_Typ) then
+         Set_Has_Timing_Event (Typ);
+      end if;
+   end Propagate_Concurrent_Flags;
+
+   ------------------------------
+   -- Propagate_DIC_Attributes --
+   ------------------------------
+
+   procedure Propagate_DIC_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id)
+   is
+      DIC_Proc : Entity_Id;
+
+   begin
+      if Present (Typ) and then Present (From_Typ) then
+         pragma Assert (Is_Type (Typ) and then Is_Type (From_Typ));
+
+         --  Nothing to do if both the source and the destination denote the
+         --  same type.
+
+         if From_Typ = Typ then
+            return;
+         end if;
+
+         DIC_Proc := DIC_Procedure (From_Typ);
+
+         --  The setting of the attributes is intentionally conservative. This
+         --  prevents accidental clobbering of enabled attributes.
+
+         if Has_Inherited_DIC (From_Typ)
+           and then not Has_Inherited_DIC (Typ)
+         then
+            Set_Has_Inherited_DIC (Typ);
+         end if;
+
+         if Has_Own_DIC (From_Typ) and then not Has_Own_DIC (Typ) then
+            Set_Has_Own_DIC (Typ);
+         end if;
+
+         if Present (DIC_Proc) and then No (DIC_Procedure (Typ)) then
+            Set_DIC_Procedure (Typ, DIC_Proc);
+         end if;
+      end if;
+   end Propagate_DIC_Attributes;
+
+   ------------------------------------
+   -- Propagate_Invariant_Attributes --
+   ------------------------------------
+
+   procedure Propagate_Invariant_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id)
+   is
+      Full_IP : Entity_Id;
+      Part_IP : Entity_Id;
+
+   begin
+      if Present (Typ) and then Present (From_Typ) then
+         pragma Assert (Is_Type (Typ) and then Is_Type (From_Typ));
+
+         --  Nothing to do if both the source and the destination denote the
+         --  same type.
+
+         if From_Typ = Typ then
+            return;
+         end if;
+
+         Full_IP := Invariant_Procedure (From_Typ);
+         Part_IP := Partial_Invariant_Procedure (From_Typ);
+
+         --  The setting of the attributes is intentionally conservative. This
+         --  prevents accidental clobbering of enabled attributes.
+
+         if Has_Inheritable_Invariants (From_Typ)
+           and then not Has_Inheritable_Invariants (Typ)
+         then
+            Set_Has_Inheritable_Invariants (Typ, True);
+         end if;
+
+         if Has_Inherited_Invariants (From_Typ)
+           and then not Has_Inherited_Invariants (Typ)
+         then
+            Set_Has_Inherited_Invariants (Typ, True);
+         end if;
+
+         if Has_Own_Invariants (From_Typ)
+           and then not Has_Own_Invariants (Typ)
+         then
+            Set_Has_Own_Invariants (Typ, True);
+         end if;
+
+         if Present (Full_IP) and then No (Invariant_Procedure (Typ)) then
+            Set_Invariant_Procedure (Typ, Full_IP);
+         end if;
+
+         if Present (Part_IP) and then No (Partial_Invariant_Procedure (Typ))
+         then
+            Set_Partial_Invariant_Procedure (Typ, Part_IP);
+         end if;
+      end if;
+   end Propagate_Invariant_Attributes;
+
    ---------------------------------------
    -- Record_Possible_Part_Of_Reference --
    ---------------------------------------
@@ -18106,81 +18804,6 @@ package body Sem_Util is
       end if;
    end Require_Entity;
 
-   -------------------------------
-   -- Requires_State_Refinement --
-   -------------------------------
-
-   function Requires_State_Refinement
-     (Spec_Id : Entity_Id;
-      Body_Id : Entity_Id) return Boolean
-   is
-      function Mode_Is_Off (Prag : Node_Id) return Boolean;
-      --  Given pragma SPARK_Mode, determine whether the mode is Off
-
-      -----------------
-      -- Mode_Is_Off --
-      -----------------
-
-      function Mode_Is_Off (Prag : Node_Id) return Boolean is
-         Mode : Node_Id;
-
-      begin
-         --  The default SPARK mode is On
-
-         if No (Prag) then
-            return False;
-         end if;
-
-         Mode := Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
-
-         --  Then the pragma lacks an argument, the default mode is On
-
-         if No (Mode) then
-            return False;
-         else
-            return Chars (Mode) = Name_Off;
-         end if;
-      end Mode_Is_Off;
-
-   --  Start of processing for Requires_State_Refinement
-
-   begin
-      --  A package that does not define at least one abstract state cannot
-      --  possibly require refinement.
-
-      if No (Abstract_States (Spec_Id)) then
-         return False;
-
-      --  The package instroduces a single null state which does not merit
-      --  refinement.
-
-      elsif Has_Null_Abstract_State (Spec_Id) then
-         return False;
-
-      --  Check whether the package body is subject to pragma SPARK_Mode. If
-      --  it is and the mode is Off, the package body is considered to be in
-      --  regular Ada and does not require refinement.
-
-      elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
-         return False;
-
-      --  The body's SPARK_Mode may be inherited from a similar pragma that
-      --  appears in the private declarations of the spec. The pragma we are
-      --  interested appears as the second entry in SPARK_Pragma.
-
-      elsif Present (SPARK_Pragma (Spec_Id))
-        and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
-      then
-         return False;
-
-      --  The spec defines at least one abstract state and the body has no way
-      --  of circumventing the refinement.
-
-      else
-         return True;
-      end if;
-   end Requires_State_Refinement;
-
    ------------------------------
    -- Requires_Transient_Scope --
    ------------------------------
@@ -19748,8 +20371,8 @@ package body Sem_Util is
          return False;
       end if;
 
-      --  Check that the size of the component is 8, 16, 32 or 64 bits and that
-      --  Typ is properly aligned.
+      --  Check that the size of the component is 8, 16, 32, or 64 bits and
+      --  that Typ is properly aligned.
 
       case Size is
          when 8 | 16 | 32 | 64 =>
@@ -20065,13 +20688,27 @@ package body Sem_Util is
             if Nkind (Parent (E)) = N_Entry_Body then
                declare
                   Prot_Item : Entity_Id;
+                  Prot_Type : Entity_Id;
+
                begin
+                  if Ekind (E) = E_Entry then
+                     Prot_Type := Scope (E);
+
+                  --  Bodies of entry families are nested within an extra scope
+                  --  that contains an entry index declaration
+
+                  else
+                     Prot_Type := Scope (Scope (E));
+                  end if;
+
+                  pragma Assert (Ekind (Prot_Type) = E_Protected_Type);
+
                   --  Traverse the entity list of the protected type and locate
                   --  an entry declaration which matches the entry body.
 
-                  Prot_Item := First_Entity (Scope (E));
+                  Prot_Item := First_Entity (Prot_Type);
                   while Present (Prot_Item) loop
-                     if Ekind (Prot_Item) = E_Entry
+                     if Ekind (Prot_Item) in Entry_Kind
                        and then Corresponding_Body (Parent (Prot_Item)) = E
                      then
                         U := Prot_Item;
@@ -20118,6 +20755,10 @@ package body Sem_Util is
               and then Present (Corresponding_Spec_Of_Stub (P))
             then
                U := Corresponding_Spec_Of_Stub (P);
+
+               if Is_Single_Protected_Object (U) then
+                  U := Etype (U);
+               end if;
             end if;
 
          when E_Subprogram_Body =>
@@ -20138,6 +20779,9 @@ package body Sem_Util is
               and then Present (Corresponding_Spec_Of_Stub (P))
             then
                U := Corresponding_Spec_Of_Stub (P);
+
+            elsif Nkind (P) = N_Subprogram_Renaming_Declaration then
+               U := Corresponding_Spec (P);
             end if;
 
          when E_Task_Body =>
@@ -20152,6 +20796,10 @@ package body Sem_Util is
               and then Present (Corresponding_Spec_Of_Stub (P))
             then
                U := Corresponding_Spec_Of_Stub (P);
+
+               if Is_Single_Task_Object (U) then
+                  U := Etype (U);
+               end if;
             end if;
 
          when Type_Kind =>
@@ -20909,4 +21557,28 @@ package body Sem_Util is
       end if;
    end Yields_Synchronized_Object;
 
+   ---------------------------
+   -- Yields_Universal_Type --
+   ---------------------------
+
+   function Yields_Universal_Type (N : Node_Id) return Boolean is
+   begin
+      --  Integer and real literals are of a universal type
+
+      if Nkind_In (N, N_Integer_Literal, N_Real_Literal) then
+         return True;
+
+      --  The values of certain attributes are of a universal type
+
+      elsif Nkind (N) = N_Attribute_Reference then
+         return
+           Universal_Type_Attribute (Get_Attribute_Id (Attribute_Name (N)));
+
+      --  ??? There are possibly other cases to consider
+
+      else
+         return False;
+      end if;
+   end Yields_Universal_Type;
+
 end Sem_Util;
This page took 0.137529 seconds and 5 git commands to generate.