diff gcc/ada/exp_util.adb @ 145:1830386684a0

gcc-9.2.0
author anatofuz
date Thu, 13 Feb 2020 11:34:05 +0900
parents 84e7813d76e9
children
line wrap: on
line diff
--- a/gcc/ada/exp_util.adb	Thu Oct 25 07:37:49 2018 +0900
+++ b/gcc/ada/exp_util.adb	Thu Feb 13 11:34:05 2020 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2018, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2019, 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- --
@@ -32,6 +32,7 @@
 with Elists;   use Elists;
 with Errout;   use Errout;
 with Exp_Aggr; use Exp_Aggr;
+with Exp_Ch2;  use Exp_Ch2;
 with Exp_Ch6;  use Exp_Ch6;
 with Exp_Ch7;  use Exp_Ch7;
 with Exp_Ch11; use Exp_Ch11;
@@ -343,7 +344,7 @@
             return;
          end if;
 
-         --  Case of zero/non-zero semantics or non-standard enumeration
+         --  Case of zero/nonzero semantics or nonstandard enumeration
          --  representation. In each case, we rewrite the node as:
 
          --      ityp!(N) /= False'Enum_Rep
@@ -472,6 +473,169 @@
       end if;
    end Append_Freeze_Actions;
 
+   --------------------------------------
+   -- Attr_Constrained_Statically_True --
+   --------------------------------------
+
+   function Attribute_Constrained_Static_Value (Pref : Node_Id) return Boolean
+   is
+      Ptyp       : constant Entity_Id := Etype (Pref);
+      Formal_Ent : constant Entity_Id := Param_Entity (Pref);
+
+      function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean;
+      --  Ada 2005 (AI-363): Returns True if the object name Obj denotes a
+      --  view of an aliased object whose subtype is constrained.
+
+      ---------------------------------
+      -- Is_Constrained_Aliased_View --
+      ---------------------------------
+
+      function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean is
+         E : Entity_Id;
+
+      begin
+         if Is_Entity_Name (Obj) then
+            E := Entity (Obj);
+
+            if Present (Renamed_Object (E)) then
+               return Is_Constrained_Aliased_View (Renamed_Object (E));
+            else
+               return Is_Aliased (E) and then Is_Constrained (Etype (E));
+            end if;
+
+         else
+            return Is_Aliased_View (Obj)
+              and then
+                (Is_Constrained (Etype (Obj))
+                 or else
+                   (Nkind (Obj) = N_Explicit_Dereference
+                    and then
+                      not Object_Type_Has_Constrained_Partial_View
+                        (Typ  => Base_Type (Etype (Obj)),
+                         Scop => Current_Scope)));
+         end if;
+      end Is_Constrained_Aliased_View;
+
+   --  Start of processing for Attribute_Constrained_Static_Value
+
+   begin
+      --  We are in a case where the attribute is known statically, and
+      --  implicit dereferences have been rewritten.
+
+      pragma Assert
+        (not (Present (Formal_Ent)
+              and then Ekind (Formal_Ent) /= E_Constant
+              and then Present (Extra_Constrained (Formal_Ent)))
+         and then
+           not (Is_Access_Type (Etype (Pref))
+                and then (not Is_Entity_Name (Pref)
+                          or else Is_Object (Entity (Pref))))
+         and then
+           not (Nkind (Pref) = N_Identifier
+                and then Ekind (Entity (Pref)) = E_Variable
+                and then Present (Extra_Constrained (Entity (Pref)))));
+
+      if Is_Entity_Name (Pref) then
+         declare
+            Ent : constant Entity_Id   := Entity (Pref);
+            Res : Boolean;
+
+         begin
+            --  (RM J.4) obsolescent cases
+
+            if Is_Type (Ent) then
+
+               --  Private type
+
+               if Is_Private_Type (Ent) then
+                  Res := not Has_Discriminants (Ent)
+                    or else Is_Constrained (Ent);
+
+               --  It not a private type, must be a generic actual type
+               --  that corresponded to a private type. We know that this
+               --  correspondence holds, since otherwise the reference
+               --  within the generic template would have been illegal.
+
+               else
+                  if Is_Composite_Type (Underlying_Type (Ent)) then
+                     Res := Is_Constrained (Ent);
+                  else
+                     Res := True;
+                  end if;
+               end if;
+
+            else
+
+               --  If the prefix is not a variable or is aliased, then
+               --  definitely true; if it's a formal parameter without an
+               --  associated extra formal, then treat it as constrained.
+
+               --  Ada 2005 (AI-363): An aliased prefix must be known to be
+               --  constrained in order to set the attribute to True.
+
+               if not Is_Variable (Pref)
+                 or else Present (Formal_Ent)
+                 or else (Ada_Version < Ada_2005
+                          and then Is_Aliased_View (Pref))
+                 or else (Ada_Version >= Ada_2005
+                          and then Is_Constrained_Aliased_View (Pref))
+               then
+                  Res := True;
+
+               --  Variable case, look at type to see if it is constrained.
+               --  Note that the one case where this is not accurate (the
+               --  procedure formal case), has been handled above.
+
+               --  We use the Underlying_Type here (and below) in case the
+               --  type is private without discriminants, but the full type
+               --  has discriminants. This case is illegal, but we generate
+               --  it internally for passing to the Extra_Constrained
+               --  parameter.
+
+               else
+                  --  In Ada 2012, test for case of a limited tagged type,
+                  --  in which case the attribute is always required to
+                  --  return True. The underlying type is tested, to make
+                  --  sure we also return True for cases where there is an
+                  --  unconstrained object with an untagged limited partial
+                  --  view which has defaulted discriminants (such objects
+                  --  always produce a False in earlier versions of
+                  --  Ada). (Ada 2012: AI05-0214)
+
+                  Res :=
+                    Is_Constrained (Underlying_Type (Etype (Ent)))
+                    or else
+                      (Ada_Version >= Ada_2012
+                       and then Is_Tagged_Type (Underlying_Type (Ptyp))
+                       and then Is_Limited_Type (Ptyp));
+               end if;
+            end if;
+
+            return Res;
+         end;
+
+      --  Prefix is not an entity name. These are also cases where we can
+      --  always tell at compile time by looking at the form and type of the
+      --  prefix. If an explicit dereference of an object with constrained
+      --  partial view, this is unconstrained (Ada 2005: AI95-0363). If the
+      --  underlying type is a limited tagged type, then Constrained is
+      --  required to always return True (Ada 2012: AI05-0214).
+
+      else
+         return not Is_Variable (Pref)
+           or else
+             (Nkind (Pref) = N_Explicit_Dereference
+              and then
+                not Object_Type_Has_Constrained_Partial_View
+                  (Typ  => Base_Type (Ptyp),
+                   Scop => Current_Scope))
+           or else Is_Constrained (Underlying_Type (Ptyp))
+           or else (Ada_Version >= Ada_2012
+                    and then Is_Tagged_Type (Underlying_Type (Ptyp))
+                    and then Is_Limited_Type (Ptyp));
+      end if;
+   end Attribute_Constrained_Static_Value;
+
    ------------------------------------
    -- Build_Allocate_Deallocate_Proc --
    ------------------------------------
