2011-08-29 Yannick Moy <moy@adacore.com>

	* exp_ch13.adb (Expand_N_Freeze_Entity): Do nothing in Alfa mode.
	* exp_ch9.adb: Do not expand tasking constructs in Alfa mode.
	* gnat1drv.adb (Adjust_Global_Switches): Suppress the expansion of
	tagged types and dispatching calls in Alfa mode.

2011-08-29  Javier Miranda  <miranda@adacore.com>

	* sem_ch3.adb (Process_Discriminants): Add missing check to ensure that
	we do not report an error on an Empty node.

2011-08-29  Geert Bosch  <bosch@adacore.com>

	* Makefile.rtl (GNATRTL_NONTASKING_OBJECTS): Add a-nllrar.o,
	a-nlrear.o and a-nurear.o.

2011-08-29  Robert Dewar  <dewar@adacore.com>

	* freeze.adb: Minor code reorganization.
	Minor reformatting.
	* sem_util.adb, errout.adb, exp_ch11.adb, a-ngrear.adb, s-gearop.adb,
	sem_ch6.adb: Minor reformatting

2011-08-29  Tristan Gingold  <gingold@adacore.com>

	* s-except.ads, s-except.adb: Provide dummy body.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_warn.adb (Within_Postcondition): Take into account the case of
	an Ensures component in a Test_Case.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@178222 138bc75d-0d04-0410-961f-82ee72b054a4

19 files changed, 275 insertions, 71 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 593ef4abf0d..d2010209ec2 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,36 @@
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch13.adb (Expand_N_Freeze_Entity): Do nothing in Alfa mode.
+	* exp_ch9.adb: Do not expand tasking constructs in Alfa mode.
+	* gnat1drv.adb (Adjust_Global_Switches): Suppress the expansion of
+	tagged types and dispatching calls in Alfa mode.
+
+2011-08-29  Javier Miranda  <miranda@adacore.com>
+
+	* sem_ch3.adb (Process_Discriminants): Add missing check to ensure that
+	we do not report an error on an Empty node.
+
+2011-08-29  Geert Bosch  <bosch@adacore.com>
+
+	* Makefile.rtl (GNATRTL_NONTASKING_OBJECTS): Add a-nllrar.o,
+	a-nlrear.o and a-nurear.o.
+
+2011-08-29  Robert Dewar  <dewar@adacore.com>
+
+	* freeze.adb: Minor code reorganization.
+	Minor reformatting.
+	* sem_util.adb, errout.adb, exp_ch11.adb, a-ngrear.adb, s-gearop.adb,
+	sem_ch6.adb: Minor reformatting
+
+2011-08-29  Tristan Gingold  <gingold@adacore.com>
+
+	* s-except.ads, s-except.adb: Provide dummy body.
+
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* sem_warn.adb (Within_Postcondition): Take into account the case of
+	an Ensures component in a Test_Case.
+
 2011-08-29  Tristan Gingold  <gingold@adacore.com>
 
 	* s-excdeb.ads, s-excdeb.adb: New files, created from s-except.
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index 4b72a20a13e..eac13f7eacd 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -184,6 +184,9 @@ GNATRTL_NONTASKING_OBJS= \
   a-ngcoty$(objext) \
   a-ngelfu$(objext) \
   a-ngrear$(objext) \
+  a-nllrar$(objext) \
+  a-nlrear$(objext) \
+  a-nurear$(objext) \
   a-nlcefu$(objext) \
   a-nlcoty$(objext) \
   a-nlelfu$(objext) \