@@ -1933,7 +2097,7 @@
       --  is subject to Source Coverage Obligations.
 
       if Generate_SCO then
-         Set_Needs_Debug_Info (Proc_Id);
+         Set_Debug_Info_Needed (Proc_Id);
       end if;
 
       --  Obtain all views of the input type
@@ -1977,6 +2141,7 @@
       Set_Scope (Obj_Id, Proc_Id);
 
       Set_First_Entity (Proc_Id, Obj_Id);
+      Set_Last_Entity  (Proc_Id, Obj_Id);
 
       --  Generate:
       --    procedure <Work_Typ>DIC (_object : <Work_Typ>);
@@ -3407,7 +3572,7 @@
       --  subject to Source Coverage Obligations.
 
       if Generate_SCO then
-         Set_Needs_Debug_Info (Proc_Id);
+         Set_Debug_Info_Needed (Proc_Id);
       end if;
 
       --  Obtain all views of the input type
@@ -4444,8 +4609,8 @@
 
    begin
       --  If no component clause, then everything is fine, since the back end
-      --  never bit-misaligns by default, even if there is a pragma Packed for
-      --  the record.
+      --  never misaligns from byte boundaries by default, even if there is a
+      --  pragma Pack for the record.
 
       if No (Comp) or else No (Component_Clause (Comp)) then
          return False;
@@ -4492,7 +4657,7 @@
    begin
       --  E is the package or generic package which is externally axiomatized
 
-      if Ekind_In (E, E_Generic_Package, E_Package)
+      if Is_Package_Or_Generic_Package (E)
         and then Has_Annotate_Pragma_For_External_Axiomatization (E)
       then
          return E;
@@ -4608,7 +4773,7 @@
    begin
       pragma Assert (Is_Concurrent_Type (Typ));
 
-      if Ekind (Typ) in Protected_Kind then
+      if Is_Protected_Type (Typ) then
          if Has_Entries (Typ)
 
             --  A protected type without entries that covers an interface and
@@ -4940,18 +5105,6 @@
       end if;
    end Evolve_Or_Else;
 
-   -----------------------------------
-   -- Exceptions_In_Finalization_OK --
-   -----------------------------------
-
-   function Exceptions_In_Finalization_OK return Boolean is
-   begin
-      return
-        not (Restriction_Active (No_Exception_Handlers)    or else
-             Restriction_Active (No_Exception_Propagation) or else
-             Restriction_Active (No_Exceptions));
-   end Exceptions_In_Finalization_OK;
-
    -----------------------------------------
    -- Expand_Static_Predicates_In_Choices --
    -----------------------------------------
@@ -5079,9 +5232,13 @@
       --  may be constants that depend on the bounds of a string literal, both
       --  standard string types and more generally arrays of characters.
 
-      --  In GNATprove mode, these extra subtypes are not needed
-
-      if GNATprove_Mode then
+      --  In GNATprove mode, these extra subtypes are not needed, unless Exp is
+      --  a static expression. In that case, the subtype will be constrained
+      --  while the original type might be unconstrained, so expanding the type
+      --  is necessary both for passing legality checks in GNAT and for precise
+      --  analysis in GNATprove.
+
+      if GNATprove_Mode and then not Is_Static_Expression (Exp) then
          return;
       end if;
 
@@ -5106,7 +5263,7 @@
 
             --  This subtype indication may be used later for constraint checks
             --  we better make sure that if a variable was used as a bound of
-            --  of the original slice, its value is frozen.
+            --  the original slice, its value is frozen.
 
             Evaluate_Slice_Bounds (Exp);
          end;
@@ -5354,6 +5511,7 @@
    ----------------------
 
    function Finalize_Address (Typ : Entity_Id) return Entity_Id is
+      Btyp : constant Entity_Id := Base_Type (Typ);
       Utyp : Entity_Id := Typ;
 
    begin
@@ -5393,12 +5551,12 @@
       --  records do not automatically inherit operations, but maybe they
       --  should???)
 
-      if Is_Untagged_Derivation (Typ) then
-         if Is_Protected_Type (Typ) then
-            Utyp := Corresponding_Record_Type (Root_Type (Base_Type (Typ)));
+      if Is_Untagged_Derivation (Btyp) then
+         if Is_Protected_Type (Btyp) then
+            Utyp := Corresponding_Record_Type (Root_Type (Btyp));
 
          else
-            Utyp := Underlying_Type (Root_Type (Base_Type (Typ)));
+            Utyp := Underlying_Type (Root_Type (Btyp));
 
             if Is_Protected_Type (Utyp) then
                Utyp := Corresponding_Record_Type (Utyp);
@@ -5626,7 +5784,7 @@
          --  We can retrieve primitive operations by name if it is an internal
          --  name. For equality we must check that both of its operands have
          --  the same type, to avoid confusion with user-defined equalities