diff --git a/gcc/ada/a-ngrear.adb b/gcc/ada/a-ngrear.adb
index b21f839588e..8ce8d9a98b0 100644
--- a/gcc/ada/a-ngrear.adb
+++ b/gcc/ada/a-ngrear.adb
@@ -48,24 +48,24 @@ package body Ada.Numerics.Generic_Real_Arrays is
    function Is_Non_Zero (X : Real'Base) return Boolean is (X /= 0.0);
 
    procedure Back_Substitute is new Ops.Back_Substitute
-       (Scalar        => Real'Base,
-        Matrix        => Real_Matrix,
-        Is_Non_Zero   => Is_Non_Zero);
+     (Scalar        => Real'Base,
+      Matrix        => Real_Matrix,
+      Is_Non_Zero   => Is_Non_Zero);
 
    function Diagonal is new Ops.Diagonal
-        (Scalar       => Real'Base,
-         Vector       => Real_Vector,
-         Matrix       => Real_Matrix);
+     (Scalar       => Real'Base,
+      Vector       => Real_Vector,
+      Matrix       => Real_Matrix);
 
    procedure Forward_Eliminate is new Ops.Forward_Eliminate
-       (Scalar        => Real'Base,
-        Matrix        => Real_Matrix,
-        Zero          => 0.0,
-        One           => 1.0);
+    (Scalar        => Real'Base,
+     Matrix        => Real_Matrix,
+     Zero          => 0.0,
+     One           => 1.0);
 
    procedure Swap_Column is new Ops.Swap_Column
-       (Scalar        => Real'Base,
-        Matrix        => Real_Matrix);
+    (Scalar        => Real'Base,
+     Matrix        => Real_Matrix);
 
    procedure Transpose is new  Ops.Transpose
        (Scalar        => Real'Base,
@@ -100,7 +100,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
    --  Sort Values and associated Vectors by decreasing absolute value
 
    procedure Swap (Left, Right : in out Real);
-   --  Exchange Left and Right.
+   --  Exchange Left and Right
 
    function Sqrt (X : Real) return Real;
    --  Sqrt is implemented locally here, in order to avoid dragging in all of
@@ -132,7 +132,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
       if not (X > 0.0) then
          if X = 0.0 then
             return X;
-
          else
             raise Argument_Error;
          end if;
@@ -158,9 +157,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
 
       for J in 1 .. 8 loop
          Next := (Root + X / Root) / 2.0;
-
          exit when Root = Next;
-
          Root := Next;
       end loop;
 
@@ -401,29 +398,29 @@ package body Ada.Numerics.Generic_Real_Arrays is
    ---------
 
    function "+" (Right : Real_Vector) return Real_Vector
-      renames Instantiations."+";
+     renames Instantiations."+";
 
    function "+" (Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."+";
+     renames Instantiations."+";
 
    function "+" (Left, Right : Real_Vector) return Real_Vector
-      renames Instantiations."+";
+     renames Instantiations."+";
 
    function "+" (Left, Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."+";
+     renames Instantiations."+";
 
    ---------
    -- "-" --
    ---------
 
    function "-" (Right : Real_Vector) return Real_Vector
-      renames Instantiations."-";
+     renames Instantiations."-";
 
    function "-" (Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."-";
+     renames Instantiations."-";
 
    function "-" (Left, Right : Real_Vector) return Real_Vector
-      renames Instantiations."-";
+     renames Instantiations."-";
 
    function "-" (Left, Right : Real_Matrix) return Real_Matrix
       renames Instantiations."-";
@@ -435,58 +432,58 @@ package body Ada.Numerics.Generic_Real_Arrays is
    --  Scalar multiplication
 
    function "*" (Left : Real'Base; Right : Real_Vector) return Real_Vector
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left : Real_Vector; Right : Real'Base) return Real_Vector
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left : Real'Base; Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    --  Vector multiplication
 
    function "*" (Left, Right : Real_Vector) return Real'Base
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left, Right : Real_Vector) return Real_Matrix
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left : Real_Vector; Right : Real_Matrix) return Real_Vector
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    function "*" (Left : Real_Matrix; Right : Real_Vector) return Real_Vector
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    --  Matrix Multiplication
 
    function "*" (Left, Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."*";
+     renames Instantiations."*";
 
    ---------
    -- "/" --
    ---------
 
    function "/" (Left : Real_Vector; Right : Real'Base) return Real_Vector
-      renames Instantiations."/";
+     renames Instantiations."/";
 
    function "/" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix
-      renames Instantiations."/";
+     renames Instantiations."/";
 
    -----------
    -- "abs" --
    -----------
 
    function "abs" (Right : Real_Vector) return Real'Base
-      renames Instantiations."abs";
+     renames Instantiations."abs";
 
    function "abs" (Right : Real_Vector) return Real_Vector
-      renames Instantiations."abs";
+     renames Instantiations."abs";
 
    function "abs" (Right : Real_Matrix) return Real_Matrix
-      renames Instantiations."abs";
+     renames Instantiations."abs";
 
    -----------------
    -- Determinant --
@@ -496,10 +493,8 @@ package body Ada.Numerics.Generic_Real_Arrays is
       M : Real_Matrix := A;
       B : Real_Matrix (A'Range (1), 1 .. 0);
       R : Real'Base;
-
    begin
       Forward_Eliminate (M, B, R);
-
       return R;
    end Determinant;
 
@@ -527,7 +522,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
    begin
       Jacobi (A, Values, Vectors, Compute_Vectors => False);
       Sort_Eigensystem (Values, Vectors);
-
       return Values;
    end Eigenvalues;
 
@@ -574,7 +568,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
       --        values of type Real.
 
       Max_Iterations  : constant := 50;
-
       N               : constant Natural := Length (A);
 
       subtype Square_Matrix is Real_Matrix (1 .. N, 1 .. N);
@@ -606,6 +599,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
 
       function Sum_Strict_Upper (M : Square_Matrix) return Real is
          Sum : Real := 0.0;
+
       begin
          for Row in 1 .. N - 1 loop
             for Col in Row + 1 .. N loop
@@ -803,7 +797,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
      (Values  : in out Real_Vector;
       Vectors : in out Real_Matrix)
    is
-
       procedure Swap (Left, Right : Integer);
       --  Swap Values (Left) with Values (Right), and also swap the
       --  corresponding eigenvectors. Note that lowerbounds may differ.
@@ -834,7 +827,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
       R : Real_Matrix (X'Range (2), X'Range (1));
    begin
       Transpose (X, R);
-
       return R;
    end Transpose;
 
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 3f9acbfb98e..39d73027840 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -2833,7 +2833,7 @@ package body Errout is
       elsif Msg = "size for& too small, minimum allowed is ^" then
 
          --  Suppress "size too small" errors in CodePeer mode and ALFA mode,
-         --  since pragma Pack is also ignored in this configuration.
+         --  since pragma Pack is also ignored in these configurations.
 
          if CodePeer_Mode or ALFA_Mode then
             return True;
diff --git a/gcc/ada/exp_ch11.adb b/gcc/ada/exp_ch11.adb
index ceca349d058..5238a1c7c0c 100644
--- a/gcc/ada/exp_ch11.adb
+++ b/gcc/ada/exp_ch11.adb
@@ -1665,7 +1665,6 @@ package body Exp_Ch11 is
       --  does not have a choice parameter specification, then we provide one.
 
       else
-
          --  Bypass expansion to a run-time call when back-end exception
          --  handling is active, unless the target is a VM or CodePeer.
 
diff --git a/gcc/ada/exp_ch13.adb b/gcc/ada/exp_ch13.adb
index a6890d72746..068ba582bb3 100644
--- a/gcc/ada/exp_ch13.adb
+++ b/gcc/ada/exp_ch13.adb
@@ -307,6 +307,13 @@ package body Exp_Ch13 is
       Delete         : Boolean := False;
 
    begin
+      --  In formal verification mode, do not generate useless and confusing
+      --  expansion for freeze nodes.
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If there are delayed aspect specifications, we insert them just
       --  before the freeze node. They are already analyzed so we don't need
       --  to reanalyze them (they were analyzed before the type was frozen),
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 62d316631e0..2dc78e9d98a 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -7440,8 +7440,8 @@ package body Exp_Ch7 is
    ------------------------------------
 
    function Make_Set_Finalize_Address_Call
-     (Loc : Source_Ptr;
-      Typ   : Entity_Id;
+     (Loc     : Source_Ptr;
+      Typ     : Entity_Id;
       Ptr_Typ : Entity_Id) return Node_Id
    is
       Desig_Typ : constant Entity_Id :=
@@ -7502,12 +7502,12 @@ package body Exp_Ch7 is
 
       return
         Make_Procedure_Call_Statement (Loc,
-          Name =>
+          Name                   =>
             New_Reference_To (RTE (RE_Set_Finalize_Address), Loc),
           Parameter_Associations => New_List (
             New_Reference_To (Finalization_Master (Ptr_Typ), Loc),
             Make_Attribute_Reference (Loc,
-              Prefix =>
+              Prefix         =>
                 New_Reference_To (TSS (Utyp, TSS_Finalize_Address), Loc),
               Attribute_Name => Name_Unrestricted_Access)));
    end Make_Set_Finalize_Address_Call;
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 214bb674972..9ec2e441c73 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -5290,6 +5290,12 @@ package body Exp_Ch9 is
       Tasknm : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Aggr := Make_Aggregate (Loc, Component_Associations => New_List);
       Count := 0;
 
@@ -5421,6 +5427,12 @@ package body Exp_Ch9 is
    --  Start of processing for Expand_N_Accept_Statement
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If accept statement is not part of a list, then its parent must be
       --  an accept alternative, and, as described above, we do not do any
       --  expansion for such accept statements at this level.
@@ -5871,6 +5883,12 @@ package body Exp_Ch9 is
       T   : Entity_Id;  --  Additional status flag
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (Trig);
       Process_Statements_For_Controlled_Objects (Abrt);
 
@@ -6820,6 +6838,12 @@ package body Exp_Ch9 is
       S : Entity_Id;  --  Primitive operation slot
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (N);
 
       if Ada_Version >= Ada_2005
@@ -7136,6 +7160,12 @@ package body Exp_Ch9 is
    procedure Expand_N_Delay_Relative_Statement (N : Node_Id) is
       Loc : constant Source_Ptr := Sloc (N);
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Rewrite (N,
         Make_Procedure_Call_Statement (Loc,
           Name => New_Reference_To (RTE (RO_CA_Delay_For), Loc),
@@ -7155,6 +7185,12 @@ package body Exp_Ch9 is
       Typ : Entity_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if Is_RTE (Base_Type (Etype (Expression (N))), RO_CA_Time) then
          Typ := RTE (RO_CA_Delay_Until);
       else
@@ -7175,6 +7211,12 @@ package body Exp_Ch9 is
 
    procedure Expand_N_Entry_Body (N : Node_Id) is
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Associate discriminals with the next protected operation body to be
       --  expanded.
 
@@ -7196,6 +7238,12 @@ package body Exp_Ch9 is
       Index   : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if No_Run_Time_Mode then
          Error_Msg_CRT ("entry call", N);
          return;
@@ -7252,6 +7300,12 @@ package body Exp_Ch9 is
       Acc_Ent    : Entity_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Formal := First_Formal (Entry_Ent);
       Last_Decl := N;
 
@@ -7520,6 +7574,12 @@ package body Exp_Ch9 is
    --  Start of processing for Expand_N_Protected_Body
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if No_Run_Time_Mode then
          Error_Msg_CRT ("protected body", N);
          return;
@@ -7870,6 +7930,12 @@ package body Exp_Ch9 is
    --  Start of processing for Expand_N_Protected_Type_Declaration
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if Present (Corresponding_Record_Type (Prot_Typ)) then
          return;
       else
@@ -9072,6 +9138,12 @@ package body Exp_Ch9 is
    --  Start of processing for Expand_N_Requeue_Statement
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Extract the components of the entry call
 
       Extract_Entry (N, Concval, Ename, Index);
@@ -9658,6 +9730,12 @@ package body Exp_Ch9 is
    --  Start of processing for Expand_N_Selective_Accept
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (N);
 
       --  First insert some declarations before the select. The first is:
@@ -10288,6 +10366,12 @@ package body Exp_Ch9 is
       --  Used to determine the proper location of wrapper body insertions
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Add renaming declarations for discriminals and a declaration for the
       --  entry family index (if applicable).
 
@@ -10493,6 +10577,12 @@ package body Exp_Ch9 is
       Decl_Stack : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If already expanded, nothing to do
 
       if Present (Corresponding_Record_Type (Tasktyp)) then
@@ -11034,6 +11124,12 @@ package body Exp_Ch9 is
       S : Entity_Id;  --  Primitive operation slot
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Under the Ravenscar profile, timed entry calls are excluded. An error
       --  was already reported on spec, so do not attempt to expand the call.
 
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index e4c56948fe6..7fae15526cb 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -2247,13 +2247,12 @@ package body Freeze is
            and then RM_Size (Rec) >= Scalar_Component_Total_RM_Size
 
            --  Never do implicit packing in CodePeer or ALFA modes since
-           --  we don't do any packing in this mode, since this generates
+           --  we don't do any packing in these modes, since this generates
            --  over-complex code that confuses static analysis, and in
            --  general, neither CodePeer not GNATprove care about the
            --  internal representation of objects.
 
-           and then not CodePeer_Mode
-           and then not ALFA_Mode
+           and then not (CodePeer_Mode or ALFA_Mode)
          then
             --  If implicit packing enabled, do it
 
@@ -3067,8 +3066,7 @@ package body Freeze is
                     and then not Is_Limited_Composite (E)
                     and then not Is_Packed (Root_Type (E))
                     and then not Has_Component_Size_Clause (Root_Type (E))
-                    and then not CodePeer_Mode
-                    and then not ALFA_Mode
+                    and then not (CodePeer_Mode or ALFA_Mode)
                   then
                      Get_Index_Bounds (First_Index (E), Lo, Hi);
 
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 6f3e6f1f956..3924190a250 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -455,14 +455,18 @@ procedure Gnat1drv is
 
          Reset_Style_Check_Options;
 
-         --  Suppress compiler warnings, since what we are
-         --  interested in here is what formal verification can find out.
+         --  Suppress compiler warnings, since what we are interested in here
+         --  is what formal verification can find out.
 
          Warning_Mode := Suppress;
 
          --  Suppress the generation of name tables for enumerations
 
          Global_Discard_Names := True;
+
+         --  Suppress the expansion of tagged types and dispatching calls
+
+         Tagged_Type_Expansion := False;
       end if;
    end Adjust_Global_Switches;
 
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 60c4b357817..a0e33d769df 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -596,6 +596,7 @@ package Lib.Xref is
         (CU           : Node_Id;
          Process      : Node_Processing;
          Inside_Stubs : Boolean);
+      --  This procedure is undocumented ???
 
       procedure Traverse_All_Compilation_Units (Process : Node_Processing);
       --  Call Process on all declarations through all compilation units
diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb
index c6e37ee3da9..76a028e66cd 100644
--- a/gcc/ada/prj-conf.adb
+++ b/gcc/ada/prj-conf.adb
@@ -722,7 +722,7 @@ package body Prj.Conf is
          --  Hash table to keep the languages used in the project tree
 
          IDE : constant Package_Id :=
-           Value_Of (Name_Ide, Project.Decl.Packages, Shared);
+                 Value_Of (Name_Ide, Project.Decl.Packages, Shared);
 
          procedure Add_Config_Switches_For_Project
            (Project    : Project_Id;
@@ -744,6 +744,7 @@ package body Prj.Conf is
             Lang          : Name_Id;
             List          : String_List_Id;
             Elem          : String_Element;
+
          begin
             if Might_Have_Sources (Project) then
                Variable :=
@@ -813,6 +814,9 @@ package body Prj.Conf is
 
          procedure For_Every_Imported_Project is new For_Every_Project_Imported
            (State => Integer, Action => Add_Config_Switches_For_Project);
+         --  Document this procedure ???
+
+         --  Local variables
 
          Name     : Name_Id;
          Count    : Natural;
@@ -820,6 +824,8 @@ package body Prj.Conf is
          Variable : Variable_Value;
          Dummy    : Integer := 0;
 
+      --  Start of processing for Get_Config_Switches
+
       begin
          For_Every_Imported_Project
            (By         => Project,
@@ -839,6 +845,7 @@ package body Prj.Conf is
          Count := 1;
          Name  := Language_Htable.Get_First;
          while Name /= No_Name loop
+
             --  Check if IDE'Compiler_Command is declared for the language.
             --  If it is, use its value to invoke gprconfig.
 
diff --git a/gcc/ada/s-except.adb b/gcc/ada/s-except.adb
index 0d3f9d4416e..9e0b27cdd6d 100755
--- a/gcc/ada/s-except.adb
+++ b/gcc/ada/s-except.adb
@@ -29,4 +29,17 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-pragma No_Body;
+--  This package does not require a body, since it is a package renaming. We
+--  provide a dummy file containing a No_Body pragma so that previous versions
+--  of the body (which did exist) will not interfere.
+
+--  pragma No_Body;
+
+--  The above pragma is commented out, since for now we can't use No_Body in
+--  a unit marked as a Compiler_Unit, since this requires GNAT 6.1, and we
+--  do not yet require this for bootstrapping. So instead we use a dummy Taft
+--  amendment type to require the body:
+
+package body System.Exceptions is
+   type Require_Body is new Integer;
+end System.Exceptions;
diff --git a/gcc/ada/s-except.ads b/gcc/ada/s-except.ads
index 8b40b15b56b..f0da1e520d3 100644
--- a/gcc/ada/s-except.ads
+++ b/gcc/ada/s-except.ads
@@ -40,6 +40,21 @@ package System.Exceptions is
    --  Visible copy to allow Ada.Exceptions to know the exception model.
 
 private
+   type Require_Body;
+   --  Dummy Taft-amendment type to make it legal (and required) to provide
+   --  a body for this package.
+   --
+   --  We do this because this unit used to have a body in earlier versions
+   --  of GNAT, and it causes various bootstrap path problems etc if we remove
+   --  a body, since we may pick up old unwanted bodies.
+   --
+   --  Note: we use this standard Ada method of requiring a body rather
+   --  than the cleaner pragma No_Body because System.Exceptions is a compiler
+   --  unit, and older bootstrap compilers do not support pragma No_Body. This
+   --  type can be removed, and s-except.adb can be replaced by a source
+   --  containing just that pragma, when we decide to move to a 2008 compiler
+   --  as the minimal bootstrap compiler version. ???
+
    ZCX_By_Default : constant Boolean := System.ZCX_By_Default;
 
    Foreign_Exception : exception;
diff --git a/gcc/ada/s-gearop.adb b/gcc/ada/s-gearop.adb
index 017392ca6ec..cb07f40902e 100644
--- a/gcc/ada/s-gearop.adb
+++ b/gcc/ada/s-gearop.adb
@@ -101,6 +101,7 @@ package body System.Generic_Array_Operations is
    procedure Back_Substitute (M, N : in out Matrix) is
       pragma Assert (M'First (1) = N'First (1) and then
                      M'Last  (1) = N'Last (1));
+
       Max_Col : Integer := M'Last (2);
 
       procedure Sub_Row
@@ -108,22 +109,27 @@ package body System.Generic_Array_Operations is
          Target : Integer;
          Source : Integer;
          Factor : Scalar);
+      --  Needs comments ???
 
       procedure Sub_Row
         (M      : in out Matrix;
          Target : Integer;
          Source : Integer;
-         Factor : Scalar) is
+         Factor : Scalar)
+      is
       begin
          for J in M'Range (2) loop
             M (Target, J) := M (Target, J) - Factor * M (Source, J);
          end loop;
       end Sub_Row;
 
+   --  Start of processing for Back_Substitute
+
    begin
       for Row in reverse M'Range (1) loop
          Find_Non_Zero : for Col in M'First (2) .. Max_Col loop
             if Is_Non_Zero (M (Row, Col)) then
+
                --  Found first non-zero element, so subtract a multiple
                --  of this row from all higher rows, to reduce all other
                --  elements in this column to zero.
@@ -160,16 +166,19 @@ package body System.Generic_Array_Operations is
          Target : Integer;
          Source : Integer;
          Factor : Scalar);
+      --  Needs commenting ???
 
       procedure Divide_Row
         (M, N  : in out Matrix;
          Row   : Integer;
          Scale : Scalar);
+      --  Needs commenting ???
 
       procedure Switch_Row
         (M, N  : in out Matrix;
          Row_1 : Integer;
          Row_2 : Integer);
+      --  Needs commenting ???
 
       -------------
       -- Sub_Row --
@@ -179,7 +188,8 @@ package body System.Generic_Array_Operations is
         (M      : in out Matrix;
          Target : Integer;
          Source : Integer;
-         Factor : Scalar) is
+         Factor : Scalar)
+         is
       begin
          for J in M'Range (2) loop
             M (Target, J) := M (Target, J) - Factor * M (Source, J);
@@ -227,6 +237,8 @@ package body System.Generic_Array_Operations is
             Y := T;
          end Swap;
 
+      --  Start of processing for Switch_Row
+
       begin
          if Row_1 /= Row_2 then
             Det := Zero - Det;
@@ -242,17 +254,22 @@ package body System.Generic_Array_Operations is
          end if;
       end Switch_Row;
 
-      I   : Integer := M'First (1);
+      I : Integer := M'First (1);
+      --  Avoid use of I ???
+
+   --  Start of processing for Forward_Eliminate
 
-   begin -- Forward_Eliminate
+   begin
       Det := One;
 
       for J in M'Range (2) loop
          declare
             Max_I   : Integer := I;
             Max_Abs : Scalar := Zero;
+
          begin
-            --  Find best pivot in column J, starting in row I.
+            --  Find best pivot in column J, starting in row I
+
             for K in I .. M'Last (1) loop
                declare
                   New_Abs : constant Scalar := abs M (K, J);
@@ -359,6 +376,7 @@ package body System.Generic_Array_Operations is
       return Result_Matrix
    is
       R : Result_Matrix (Left'Range (1), Left'Range (2));
+
    begin
       if Left'Length (1) /= Right'Length (1)
         or else Left'Length (2) /= Right'Length (2)
@@ -557,6 +575,7 @@ package body System.Generic_Array_Operations is
          for K in R'Range (2) loop
             declare
                S : Result_Scalar := Zero;
+
             begin
                for M in Left'Range (2) loop
                   S := S + Left (J, M)
@@ -590,6 +609,7 @@ package body System.Generic_Array_Operations is
       for J in Left'Range (1) loop
          declare
             S : Result_Scalar := Zero;
+
          begin
             for K in Left'Range (2) loop
                S := S + Left (J, K) * Right (K - Left'First (2) + Right'First);
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 2ab8ab1bf4f..34c063d3c97 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -17237,9 +17237,8 @@ package body Sem_Ch3 is
             --  worst, and therefore defaults are not allowed if the parent is
             --  a generic formal private type (see ACATS B370001).
 
-            if Is_Access_Type (Discr_Type) then
+            if Is_Access_Type (Discr_Type) and then Default_Present then
                if Ekind (Discr_Type) /= E_Anonymous_Access_Type
-                 or else not Default_Present
                  or else Is_Limited_Record (Current_Scope)
                  or else Is_Concurrent_Type (Current_Scope)
                  or else Is_Concurrent_Record_Type (Current_Scope)
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index a4b0c3ce05b..afd03c2d51f 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -7052,8 +7052,13 @@ package body Sem_Ch6 is
       function Controlling_Formal (Prim : Entity_Id) return Entity_Id;
       --  Return the controlling formal of Prim
 
+      ------------------------
+      -- Controlling_Formal --
+      ------------------------
+
       function Controlling_Formal (Prim : Entity_Id) return Entity_Id is
          E : Entity_Id := First_Entity (Prim);
+
       begin
          while Present (E) loop
             if Is_Formal (E) and then Is_Controlling_Formal (E) then
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index e6730f20bc7..3072f6a3522 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7953,8 +7953,8 @@ package body Sem_Util is
    --------------------------------------------------
 
    function Is_Subprogram_Stub_Without_Prior_Declaration
-     (N : Node_Id) return Boolean is
-
+     (N : Node_Id) return Boolean
+   is
    begin
       --  A subprogram stub without prior declaration serves as declaration for
       --  the actual subprogram body. As such, it has an attached defining
diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index 044efd872e8..d58a14d7bca 100644
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -1748,14 +1748,15 @@ package body Sem_Warn is
                      SE : constant Entity_Id := Scope (E);
 
                      function Within_Postcondition return Boolean;
-                     --  Returns True iff N is within a Precondition
+                     --  Returns True iff N is within a Postcondition or
+                     --  Ensures component in a Test_Case.
 
                      --------------------------
                      -- Within_Postcondition --
                      --------------------------
 
                      function Within_Postcondition return Boolean is
-                        Nod : Node_Id;
+                        Nod, P : Node_Id;
 
                      begin
                         Nod := Parent (N);
@@ -1764,6 +1765,17 @@ package body Sem_Warn is
                              and then Pragma_Name (Nod) = Name_Postcondition
                            then
                               return True;
+
+                           elsif Present (Parent (Nod)) then
+                              P := Parent (Nod);
+
+                              if Nkind (P) = N_Pragma
+                                and then Pragma_Name (P) = Name_Test_Case
+                                and then
+                                  Nod = Get_Ensures_From_Test_Case_Pragma (P)
+                              then
+                                 return True;
+                              end if;
                            end if;
 
                            Nod := Parent (Nod);
@@ -1893,8 +1905,8 @@ package body Sem_Warn is
                      end if;
 
                      --  One more check, don't bother if we are within a
-                     --  postcondition pragma, since the expression occurs
-                     --  in a place unrelated to the actual test.
+                     --  postcondition, since the expression occurs in a
+                     --  place unrelated to the actual test.
 
                      if not Within_Postcondition then