-         --  than may have a non-symmetric signature.
+         --  than may have a asymmetric signature.
 
          exit when Chars (Op) = Name
            and then
@@ -6637,13 +6795,11 @@
    -- Homonym_Number --
    --------------------
 
-   function Homonym_Number (Subp : Entity_Id) return Nat is
-      Count : Nat;
-      Hom   : Entity_Id;
-
-   begin
-      Count := 1;
-      Hom := Homonym (Subp);
+   function Homonym_Number (Subp : Entity_Id) return Pos is
+      Hom   : Entity_Id := Homonym (Subp);
+      Count : Pos := 1;
+
+   begin
       while Present (Hom) loop
          if Scope (Hom) = Scope (Subp) then
             Count := Count + 1;
@@ -6702,20 +6858,34 @@
    -- Insert_Action --
    -------------------
 
-   procedure Insert_Action (Assoc_Node : Node_Id; Ins_Action : Node_Id) is
+   procedure Insert_Action
+     (Assoc_Node   : Node_Id;
+      Ins_Action   : Node_Id;
+      Spec_Expr_OK : Boolean := False)
+   is
    begin
       if Present (Ins_Action) then
-         Insert_Actions (Assoc_Node, New_List (Ins_Action));
+         Insert_Actions
+           (Assoc_Node   => Assoc_Node,
+            Ins_Actions  => New_List (Ins_Action),
+            Spec_Expr_OK => Spec_Expr_OK);
       end if;
    end Insert_Action;
 
    --  Version with check(s) suppressed
 
    procedure Insert_Action
-     (Assoc_Node : Node_Id; Ins_Action : Node_Id; Suppress : Check_Id)
+     (Assoc_Node   : Node_Id;
+      Ins_Action   : Node_Id;
+      Suppress     : Check_Id;
+      Spec_Expr_OK : Boolean := False)
    is
    begin
-      Insert_Actions (Assoc_Node, New_List (Ins_Action), Suppress);
+      Insert_Actions
+        (Assoc_Node   => Assoc_Node,
+         Ins_Actions  => New_List (Ins_Action),
+         Suppress     => Suppress,
+         Spec_Expr_OK => Spec_Expr_OK);
    end Insert_Action;
 
    -------------------------
@@ -6734,7 +6904,11 @@
    -- Insert_Actions --
    --------------------
 
-   procedure Insert_Actions (Assoc_Node : Node_Id; Ins_Actions : List_Id) is
+   procedure Insert_Actions
+     (Assoc_Node   : Node_Id;
+      Ins_Actions  : List_Id;
+      Spec_Expr_OK : Boolean := False)
+   is
       N : Node_Id;
       P : Node_Id;
 
@@ -6745,14 +6919,20 @@
          return;
       end if;
 
+      --  Insert the action when the context is "Handling of Default and Per-
+      --  Object Expressions" only when requested by the caller.
+
+      if Spec_Expr_OK then
+         null;
+
       --  Ignore insert of actions from inside default expression (or other
       --  similar "spec expression") in the special spec-expression analyze
       --  mode. Any insertions at this point have no relevance, since we are
       --  only doing the analyze to freeze the types of any static expressions.
-      --  See section "Handling of Default Expressions" in the spec of package
-      --  Sem for further details.
-
-      if In_Spec_Expression then
+      --  See section "Handling of Default and Per-Object Expressions" in the
+      --  spec of package Sem for further details.
+
+      elsif In_Spec_Expression then
          return;
       end if;
 
@@ -6806,8 +6986,8 @@
          N := Assoc_Node;
          P := Parent (Assoc_Node);
 
-      --  Non-subexpression case. Note that N is initially Empty in this case
-      --  (N is only guaranteed Non-Empty in the subexpr case).
+      --  Nonsubexpression case. Note that N is initially Empty in this case
+      --  (N is only guaranteed non-Empty in the subexpr case).
 
       else
          N := Empty;
@@ -7062,7 +7242,6 @@
                | N_Procedure_Instantiation
                | N_Protected_Body
                | N_Protected_Body_Stub
-               | N_Protected_Type_Declaration
                | N_Single_Task_Declaration
                | N_Subprogram_Body
                | N_Subprogram_Body_Stub
@@ -7071,7 +7250,6 @@
                | N_Subtype_Declaration
                | N_Task_Body
                | N_Task_Body_Stub
-               | N_Task_Type_Declaration
 
                --  Use clauses can appear in lists of declarations
 
@@ -7135,6 +7313,21 @@
                   return;
                end if;
 
+            --  the expansion of Task and protected type declarations can
+            --  create declarations for temporaries which, like other actions
+            --  are inserted and analyzed before the current declaraation.
+            --  However, the current scope is the synchronized type, and
+            --  for unnesting it is critical that the proper scope for these
+            --  generated entities be the enclosing one.
+
+            when N_Task_Type_Declaration
+               | N_Protected_Type_Declaration =>
+
+               Push_Scope (Scope (Current_Scope));
+               Insert_List_Before_And_Analyze (P, Ins_Actions);
+               Pop_Scope;
+               return;
+
             --  A special case, N_Raise_xxx_Error can act either as a statement
             --  or a subexpression. We tell the difference by looking at the
             --  Etype. It is set to Standard_Void_Type in the statement case.
@@ -7416,9 +7609,10 @@
    --  Version with check(s) suppressed
 
    procedure Insert_Actions
-     (Assoc_Node  : Node_Id;
-      Ins_Actions : List_Id;
-      Suppress    : Check_Id)
+     (Assoc_Node   : Node_Id;
+      Ins_Actions  : List_Id;
+      Suppress     : Check_Id;
+      Spec_Expr_OK : Boolean := False)
    is
    begin
       if Suppress = All_Checks then
@@ -7426,7 +7620,7 @@
             Sva : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
             Scope_Suppress.Suppress := (others => True);
-            Insert_Actions (Assoc_Node, Ins_Actions);
+            Insert_Actions (Assoc_Node, Ins_Actions, Spec_Expr_OK);
             Scope_Suppress.Suppress := Sva;
          end;
 
@@ -7435,7 +7629,7 @@
             Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
          begin
             Scope_Suppress.Suppress (Suppress) := True;
-            Insert_Actions (Assoc_Node, Ins_Actions);
+            Insert_Actions (Assoc_Node, Ins_Actions, Spec_Expr_OK);
             Scope_Suppress.Suppress (Suppress) := Svg;
          end;
       end if;
@@ -8220,8 +8414,8 @@
          return False;
       end if;
 
-      --  Here we have a tagged type, see if it has any unlayed out fields
-      --  other than a possible tag and parent fields. If so, we return False.
+      --  Here we have a tagged type, see if it has any component (other than
+      --  tag and parent) with no component_clause. If so, we return False.
 
       Comp := First_Component (U);
       while Present (Comp) loop
@@ -8235,7 +8429,7 @@
          end if;
       end loop;
 
-      --  All components are layed out
+      --  All components have clauses
 
       return True;
    end Is_Fully_Repped_Tagged_Type;
@@ -8315,7 +8509,7 @@
             S : Nat;
 
          begin
-            --  If component reference is for an array with non-static bounds,
+            --  If component reference is for an array with nonstatic bounds,
             --  then it is always aligned: we can only process unaligned arrays
             --  with static bounds (more precisely compile time known bounds).
 
@@ -8455,12 +8649,6 @@
          return False;
       end if;
 
-      --  We only need to worry if the target has strict alignment
-
-      if not Target_Strict_Alignment then
-         return False;
-      end if;
-
       --  If it is a slice, then look at the array type being sliced
 
       declare
@@ -8504,9 +8692,11 @@
                --  We are definitely in trouble if the record in question
                --  has an alignment, and either we know this alignment is
                --  inconsistent with the alignment of the slice, or we don't
-               --  know what the alignment of the slice should be.
-
-               if Known_Alignment (Ptyp)
+               --  know what the alignment of the slice should be. But this
+               --  really matters only if the target has strict alignment.
+
+               if Target_Strict_Alignment
+                 and then Known_Alignment (Ptyp)
                  and then (Unknown_Alignment (Styp)
                             or else Alignment (Styp) > Alignment (Ptyp))
                then
@@ -9037,7 +9227,7 @@
       then
          Constr_Root := Root_Typ;
 
-         --  At this point in the expansion, non-limited view of the type
+         --  At this point in the expansion, nonlimited view of the type
          --  must be available, otherwise the error will be reported later.
 
          if From_Limited_With (Constr_Root)
@@ -9198,10 +9388,16 @@
       Proc_Id := Invariant_Procedure (Typ);
       pragma Assert (Present (Proc_Id));
 
-      return
-        Make_Procedure_Call_Statement (Loc,
-          Name                   => New_Occurrence_Of (Proc_Id, Loc),
-          Parameter_Associations => New_List (Relocate_Node (Expr)));
+      --  Ignore the invariant if that policy is in effect
+
+      if Invariants_Ignored (Typ) then
+         return Make_Null_Statement (Loc);
+      else
+         return
+           Make_Procedure_Call_Statement (Loc,
+             Name                   => New_Occurrence_Of (Proc_Id, Loc),
+             Parameter_Associations => New_List (Relocate_Node (Expr)));
+      end if;
    end Make_Invariant_Call;
 
    ------------------------
@@ -9313,9 +9509,9 @@
 
       --  If the type is tagged, the expression may be class-wide, in which
       --  case it has to be converted to its root type, given that the
-      --  generated predicate function is not dispatching. The conversion
-      --  is type-safe and does not need validation, which matters when
-      --  private extensions are involved.
+      --  generated predicate function is not dispatching. The conversion is
+      --  type-safe and does not need validation, which matters when private
+      --  extensions are involved.
 
       if Is_Tagged_Type (Typ) then
          Call :=
@@ -9522,7 +9718,7 @@
       end if;
 
       --  Do not generate a check within an internal subprogram (stream
-      --  functions and the like, including including predicate functions).
+      --  functions and the like, including predicate functions).
 
       if Within_Internal_Subprogram then
          return Make_Null_Statement (Loc);
@@ -9810,7 +10006,7 @@
       --  in the derivation chain starting from parent type Par_Typ leading to
       --  derived type Deriv_Typ. The returned value is one of the following:
       --
-      --    * An entity which is either a discriminant or a non-discriminant
+      --    * An entity which is either a discriminant or a nondiscriminant
       --      name, and renames/constraints Discr.
       --
       --    * An expression which constraints Discr
@@ -10524,94 +10720,6 @@
       end if;
    end Needs_Constant_Address;
 
-   ------------------------
-   -- Needs_Finalization --
-   ------------------------
-
-   function Needs_Finalization (Typ : Entity_Id) return Boolean is
-      function Has_Some_Controlled_Component
-        (Input_Typ : Entity_Id) return Boolean;
-      --  Determine whether type Input_Typ has at least one controlled
-      --  component.
-
-      -----------------------------------
-      -- Has_Some_Controlled_Component --
-      -----------------------------------
-
-      function Has_Some_Controlled_Component
-        (Input_Typ : Entity_Id) return Boolean
-      is
-         Comp : Entity_Id;
-
-      begin
-         --  When a type is already frozen and has at least one controlled
-         --  component, or is manually decorated, it is sufficient to inspect
-         --  flag Has_Controlled_Component.
-
-         if Has_Controlled_Component (Input_Typ) then
-            return True;
-
-         --  Otherwise inspect the internals of the type
-
-         elsif not Is_Frozen (Input_Typ) then
-            if Is_Array_Type (Input_Typ) then
-               return Needs_Finalization (Component_Type (Input_Typ));
-
-            elsif Is_Record_Type (Input_Typ) then
-               Comp := First_Component (Input_Typ);
-               while Present (Comp) loop
-                  if Needs_Finalization (Etype (Comp)) then
-                     return True;
-                  end if;
-
-                  Next_Component (Comp);
-               end loop;
-            end if;
-         end if;
-
-         return False;
-      end Has_Some_Controlled_Component;
-
-   --  Start of processing for Needs_Finalization
-
-   begin
-      --  Certain run-time configurations and targets do not provide support
-      --  for controlled types.
-
-      if Restriction_Active (No_Finalization) then
-         return False;
-
-      --  C++ types are not considered controlled. It is assumed that the non-
-      --  Ada side will handle their clean up.
-
-      elsif Convention (Typ) = Convention_CPP then
-         return False;
-
-      --  Class-wide types are treated as controlled because derivations from
-      --  the root type may introduce controlled components.
-
-      elsif Is_Class_Wide_Type (Typ) then
-         return True;
-
-      --  Concurrent types are controlled as long as their corresponding record
-      --  is controlled.
-
-      elsif Is_Concurrent_Type (Typ)
-        and then Present (Corresponding_Record_Type (Typ))
-        and then Needs_Finalization (Corresponding_Record_Type (Typ))
-      then
-         return True;
-
-      --  Otherwise the type is controlled when it is either derived from type
-      --  [Limited_]Controlled and not subject to aspect Disable_Controlled, or
-      --  contains at least one controlled component.
-
-      else
-         return
-           Is_Controlled (Typ) or else Has_Some_Controlled_Component (Typ);
-      end if;
-   end Needs_Finalization;
-
    ----------------------------
    -- New_Class_Wide_Subtype --
    ----------------------------
@@ -10771,9 +10879,9 @@
                Ptyp : constant Entity_Id := Etype (P);
 
             begin
-               --  If we know the component size and it is less than 64, then
-               --  we are definitely OK. The back end always does assignment of
-               --  misaligned small objects correctly.
+               --  If we know the component size and it is not larger than 64,
+               --  then we are definitely OK. The back end does the assignment
+               --  of misaligned small objects correctly.
 
                if Known_Static_Component_Size (Ptyp)
                  and then Component_Size (Ptyp) <= 64
@@ -10796,13 +10904,15 @@
                Comp : constant Entity_Id := Entity (Selector_Name (N));
 
             begin
-               --  If there is no component clause, then we are in the clear
-               --  since the back end will never misalign a large component
-               --  unless it is forced to do so. In the clear means we need
-               --  only the recursive test on the prefix.
+               --  This is the crucial test: if the component itself causes
+               --  trouble, then we can stop and return True.
 
                if Component_May_Be_Bit_Aligned (Comp) then
                   return True;
+
+               --  Otherwise, we need to test the prefix, to see if we are
+               --  selecting from a possibly unaligned component.
+
                else
                   return Possible_Bit_Aligned_Component (P);
                end if;
@@ -10815,7 +10925,7 @@
             return Possible_Bit_Aligned_Component (Prefix (N));
 
          --  For an unchecked conversion, check whether the expression may
-         --  be bit-aligned.
+         --  be bit aligned.
 
          when N_Unchecked_Type_Conversion =>
             return Possible_Bit_Aligned_Component (Expression (N));
@@ -11303,7 +11413,17 @@
          --  Generate:
          --    Rnn : Exp_Type renames Expr;
 
-         if Renaming_Req then
+         --  In GNATprove mode, we prefer to use renamings for intermediate
+         --  variables to definition of constants, due to the implicit move
+         --  operation that such a constant definition causes as part of the
+         --  support in GNATprove for ownership pointers. Hence, we generate
+         --  a renaming for a reference to an object of a nonscalar type.
+
+         if Renaming_Req
+           or else (GNATprove_Mode
+                     and then Is_Object_Reference (Exp)
+                     and then not Is_Scalar_Type (Exp_Type))
+         then
             E :=
               Make_Object_Renaming_Declaration (Loc,
                 Defining_Identifier => Def_Id,
@@ -11425,7 +11545,7 @@
 
       --  For expressions that denote names, we can use a renaming scheme.
       --  This is needed for correctness in the case of a volatile object of
-      --  a non-volatile type because the Make_Reference call of the "default"
+      --  a nonvolatile type because the Make_Reference call of the "default"
       --  approach would generate an illegal access value (an access value
       --  cannot designate such an object - see Analyze_Reference).
 
@@ -11447,7 +11567,7 @@
              Name                => Relocate_Node (Exp)));
 
          --  If this is a packed reference, or a selected component with
-         --  a non-standard representation, a reference to the temporary
+         --  a nonstandard representation, a reference to the temporary
          --  will be replaced by a copy of the original expression (see
          --  Exp_Ch2.Expand_Renaming). Otherwise the temporary must be
          --  elaborated by gigi, and is of course not to be replaced in-line
@@ -11661,6 +11781,10 @@
 
       Set_Assignment_OK (Res, Assignment_OK (Exp));
 
+      --  Preserve the Do_Range_Check flag in all copies
+
+      Set_Do_Range_Check (Res, Do_Range_Check (Exp));
+
       --  Finally rewrite the original expression and we are done
 
       Rewrite (Exp, Res);
@@ -12053,7 +12177,7 @@
                          and then Nkind_In (N, N_Package_Body,
                                                N_Package_Specification);
       --  N is at the library level if the top-most context is a package and
-      --  the path taken to reach N does not inlcude non-package constructs.
+      --  the path taken to reach N does not include nonpackage constructs.
 
    begin
       case Nkind (N) is
@@ -12126,9 +12250,7 @@
       Typ     : Entity_Id;
 
    begin
-      if No (L)
-        or else Is_Empty_List (L)
-      then
+      if No (L) or else Is_Empty_List (L) then
          return False;
       end if;
 
@@ -12740,7 +12862,7 @@
 
             --  Mark the assignment statement as elaboration code. This allows
             --  the early call region mechanism (see Sem_Elab) to properly
-            --  ignore such assignments even though they are non-preelaborable
+            --  ignore such assignments even though they are nonpreelaborable
             --  code.
 
             Set_Is_Elaboration_Code (Asn);
@@ -13400,7 +13522,11 @@
    --  required for the case of False .. False, since False xor False = False.
    --  See also Silly_Boolean_Array_Not_Test
 
-   procedure Silly_Boolean_Array_Xor_Test (N : Node_Id; T : Entity_Id) is
+   procedure Silly_Boolean_Array_Xor_Test
+     (N : Node_Id;
+      R : Node_Id;
+      T : Entity_Id)
+   is
       Loc : constant Source_Ptr := Sloc (N);
       CT  : constant Entity_Id  := Component_Type (T);
 
@@ -13421,9 +13547,9 @@
         Make_Raise_Constraint_Error (Loc,
           Condition =>
             Make_And_Then (Loc,
-              Left_Opnd =>
+              Left_Opnd  =>
                 Make_And_Then (Loc,
-                  Left_Opnd =>
+                  Left_Opnd  =>
                     Convert_To (Standard_Boolean,
                       Make_Attribute_Reference (Loc,
                         Prefix         => New_Occurrence_Of (CT, Loc),
@@ -13435,8 +13561,8 @@
                         Prefix         => New_Occurrence_Of (CT, Loc),
                         Attribute_Name => Name_Last))),
 
-              Right_Opnd => Make_Non_Empty_Check (Loc, Right_Opnd (N))),
-          Reason => CE_Range_Check_Failed));
+              Right_Opnd => Make_Non_Empty_Check (Loc, R)),
+          Reason    => CE_Range_Check_Failed));
    end Silly_Boolean_Array_Xor_Test;
 
    --------------------------
@@ -13553,9 +13679,17 @@
          begin
             E := First_Component_Or_Discriminant (Typ);
             while Present (E) loop
-               if Component_May_Be_Bit_Aligned (E)
-                 or else Type_May_Have_Bit_Aligned_Components (Etype (E))
-               then
+               --  This is the crucial test: if the component itself causes
+               --  trouble, then we can stop and return True.
+
+               if Component_May_Be_Bit_Aligned (E) then
+                  return True;
+               end if;
+
+               --  Otherwise, we need to test its type, to see if it may
+               --  itself contain a troublesome component.
+
+               if Type_May_Have_Bit_Aligned_Components (Etype (E)) then
                   return True;
                end if;