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

	* exp_ch9.adb, s-tassta.adb, s-secsta.adb: Minor reformatting.

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

	* exp_ch6_light.adb, exp_ch6_light.ads, exp_attr_light.adb,
	exp_attr_light.ads, exp_ch7_light.adb, exp_ch7_light.ads,
	exp_light.adb, exp_light.ads, exp_prag.adb, expander.adb,
	gnat1drv.adb, exp_ch11.adb, exp_ch6.adb, exp_ch6.ads, exp_aggr.adb:
	Revert change which introduced files for "light"
	expansion, to be replaced by a single file for Alfa expansion.



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

19 files changed, 333 insertions, 831 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ce9e88b6559..81574bb4798 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2011-08-30  Robert Dewar  <dewar@adacore.com>
 
+	* exp_ch9.adb, s-tassta.adb, s-secsta.adb: Minor reformatting.
+
+2011-08-30  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch6_light.adb, exp_ch6_light.ads, exp_attr_light.adb,
+	exp_attr_light.ads, exp_ch7_light.adb, exp_ch7_light.ads,
+	exp_light.adb, exp_light.ads, exp_prag.adb, expander.adb,
+	gnat1drv.adb, exp_ch11.adb, exp_ch6.adb, exp_ch6.ads, exp_aggr.adb:
+	Revert change which introduced files for "light"
+	expansion, to be replaced by a single file for Alfa expansion.
+
+2011-08-30  Robert Dewar  <dewar@adacore.com>
+
 	* opt.ads, s-soflin.adb, exp_ch9.adb, sem_res.adb: Update comment.
 	Minor code reorg/reformatting.
 
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index a54ebe8b297..037a8dcc6ea 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4664,6 +4664,12 @@ package body Exp_Aggr is
          Check_Same_Aggr_Bounds (N, 1);
       end if;
 
+      --  In formal verification mode, leave the aggregate non-expanded
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  STEP 2
 
       --  Here we test for is packed array aggregate that we can handle at
diff --git a/gcc/ada/exp_attr_light.adb b/gcc/ada/exp_attr_light.adb
deleted file mode 100644
index 95a22dd7531..00000000000
--- a/gcc/ada/exp_attr_light.adb
+++ /dev/null
@@ -1,50 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                       E X P _ A T T R _ L I G H T                        --
---                                                                          --
---                                 B o d y                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
-with Exp_Attr; use Exp_Attr;
-with Sinfo;    use Sinfo;
-with Snames;   use Snames;
-
-package body Exp_Attr_Light is
-
-   ----------------------------------------
-   -- Expand_Light_N_Attribute_Reference --
-   ----------------------------------------
-
-   procedure Expand_Light_N_Attribute_Reference (N : Node_Id) is
-      Id : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
-
-   begin
-      case Id is
-         when Attribute_Old    |
-              Attribute_Result =>
-            Expand_N_Attribute_Reference (N);
-
-         when others =>
-            null;
-      end case;
-   end Expand_Light_N_Attribute_Reference;
-
-end Exp_Attr_Light;
diff --git a/gcc/ada/exp_attr_light.ads b/gcc/ada/exp_attr_light.ads
deleted file mode 100644
index 3b2bf7df099..00000000000
--- a/gcc/ada/exp_attr_light.ads
+++ /dev/null
@@ -1,35 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                       E X P _ A T T R _ L I G H T                        --
---                                                                          --
---                                 S p e c                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
---  Light expand routines for attribute references
-
-with Types; use Types;
-
-package Exp_Attr_Light is
-
-   procedure Expand_Light_N_Attribute_Reference (N : Node_Id);
-   --  Expand attributes 'Old and 'Result only
-
-end Exp_Attr_Light;
diff --git a/gcc/ada/exp_ch11.adb b/gcc/ada/exp_ch11.adb
index dca021f9237..caf66cca0e0 100644
--- a/gcc/ada/exp_ch11.adb
+++ b/gcc/ada/exp_ch11.adb
@@ -1673,6 +1673,7 @@ package body Exp_Ch11 is
 
          if VM_Target = No_VM
            and then not CodePeer_Mode
+           and then not ALFA_Mode
            and then Exception_Mechanism = Back_End_Exceptions
          then
             return;
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 6780f6e8998..b390db4c1e1 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -156,6 +156,36 @@ package body Exp_Ch6 is
    --  the values are not changed for the call, we know immediately that
    --  we have an infinite recursion.
 
+   procedure Expand_Actuals (N : Node_Id; Subp : Entity_Id);
+   --  For each actual of an in-out or out parameter which is a numeric
+   --  (view) conversion of the form T (A), where A denotes a variable,
+   --  we insert the declaration:
+   --
+   --    Temp : T[ := T (A)];
+   --
+   --  prior to the call. Then we replace the actual with a reference to Temp,
+   --  and append the assignment:
+   --
+   --    A := TypeA (Temp);
+   --
+   --  after the call. Here TypeA is the actual type of variable A. For out
+   --  parameters, the initial declaration has no expression. If A is not an
+   --  entity name, we generate instead:
+   --
+   --    Var  : TypeA renames A;
+   --    Temp : T := Var;       --  omitting expression for out parameter.
+   --    ...
+   --    Var := TypeA (Temp);
+   --
+   --  For other in-out parameters, we emit the required constraint checks
+   --  before and/or after the call.
+   --
+   --  For all parameter modes, actuals that denote components and slices of
+   --  packed arrays are expanded into suitable temporaries.
+   --
+   --  For non-scalar objects that are possibly unaligned, add call by copy
+   --  code (copy in for IN and IN OUT, copy out for OUT and IN OUT).
+
    procedure Expand_Ctrl_Function_Call (N : Node_Id);
    --  N is a function call which returns a controlled object. Transform the
    --  call into a temporary which retrieves the returned object from the
diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads
index 95a10ec9ded..1896ce21069 100644
--- a/gcc/ada/exp_ch6.ads
+++ b/gcc/ada/exp_ch6.ads
@@ -37,36 +37,6 @@ package Exp_Ch6 is
    procedure Expand_N_Subprogram_Body_Stub      (N : Node_Id);
    procedure Expand_N_Subprogram_Declaration    (N : Node_Id);
 
-   procedure Expand_Actuals (N : Node_Id; Subp : Entity_Id);
-   --  For each actual of an in-out or out parameter which is a numeric
-   --  (view) conversion of the form T (A), where A denotes a variable,
-   --  we insert the declaration:
-   --
-   --    Temp : T[ := T (A)];
-   --
-   --  prior to the call. Then we replace the actual with a reference to Temp,
-   --  and append the assignment:
-   --
-   --    A := TypeA (Temp);
-   --
-   --  after the call. Here TypeA is the actual type of variable A. For out
-   --  parameters, the initial declaration has no expression. If A is not an
-   --  entity name, we generate instead:
-   --
-   --    Var  : TypeA renames A;
-   --    Temp : T := Var;       --  omitting expression for out parameter.
-   --    ...
-   --    Var := TypeA (Temp);
-   --
-   --  For other in-out parameters, we emit the required constraint checks
-   --  before and/or after the call.
-   --
-   --  For all parameter modes, actuals that denote components and slices of
-   --  packed arrays are expanded into suitable temporaries.
-   --
-   --  For non-scalar objects that are possibly unaligned, add call by copy
-   --  code (copy in for IN and IN OUT, copy out for OUT and IN OUT).
-
    procedure Expand_Call (N : Node_Id);
    --  This procedure contains common processing for Expand_N_Function_Call,
    --  Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
diff --git a/gcc/ada/exp_ch6_light.adb b/gcc/ada/exp_ch6_light.adb
deleted file mode 100644
index e07057c41f5..00000000000
--- a/gcc/ada/exp_ch6_light.adb
+++ /dev/null
@@ -1,193 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                         E X P _ C H 6 _ L I G H T                        --
---                                                                          --
---                                 B o d y                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
-with Atree;    use Atree;
-with Einfo;    use Einfo;
-with Exp_Ch6;  use Exp_Ch6;
-with Exp_Dbug; use Exp_Dbug;
-with Rtsfind;  use Rtsfind;
-with Sem_Aux;  use Sem_Aux;
-with Sem_Res;  use Sem_Res;
-with Sinfo;    use Sinfo;
-with Stand;    use Stand;
-with Tbuild;   use Tbuild;
-
-package body Exp_Ch6_Light is
-
-   -----------------------
-   -- Local Subprograms --
-   -----------------------
-
-   procedure Expand_Simple_Function_Return (N : Node_Id);
-   --  Expand simple return from function
-
-   -----------------------
-   -- Expand_Light_Call --
-   -----------------------
-
-   procedure Expand_Light_Call (N : Node_Id) is
-      Call_Node   : constant Node_Id := N;
-      Parent_Subp : Entity_Id;
-      Subp        : Entity_Id;
-
-   begin
-      --  Ignore if previous error
-
-      if Nkind (Call_Node) in N_Has_Etype
-        and then Etype (Call_Node) = Any_Type
-      then
-         return;
-      end if;
-
-      --  Call using access to subprogram with explicit dereference
-
-      if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
-         Subp        := Etype (Name (Call_Node));
-         Parent_Subp := Empty;
-
-      --  Case of call to simple entry, where the Name is a selected component
-      --  whose prefix is the task, and whose selector name is the entry name
-
-      elsif Nkind (Name (Call_Node)) = N_Selected_Component then
-         Subp        := Entity (Selector_Name (Name (Call_Node)));
-         Parent_Subp := Empty;
-
-      --  Case of call to member of entry family, where Name is an indexed
-      --  component, with the prefix being a selected component giving the
-      --  task and entry family name, and the index being the entry index.
-
-      elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
-         Subp        := Entity (Selector_Name (Prefix (Name (Call_Node))));
-         Parent_Subp := Empty;
-
-      --  Normal case
-
-      else
-         Subp        := Entity (Name (Call_Node));
-         Parent_Subp := Alias (Subp);
-      end if;
-
-      --  Various expansion activities for actuals are carried out
-
-      Expand_Actuals (N, Subp);
-
-      --  If the subprogram is a renaming, replace it in the call with the name
-      --  of the actual subprogram being called.
-
-      if Present (Parent_Subp) then
-         Parent_Subp := Ultimate_Alias (Parent_Subp);
-
-         --  The below setting of Entity is suspect, see F109-018 discussion???
-
-         Set_Entity (Name (Call_Node), Parent_Subp);
-      end if;
-
-   end Expand_Light_Call;
-
-   --------------------------------------------
-   -- Expand_Light_N_Simple_Return_Statement --
-   --------------------------------------------
-
-   procedure Expand_Light_N_Simple_Return_Statement (N : Node_Id) is
-   begin
-      --  Defend against previous errors (i.e. the return statement calls a
-      --  function that is not available in configurable runtime).
-
-      if Present (Expression (N))
-        and then Nkind (Expression (N)) = N_Empty
-      then
-         return;
-      end if;
-
-      --  Distinguish the function and non-function cases:
-
-      case Ekind (Return_Applies_To (Return_Statement_Entity (N))) is
-
-         when E_Function          |
-              E_Generic_Function  =>
-            Expand_Simple_Function_Return (N);
-
-         when E_Procedure         |
-              E_Generic_Procedure |
-              E_Entry             |
-              E_Entry_Family      |
-              E_Return_Statement =>
-            --  Expand_Non_Function_Return (N);
-            null;
-
-         when others =>
-            raise Program_Error;
-      end case;
-
-   exception
-      when RE_Not_Available =>
-         return;
-   end Expand_Light_N_Simple_Return_Statement;
-
-   ------------------------------------
-   -- Expand_Light_N_Subprogram_Body --
-   ------------------------------------
-
-   procedure Expand_Light_N_Subprogram_Body (N : Node_Id) is
-   begin
-      Qualify_Entity_Names (N);
-   end Expand_Light_N_Subprogram_Body;
-
-   -----------------------------------
-   -- Expand_Simple_Function_Return --
-   -----------------------------------
-
-   procedure Expand_Simple_Function_Return (N : Node_Id) is
-      Scope_Id : constant Entity_Id :=
-                   Return_Applies_To (Return_Statement_Entity (N));
-      --  The function we are returning from
-
-      R_Type : constant Entity_Id := Etype (Scope_Id);
-      --  The result type of the function
-
-      Exp : constant Node_Id := Expression (N);
-      pragma Assert (Present (Exp));
-
-      Exptyp : constant Entity_Id := Etype (Exp);
-      --  The type of the expression (not necessarily the same as R_Type)
-
-   begin
-      --  Check the result expression of a scalar function against the subtype
-      --  of the function by inserting a conversion. This conversion must
-      --  eventually be performed for other classes of types, but for now it's
-      --  only done for scalars.
-      --  ???
-
-      if Is_Scalar_Type (Exptyp) then
-         Rewrite (Exp, Convert_To (R_Type, Exp));
-
-         --  The expression is resolved to ensure that the conversion gets
-         --  expanded to generate a possible constraint check.
-
-         Analyze_And_Resolve (Exp, R_Type);
-      end if;
-   end Expand_Simple_Function_Return;
-
-end Exp_Ch6_Light;
diff --git a/gcc/ada/exp_ch6_light.ads b/gcc/ada/exp_ch6_light.ads
deleted file mode 100644
index 0cdec5cf5a8..00000000000
--- a/gcc/ada/exp_ch6_light.ads
+++ /dev/null
@@ -1,44 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                         E X P _ C H 6 _ L I G H T                        --
---                                                                          --
---                                 S p e c                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
---  Light expand routines for chapter 6 constructs
-
-with Types; use Types;
-
-package Exp_Ch6_Light is
-
-   procedure Expand_Light_Call (N : Node_Id);
-   --  This procedure contains common processing for function and procedure
-   --  calls:
-   --  * expansion of actuals to introduce necessary temporaries
-   --  * replacement of renaming by subprogram renamed
-
-   procedure Expand_Light_N_Simple_Return_Statement (N : Node_Id);
-   --  Insert conversion on function return if necessary
-
-   procedure Expand_Light_N_Subprogram_Body (N : Node_Id);
-   --  Fully qualify names of enclosed entities
-
-end Exp_Ch6_Light;
diff --git a/gcc/ada/exp_ch7_light.adb b/gcc/ada/exp_ch7_light.adb
deleted file mode 100644
index f4e6a871e21..00000000000
--- a/gcc/ada/exp_ch7_light.adb
+++ /dev/null
@@ -1,35 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                         E X P _ C H 7 _ L I G H T                        --
---                                                                          --
---                                 B o d y                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
-with Exp_Dbug; use Exp_Dbug;
-
-package body Exp_Ch7_Light is
-
-   procedure Expand_Light_N_Package_Declaration (N : Node_Id) is
-   begin
-      Qualify_Entity_Names (N);
-   end Expand_Light_N_Package_Declaration;
-
-end Exp_Ch7_Light;
diff --git a/gcc/ada/exp_ch7_light.ads b/gcc/ada/exp_ch7_light.ads
deleted file mode 100644
index 87ab34be101..00000000000
--- a/gcc/ada/exp_ch7_light.ads
+++ /dev/null
@@ -1,35 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                         E X P _ C H 7 _ L I G H T                        --
---                                                                          --
---                                 S p e c                                  --
---                                                                          --
---              Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
---  Light expand routines for chapter 7 constructs
-
-with Types; use Types;
-
-package Exp_Ch7_Light is
-
-   procedure Expand_Light_N_Package_Declaration (N : Node_Id);
-   --  Fully qualify names of enclosed entities
-
-end Exp_Ch7_Light;
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 58d6df00bf6..ae7ed12e45a 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -11130,10 +11130,8 @@ package body Exp_Ch9 is
 
          Prepend_To (Decls,
            Make_Object_Declaration (Loc,
-             Defining_Identifier =>
-               B,
-             Object_Definition =>
-               New_Reference_To (Standard_Boolean, Loc)));
+             Defining_Identifier => B,
+             Object_Definition   => New_Reference_To (Standard_Boolean, Loc)));
       end if;
 
       --  Duration and mode processing
@@ -11149,15 +11147,19 @@ package body Exp_Ch9 is
 
       elsif Is_RTE (D_Type, RO_CA_Time) then
          D_Disc := Make_Integer_Literal (Loc, 1);
-         D_Conv := Make_Function_Call (Loc,
-           New_Reference_To (RTE (RO_CA_To_Duration), Loc),
-           New_List (New_Copy (Expression (D_Stat))));
+         D_Conv :=
+           Make_Function_Call (Loc,
+             Name => New_Reference_To (RTE (RO_CA_To_Duration), Loc),
+             Parameter_Associations =>
+               New_List (New_Copy (Expression (D_Stat))));
 
       else pragma Assert (Is_RTE (D_Type, RO_RT_Time));
          D_Disc := Make_Integer_Literal (Loc, 2);
-         D_Conv := Make_Function_Call (Loc,
-           New_Reference_To (RTE (RO_RT_To_Duration), Loc),
-           New_List (New_Copy (Expression (D_Stat))));
+         D_Conv :=
+           Make_Function_Call (Loc,
+             Name => New_Reference_To (RTE (RO_RT_To_Duration), Loc),
+             Parameter_Associations =>
+               New_List (New_Copy (Expression (D_Stat))));
       end if;
 
       D := Make_Temporary (Loc, 'D');
@@ -11167,10 +11169,8 @@ package body Exp_Ch9 is
 
       Append_To (Decls,
         Make_Object_Declaration (Loc,
-          Defining_Identifier =>
-            D,
-          Object_Definition =>
-            New_Reference_To (Standard_Duration, Loc)));
+          Defining_Identifier => D,
+          Object_Definition   => New_Reference_To (Standard_Duration, Loc)));
 
       M := Make_Temporary (Loc, 'M');
 
@@ -11179,22 +11179,17 @@ package body Exp_Ch9 is
 
       Append_To (Decls,
         Make_Object_Declaration (Loc,
-          Defining_Identifier =>
-            M,
-          Object_Definition =>
-            New_Reference_To (Standard_Integer, Loc),
-          Expression =>
-            D_Disc));
+          Defining_Identifier => M,
+          Object_Definition   => New_Reference_To (Standard_Integer, Loc),
+          Expression          => D_Disc));
 
       --  Do the assignment at this stage only because the evaluation of the
       --  expression must not occur before (see ACVC C97302A).
 
       Append_To (Stmts,
         Make_Assignment_Statement (Loc,
-          Name =>
-            New_Reference_To (D, Loc),
-          Expression =>
-            D_Conv));
+          Name       => New_Reference_To (D, Loc),
+          Expression => D_Conv));
 
       --  Parameter block processing
 
@@ -11211,8 +11206,8 @@ package body Exp_Ch9 is
          K := Build_K (Loc, Decls, Obj);
 
          Blk_Typ := Build_Parameter_Block (Loc, Actuals, Formals, Decls);
-         P := Parameter_Block_Pack
-                (Loc, Blk_Typ, Actuals, Formals, Decls, Stmts);
+         P :=
+           Parameter_Block_Pack (Loc, Blk_Typ, Actuals, Formals, Decls, Stmts);
 
          --  Dispatch table slot processing, generate:
          --    S : Integer;
@@ -11238,9 +11233,10 @@ package body Exp_Ch9 is
 
          Append_To (Params, New_Copy_Tree (Obj));
          Append_To (Params, New_Reference_To (S, Loc));
-         Append_To (Params, Make_Attribute_Reference (Loc,
-                              Prefix => New_Reference_To (P, Loc),
-                              Attribute_Name => Name_Address));
+         Append_To (Params,
+           Make_Attribute_Reference (Loc,
+             Prefix         => New_Reference_To (P, Loc),
+             Attribute_Name => Name_Address));
          Append_To (Params, New_Reference_To (D, Loc));
          Append_To (Params, New_Reference_To (M, Loc));
          Append_To (Params, New_Reference_To (C, Loc));
@@ -11249,12 +11245,10 @@ package body Exp_Ch9 is
          Append_To (Conc_Typ_Stmts,
            Make_Procedure_Call_Statement (Loc,
              Name =>
-               New_Reference_To (
-                 Find_Prim_Op (Etype (Etype (Obj)),
-                   Name_uDisp_Timed_Select),
-                 Loc),
-             Parameter_Associations =>
-               Params));
+               New_Reference_To
+                 (Find_Prim_Op
+                   (Etype (Etype (Obj)), Name_uDisp_Timed_Select), Loc),
+             Parameter_Associations => Params));
 
          --  Generate:
          --    if C = POK_Protected_Entry
@@ -11274,24 +11268,22 @@ package body Exp_Ch9 is
             Append_To (Conc_Typ_Stmts,
               Make_If_Statement (Loc,
 
-                Condition =>
+                Condition       =>
                   Make_Or_Else (Loc,
-                    Left_Opnd =>
+                    Left_Opnd  =>
                       Make_Op_Eq (Loc,
-                        Left_Opnd =>
-                          New_Reference_To (C, Loc),
+                        Left_Opnd => New_Reference_To (C, Loc),
                         Right_Opnd =>
-                          New_Reference_To (RTE (
-                            RE_POK_Protected_Entry), Loc)),
+                          New_Reference_To
+                            (RTE (RE_POK_Protected_Entry), Loc)),
+
                     Right_Opnd =>
                       Make_Op_Eq (Loc,
-                        Left_Opnd =>
-                          New_Reference_To (C, Loc),
+                        Left_Opnd  => New_Reference_To (C, Loc),
                         Right_Opnd =>
                           New_Reference_To (RTE (RE_POK_Task_Entry), Loc))),
 
-                Then_Statements =>
-                  Unpack));
+                Then_Statements => Unpack));
          end if;
 
          --  Generate:
@@ -11317,33 +11309,30 @@ package body Exp_Ch9 is
                Make_Or_Else (Loc,
                  Left_Opnd =>
                    Make_Op_Eq (Loc,
-                     Left_Opnd =>
-                       New_Reference_To (C, Loc),
+                     Left_Opnd  => New_Reference_To (C, Loc),
                      Right_Opnd =>
                        New_Reference_To (RTE (RE_POK_Procedure), Loc)),
+
                  Right_Opnd =>
                    Make_Or_Else (Loc,
                      Left_Opnd =>
                        Make_Op_Eq (Loc,
-                         Left_Opnd =>
-                           New_Reference_To (C, Loc),
+                         Left_Opnd  => New_Reference_To (C, Loc),
                          Right_Opnd =>
                            New_Reference_To (RTE (
                              RE_POK_Protected_Procedure), Loc)),
                      Right_Opnd =>
                        Make_Op_Eq (Loc,
-                         Left_Opnd =>
-                           New_Reference_To (C, Loc),
+                         Left_Opnd  => New_Reference_To (C, Loc),
                          Right_Opnd =>
-                           New_Reference_To (RTE (
-                             RE_POK_Task_Procedure), Loc)))),
+                           New_Reference_To
+                             (RTE (RE_POK_Task_Procedure), Loc)))),
 
-             Then_Statements =>
-               New_List (E_Call)));
+             Then_Statements => New_List (E_Call)));
 
          Append_To (Conc_Typ_Stmts,
            Make_If_Statement (Loc,
-             Condition => New_Reference_To (B, Loc),
+             Condition       => New_Reference_To (B, Loc),
              Then_Statements => N_Stats,
              Else_Statements => D_Stats));
 
@@ -11363,18 +11352,13 @@ package body Exp_Ch9 is
 
          Append_To (Stmts,
            Make_If_Statement (Loc,
-             Condition =>
+             Condition       =>
                Make_Op_Eq (Loc,
-                 Left_Opnd =>
-                   New_Reference_To (K, Loc),
+                 Left_Opnd  => New_Reference_To (K, Loc),
                  Right_Opnd =>
                    New_Reference_To (RTE (RE_TK_Limited_Tagged), Loc)),
-
-             Then_Statements =>
-               Lim_Typ_Stmts,
-
-             Else_Statements =>
-               Conc_Typ_Stmts));
+             Then_Statements => Lim_Typ_Stmts,
+             Else_Statements => Conc_Typ_Stmts));
 
       else
          --  Skip assignments to temporaries created for in-out parameters.
@@ -11391,7 +11375,7 @@ package body Exp_Ch9 is
 
          Insert_Before (Stmt,
            Make_Assignment_Statement (Loc,
-             Name => New_Reference_To (D, Loc),
+             Name       => New_Reference_To (D, Loc),
              Expression => D_Conv));
 
          Call   := Stmt;
@@ -11451,8 +11435,9 @@ package body Exp_Ch9 is
 
                   Rewrite (Call,
                     Make_Procedure_Call_Statement (Loc,
-                      Name => New_Reference_To (
-                        RTE (RE_Timed_Protected_Single_Entry_Call), Loc),
+                      Name =>
+                        New_Reference_To
+                          (RTE (RE_Timed_Protected_Single_Entry_Call), Loc),
                       Parameter_Associations => Params));
 
                when others =>
@@ -11477,14 +11462,14 @@ package body Exp_Ch9 is
 
          Append_To (Stmts,
            Make_Implicit_If_Statement (N,
-             Condition => New_Reference_To (B, Loc),
+             Condition       => New_Reference_To (B, Loc),
              Then_Statements => E_Stats,
              Else_Statements => D_Stats));
       end if;
 
       Rewrite (N,
         Make_Block_Statement (Loc,
-          Declarations => Decls,
+          Declarations               => Decls,
           Handled_Statement_Sequence =>
             Make_Handled_Sequence_Of_Statements (Loc, Stmts)));
 
diff --git a/gcc/ada/exp_light.adb b/gcc/ada/exp_light.adb
deleted file mode 100644
index 47aa2e64e9c..00000000000
--- a/gcc/ada/exp_light.adb
+++ /dev/null
@@ -1,64 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                            E X P _ L I G H T                             --
---                                                                          --
---                                 B o d y                                  --
---                                                                          --
---             Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
-with Atree;          use Atree;
-with Exp_Attr_Light; use Exp_Attr_Light;
-with Exp_Ch6_Light;  use Exp_Ch6_Light;
-with Exp_Ch7_Light;  use Exp_Ch7_Light;
-with Sinfo;          use Sinfo;
-
-package body Exp_Light is
-
-   ------------------
-   -- Expand_Light --
-   ------------------
-
-   procedure Expand_Light (N : Node_Id) is
-   begin
-      case Nkind (N) is
-
-         when N_Package_Declaration =>
-            Expand_Light_N_Package_Declaration (N);
-
-         when N_Simple_Return_Statement =>
-            Expand_Light_N_Simple_Return_Statement (N);
-
-         when N_Subprogram_Body =>
-            Expand_Light_N_Subprogram_Body (N);
-
-         when N_Function_Call            |
-              N_Procedure_Call_Statement =>
-            Expand_Light_Call (N);
-
-         when N_Attribute_Reference =>
-            Expand_Light_N_Attribute_Reference (N);
-
-         when others =>
-            null;
-
-      end case;
-   end Expand_Light;
-
-end Exp_Light;
diff --git a/gcc/ada/exp_light.ads b/gcc/ada/exp_light.ads
deleted file mode 100644
index 26804596f23..00000000000
--- a/gcc/ada/exp_light.ads
+++ /dev/null
@@ -1,52 +0,0 @@
-------------------------------------------------------------------------------
---                                                                          --
---                         GNAT COMPILER COMPONENTS                         --
---                                                                          --
---                            E X P _ L I G H T                             --
---                                                                          --
---                                 S p e c                                  --
---                                                                          --
---             Copyright (C) 2011, 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- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
--- for  more details.  You should have  received  a copy of the GNU General --
--- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license.          --
---                                                                          --
--- GNAT was originally developed  by the GNAT team at  New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc.      --
---                                                                          --
-------------------------------------------------------------------------------
-
---  This package implements a light expansion which is used in formal
---  verification mode. Instead of a complete expansion of nodes for code
---  generation, this light expansion targets generation of intermediate code
---  for formal verification.
-
---  Expand_Light is called directly by Expander.Expand.
-
---  Light expansion has three main objectives:
-
---    1. Perform limited expansion to explicit some Ada rules and constructs
---       (translate 'Old and 'Result, replace renamings by renamed, insert
---        conversions, expand actuals in calls to introduce temporaries)
-
---    2. Facilitate treatment for the formal verification back-end (fully
---       qualify names)
-
---    3. Avoid the introduction of low-level code that is difficult to analyze
---       formally, as typically done in the full expansion for high-level
---       constructs (tasking, dispatching)
-
-with Types; use Types;
-
-package Exp_Light is
-
-   procedure Expand_Light (N : Node_Id);
-
-end Exp_Light;
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 22e9bb04691..5c3d2ca2777 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -321,6 +321,15 @@ package body Exp_Prag is
       --  be an explicit conditional in the source, not an implicit if, so we
       --  do not call Make_Implicit_If_Statement.
 
+      --  In formal verification mode, we keep the pragma check in the code,
+      --  and its enclosed expression is not expanded. This requires that no
+      --  transient scope is introduced for pragma check in this mode in
+      --  Exp_Ch7.Establish_Transient_Scope.
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Case where we generate a direct raise
 
       if ((Debug_Flag_Dot_G
diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb
index 59045e73a77..95b5d978c67 100644
--- a/gcc/ada/expander.adb
+++ b/gcc/ada/expander.adb
@@ -39,7 +39,6 @@ with Exp_Ch9;   use Exp_Ch9;
 with Exp_Ch11;  use Exp_Ch11;
 with Exp_Ch12;  use Exp_Ch12;
 with Exp_Ch13;  use Exp_Ch13;
-with Exp_Light; use Exp_Light;
 with Exp_Prag;  use Exp_Prag;
 with Opt;       use Opt;
 with Rtsfind;   use Rtsfind;
@@ -132,331 +131,325 @@ package body Expander is
          --  routines.
 
          begin
-            if ALFA_Mode then
-               Expand_Light (N);
-
-            else
-               case Nkind (N) is
+            case Nkind (N) is
 
-                  when N_Abort_Statement =>
-                     Expand_N_Abort_Statement (N);
+               when N_Abort_Statement =>
+                  Expand_N_Abort_Statement (N);
 
-                  when N_Accept_Statement =>
-                     Expand_N_Accept_Statement (N);
+               when N_Accept_Statement =>
+                  Expand_N_Accept_Statement (N);
 
-                  when N_Aggregate =>
-                     Expand_N_Aggregate (N);
+               when N_Aggregate =>
+                  Expand_N_Aggregate (N);
 
-                  when N_Allocator =>
-                     Expand_N_Allocator (N);
+               when N_Allocator =>
+                  Expand_N_Allocator (N);
 
-                  when N_And_Then =>
-                     Expand_N_And_Then (N);
+               when N_And_Then =>
+                  Expand_N_And_Then (N);
 
-                  when N_Assignment_Statement =>
-                     Expand_N_Assignment_Statement (N);
+               when N_Assignment_Statement =>
+                  Expand_N_Assignment_Statement (N);
 
-                  when N_Asynchronous_Select =>
-                     Expand_N_Asynchronous_Select (N);
+               when N_Asynchronous_Select =>
+                  Expand_N_Asynchronous_Select (N);
 
-                  when N_Attribute_Definition_Clause =>
-                     Expand_N_Attribute_Definition_Clause (N);
+               when N_Attribute_Definition_Clause =>
+                  Expand_N_Attribute_Definition_Clause (N);
 
-                  when N_Attribute_Reference =>
-                     Expand_N_Attribute_Reference (N);
+               when N_Attribute_Reference =>
+                  Expand_N_Attribute_Reference (N);
 
-                  when N_Block_Statement =>
-                     Expand_N_Block_Statement (N);
+               when N_Block_Statement =>
+                  Expand_N_Block_Statement (N);
 
-                  when N_Case_Expression =>
-                     Expand_N_Case_Expression (N);
+               when N_Case_Expression =>
+                  Expand_N_Case_Expression (N);
 
-                  when N_Case_Statement =>
-                     Expand_N_Case_Statement (N);
+               when N_Case_Statement =>
+                  Expand_N_Case_Statement (N);
 
-                  when N_Conditional_Entry_Call =>
-                     Expand_N_Conditional_Entry_Call (N);
+               when N_Conditional_Entry_Call =>
+                  Expand_N_Conditional_Entry_Call (N);
 
-                  when N_Conditional_Expression =>
-                     Expand_N_Conditional_Expression (N);
+               when N_Conditional_Expression =>
+                  Expand_N_Conditional_Expression (N);
 
-                  when N_Delay_Relative_Statement =>
-                     Expand_N_Delay_Relative_Statement (N);
+               when N_Delay_Relative_Statement =>
+                  Expand_N_Delay_Relative_Statement (N);
 
-                  when N_Delay_Until_Statement =>
-                     Expand_N_Delay_Until_Statement (N);
+               when N_Delay_Until_Statement =>
+                  Expand_N_Delay_Until_Statement (N);
 
-                  when N_Entry_Body =>
-                     Expand_N_Entry_Body (N);
+               when N_Entry_Body =>
+                  Expand_N_Entry_Body (N);
 
-                  when N_Entry_Call_Statement =>
-                     Expand_N_Entry_Call_Statement (N);
+               when N_Entry_Call_Statement =>
+                  Expand_N_Entry_Call_Statement (N);
 
-                  when N_Entry_Declaration =>
-                     Expand_N_Entry_Declaration (N);
+               when N_Entry_Declaration =>
+                  Expand_N_Entry_Declaration (N);
 
-                  when N_Exception_Declaration =>
-                     Expand_N_Exception_Declaration (N);
+               when N_Exception_Declaration =>
+                  Expand_N_Exception_Declaration (N);
 
-                  when N_Exception_Renaming_Declaration =>
-                     Expand_N_Exception_Renaming_Declaration (N);
+               when N_Exception_Renaming_Declaration =>
+                  Expand_N_Exception_Renaming_Declaration (N);
 
-                  when N_Exit_Statement =>
-                     Expand_N_Exit_Statement (N);
+               when N_Exit_Statement =>
+                  Expand_N_Exit_Statement (N);
 
-                  when N_Expanded_Name =>
-                     Expand_N_Expanded_Name (N);
+               when N_Expanded_Name =>
+                  Expand_N_Expanded_Name (N);
 
-                  when N_Explicit_Dereference =>
-                     Expand_N_Explicit_Dereference (N);
+               when N_Explicit_Dereference =>
+                  Expand_N_Explicit_Dereference (N);
 
-                  when N_Expression_With_Actions =>
-                     Expand_N_Expression_With_Actions (N);
+               when N_Expression_With_Actions =>
+                  Expand_N_Expression_With_Actions (N);
 
-                  when N_Extended_Return_Statement =>
-                     Expand_N_Extended_Return_Statement (N);
+               when N_Extended_Return_Statement =>
+                  Expand_N_Extended_Return_Statement (N);
 
-                  when N_Extension_Aggregate =>
-                     Expand_N_Extension_Aggregate (N);
+               when N_Extension_Aggregate =>
+                  Expand_N_Extension_Aggregate (N);
 
-                  when N_Free_Statement =>
-                     Expand_N_Free_Statement (N);
+               when N_Free_Statement =>
+                  Expand_N_Free_Statement (N);
 
-                  when N_Freeze_Entity =>
-                     Expand_N_Freeze_Entity (N);
+               when N_Freeze_Entity =>
+                  Expand_N_Freeze_Entity (N);
 
-                  when N_Full_Type_Declaration =>
-                     Expand_N_Full_Type_Declaration (N);
+               when N_Full_Type_Declaration =>
+                  Expand_N_Full_Type_Declaration (N);
 
-                  when N_Function_Call =>
-                     Expand_N_Function_Call (N);
+               when N_Function_Call =>
+                  Expand_N_Function_Call (N);
 
-                  when N_Generic_Instantiation =>
-                     Expand_N_Generic_Instantiation (N);
+               when N_Generic_Instantiation =>
+                  Expand_N_Generic_Instantiation (N);
 
-                  when N_Goto_Statement =>
-                     Expand_N_Goto_Statement (N);
+               when N_Goto_Statement =>
+                  Expand_N_Goto_Statement (N);
 
-                  when N_Handled_Sequence_Of_Statements =>
-                     Expand_N_Handled_Sequence_Of_Statements (N);
+               when N_Handled_Sequence_Of_Statements =>
+                  Expand_N_Handled_Sequence_Of_Statements (N);
 
-                  when N_Identifier =>
-                     Expand_N_Identifier (N);
+               when N_Identifier =>
+                  Expand_N_Identifier (N);
 
-                  when N_Indexed_Component =>
-                     Expand_N_Indexed_Component (N);
+               when N_Indexed_Component =>
+                  Expand_N_Indexed_Component (N);
 
-                  when N_If_Statement =>
-                     Expand_N_If_Statement (N);
+               when N_If_Statement =>
+                  Expand_N_If_Statement (N);
 
-                  when N_In =>
-                     Expand_N_In (N);
+               when N_In =>
+                  Expand_N_In (N);
 
-                  when N_Loop_Statement =>
-                     Expand_N_Loop_Statement (N);
+               when N_Loop_Statement =>
+                  Expand_N_Loop_Statement (N);
 
-                  when N_Not_In =>
-                     Expand_N_Not_In (N);
+               when N_Not_In =>
+                  Expand_N_Not_In (N);
 
-                  when N_Null =>
-                     Expand_N_Null (N);
+               when N_Null =>
+                  Expand_N_Null (N);
 
-                  when N_Object_Declaration =>
-                     Expand_N_Object_Declaration (N);
+               when N_Object_Declaration =>
+                  Expand_N_Object_Declaration (N);
 
-                  when N_Object_Renaming_Declaration =>
-                     Expand_N_Object_Renaming_Declaration (N);
+               when N_Object_Renaming_Declaration =>
+                  Expand_N_Object_Renaming_Declaration (N);
 
-                  when N_Op_Add =>
-                     Expand_N_Op_Add (N);
+               when N_Op_Add =>
+                  Expand_N_Op_Add (N);
 
-                  when N_Op_Abs =>
-                     Expand_N_Op_Abs (N);
+               when N_Op_Abs =>
+                  Expand_N_Op_Abs (N);
 
-                  when N_Op_And =>
-                     Expand_N_Op_And (N);
+               when N_Op_And =>
+                  Expand_N_Op_And (N);
 
-                  when N_Op_Concat =>
-                     Expand_N_Op_Concat (N);
+               when N_Op_Concat =>
+                  Expand_N_Op_Concat (N);
 
-                  when N_Op_Divide =>
-                     Expand_N_Op_Divide (N);
+               when N_Op_Divide =>
+                  Expand_N_Op_Divide (N);
 
-                  when N_Op_Eq =>
-                     Expand_N_Op_Eq (N);
+               when N_Op_Eq =>
+                  Expand_N_Op_Eq (N);
 
-                  when N_Op_Expon =>
-                     Expand_N_Op_Expon (N);
+               when N_Op_Expon =>
+                  Expand_N_Op_Expon (N);
 
-                  when N_Op_Ge =>
-                     Expand_N_Op_Ge (N);
+               when N_Op_Ge =>
+                  Expand_N_Op_Ge (N);
 
-                  when N_Op_Gt =>
-                     Expand_N_Op_Gt (N);
+               when N_Op_Gt =>
+                  Expand_N_Op_Gt (N);
 
-                  when N_Op_Le =>
-                     Expand_N_Op_Le (N);
+               when N_Op_Le =>
+                  Expand_N_Op_Le (N);
 
-                  when N_Op_Lt =>
-                     Expand_N_Op_Lt (N);
+               when N_Op_Lt =>
+                  Expand_N_Op_Lt (N);
 
-                  when N_Op_Minus =>
-                     Expand_N_Op_Minus (N);
+               when N_Op_Minus =>
+                  Expand_N_Op_Minus (N);
 
-                  when N_Op_Mod =>
-                     Expand_N_Op_Mod (N);
+               when N_Op_Mod =>
+                  Expand_N_Op_Mod (N);
 
-                  when N_Op_Multiply =>
-                     Expand_N_Op_Multiply (N);
+               when N_Op_Multiply =>
+                  Expand_N_Op_Multiply (N);
 
-                  when N_Op_Ne =>
-                     Expand_N_Op_Ne (N);
+               when N_Op_Ne =>
+                  Expand_N_Op_Ne (N);
 
-                  when N_Op_Not =>
-                     Expand_N_Op_Not (N);
+               when N_Op_Not =>
+                  Expand_N_Op_Not (N);
 
-                  when N_Op_Or =>
-                     Expand_N_Op_Or (N);
+               when N_Op_Or =>
+                  Expand_N_Op_Or (N);
 
-                  when N_Op_Plus =>
-                     Expand_N_Op_Plus (N);
+               when N_Op_Plus =>
+                  Expand_N_Op_Plus (N);
 
-                  when N_Op_Rem =>
-                     Expand_N_Op_Rem (N);
+               when N_Op_Rem =>
+                  Expand_N_Op_Rem (N);
 
-                  when N_Op_Rotate_Left =>
-                     Expand_N_Op_Rotate_Left (N);
+               when N_Op_Rotate_Left =>
+                  Expand_N_Op_Rotate_Left (N);
 
-                  when N_Op_Rotate_Right =>
-                     Expand_N_Op_Rotate_Right (N);
+               when N_Op_Rotate_Right =>
+                  Expand_N_Op_Rotate_Right (N);
 
-                  when N_Op_Shift_Left =>
-                     Expand_N_Op_Shift_Left (N);
+               when N_Op_Shift_Left =>
+                  Expand_N_Op_Shift_Left (N);
 
-                  when N_Op_Shift_Right =>
-                     Expand_N_Op_Shift_Right (N);
+               when N_Op_Shift_Right =>
+                  Expand_N_Op_Shift_Right (N);
 
-                  when N_Op_Shift_Right_Arithmetic =>
-                     Expand_N_Op_Shift_Right_Arithmetic (N);
+               when N_Op_Shift_Right_Arithmetic =>
+                  Expand_N_Op_Shift_Right_Arithmetic (N);
 
-                  when N_Op_Subtract =>
-                     Expand_N_Op_Subtract (N);
+               when N_Op_Subtract =>
+                  Expand_N_Op_Subtract (N);
 
-                  when N_Op_Xor =>
-                     Expand_N_Op_Xor (N);
+               when N_Op_Xor =>
+                  Expand_N_Op_Xor (N);
 
-                  when N_Or_Else =>
-                     Expand_N_Or_Else (N);
+               when N_Or_Else =>
+                  Expand_N_Or_Else (N);
 
-                  when N_Package_Body =>
-                     Expand_N_Package_Body (N);
+               when N_Package_Body =>
+                  Expand_N_Package_Body (N);
 
-                  when N_Package_Declaration =>
-                     Expand_N_Package_Declaration (N);
+               when N_Package_Declaration =>
+                  Expand_N_Package_Declaration (N);
 
-                  when N_Package_Renaming_Declaration =>
-                     Expand_N_Package_Renaming_Declaration (N);
+               when N_Package_Renaming_Declaration =>
+                  Expand_N_Package_Renaming_Declaration (N);
 
-                  when N_Subprogram_Renaming_Declaration =>
-                     Expand_N_Subprogram_Renaming_Declaration (N);
+               when N_Subprogram_Renaming_Declaration =>
+                  Expand_N_Subprogram_Renaming_Declaration (N);
 
-                  when N_Pragma =>
-                     Expand_N_Pragma (N);
+               when N_Pragma =>
+                  Expand_N_Pragma (N);
 
-                  when N_Procedure_Call_Statement =>
-                     Expand_N_Procedure_Call_Statement (N);
+               when N_Procedure_Call_Statement =>
+                  Expand_N_Procedure_Call_Statement (N);
 
-                  when N_Protected_Type_Declaration =>
-                     Expand_N_Protected_Type_Declaration (N);
+               when N_Protected_Type_Declaration =>
+                  Expand_N_Protected_Type_Declaration (N);
 
-                  when N_Protected_Body =>
-                     Expand_N_Protected_Body (N);
+               when N_Protected_Body =>
+                  Expand_N_Protected_Body (N);
 
-                  when N_Qualified_Expression =>
-                     Expand_N_Qualified_Expression (N);
+               when N_Qualified_Expression =>
+                  Expand_N_Qualified_Expression (N);
 
-                  when N_Quantified_Expression  =>
-                     Expand_N_Quantified_Expression (N);
+               when N_Quantified_Expression  =>
+                  Expand_N_Quantified_Expression (N);
 
-                  when N_Raise_Statement =>
-                     Expand_N_Raise_Statement (N);
+               when N_Raise_Statement =>
+                  Expand_N_Raise_Statement (N);
 
-                  when N_Raise_Constraint_Error =>
-                     Expand_N_Raise_Constraint_Error (N);
+               when N_Raise_Constraint_Error =>
+                  Expand_N_Raise_Constraint_Error (N);
 
-                  when N_Raise_Program_Error =>
-                     Expand_N_Raise_Program_Error (N);
+               when N_Raise_Program_Error =>
+                  Expand_N_Raise_Program_Error (N);
 
-                  when N_Raise_Storage_Error =>
-                     Expand_N_Raise_Storage_Error (N);
+               when N_Raise_Storage_Error =>
+                  Expand_N_Raise_Storage_Error (N);
 
-                  when N_Real_Literal =>
-                     Expand_N_Real_Literal (N);
+               when N_Real_Literal =>
+                  Expand_N_Real_Literal (N);
 
-                  when N_Record_Representation_Clause =>
-                     Expand_N_Record_Representation_Clause (N);
+               when N_Record_Representation_Clause =>
+                  Expand_N_Record_Representation_Clause (N);
 
-                  when N_Requeue_Statement =>
-                     Expand_N_Requeue_Statement (N);
+               when N_Requeue_Statement =>
+                  Expand_N_Requeue_Statement (N);
 
-                  when N_Simple_Return_Statement =>
-                     Expand_N_Simple_Return_Statement (N);
+               when N_Simple_Return_Statement =>
+                  Expand_N_Simple_Return_Statement (N);
 
-                  when N_Selected_Component =>
-                     Expand_N_Selected_Component (N);
+               when N_Selected_Component =>
+                  Expand_N_Selected_Component (N);
 
-                  when N_Selective_Accept =>
-                     Expand_N_Selective_Accept (N);
+               when N_Selective_Accept =>
+                  Expand_N_Selective_Accept (N);
 
-                  when N_Single_Task_Declaration =>
-                     Expand_N_Single_Task_Declaration (N);
+               when N_Single_Task_Declaration =>
+                  Expand_N_Single_Task_Declaration (N);
 
-                  when N_Slice =>
-                     Expand_N_Slice (N);
+               when N_Slice =>
+                  Expand_N_Slice (N);
 
-                  when N_Subtype_Indication =>
-                     Expand_N_Subtype_Indication (N);
+               when N_Subtype_Indication =>
+                  Expand_N_Subtype_Indication (N);
 
-                  when N_Subprogram_Body =>
-                     Expand_N_Subprogram_Body (N);
+               when N_Subprogram_Body =>
+                  Expand_N_Subprogram_Body (N);
 
-                  when N_Subprogram_Body_Stub =>
-                     Expand_N_Subprogram_Body_Stub (N);
+               when N_Subprogram_Body_Stub =>
+                  Expand_N_Subprogram_Body_Stub (N);
 
-                  when N_Subprogram_Declaration =>
-                     Expand_N_Subprogram_Declaration (N);
+               when N_Subprogram_Declaration =>
+                  Expand_N_Subprogram_Declaration (N);
 
-                  when N_Subprogram_Info =>
-                     Expand_N_Subprogram_Info (N);
+               when N_Subprogram_Info =>
+                  Expand_N_Subprogram_Info (N);
 
-                  when N_Task_Body =>
-                     Expand_N_Task_Body (N);
+               when N_Task_Body =>
+                  Expand_N_Task_Body (N);
 
-                  when N_Task_Type_Declaration =>
-                     Expand_N_Task_Type_Declaration (N);
+               when N_Task_Type_Declaration =>
+                  Expand_N_Task_Type_Declaration (N);
 
-                  when N_Timed_Entry_Call =>
-                     Expand_N_Timed_Entry_Call (N);
+               when N_Timed_Entry_Call =>
+                  Expand_N_Timed_Entry_Call (N);
 
-                  when N_Type_Conversion =>
-                     Expand_N_Type_Conversion (N);
+               when N_Type_Conversion =>
+                  Expand_N_Type_Conversion (N);
 
-                  when N_Unchecked_Expression =>
-                     Expand_N_Unchecked_Expression (N);
+               when N_Unchecked_Expression =>
+                  Expand_N_Unchecked_Expression (N);
 
-                  when N_Unchecked_Type_Conversion =>
-                     Expand_N_Unchecked_Type_Conversion (N);
+               when N_Unchecked_Type_Conversion =>
+                  Expand_N_Unchecked_Type_Conversion (N);
 
-                  when N_Variant_Part =>
-                     Expand_N_Variant_Part (N);
+               when N_Variant_Part =>
+                  Expand_N_Variant_Part (N);
 
-                  --  For all other node kinds, no expansion activity is
-                  --  required.
+               --  For all other node kinds, no expansion activity is required
 
-                  when others => null;
+               when others => null;
 
-               end case;
-            end if;
+            end case;
 
          exception
             when RE_Not_Available =>
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index b538f4bc82e..f371afafa45 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -435,9 +435,8 @@ procedure Gnat1drv is
 
          Polling_Required := False;
 
-         --  Set operating mode to Generate_Code, but full front-end expansion
-         --  is not desirable in ALFA mode, so a light expansion is performed
-         --  instead.
+         --  Set operating mode to Generate_Code to benefit from full front-end
+         --  expansion (e.g. default arguments).
 
          Operating_Mode := Generate_Code;
 
diff --git a/gcc/ada/s-secsta.adb b/gcc/ada/s-secsta.adb
index 1a4aa788c41..0afea184baf 100644
--- a/gcc/ada/s-secsta.adb
+++ b/gcc/ada/s-secsta.adb
@@ -33,6 +33,7 @@ pragma Compiler_Unit;
 
 with System.Soft_Links;
 with System.Parameters;
+
 with Ada.Unchecked_Conversion;
 with Ada.Unchecked_Deallocation;
 
diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb
index be295eb8582..74d522c985a 100644
--- a/gcc/ada/s-tassta.adb
+++ b/gcc/ada/s-tassta.adb
@@ -1023,9 +1023,10 @@ package body System.Tasking.Stages is
       Secondary_Stack_Size :
         constant SSE.Storage_Offset :=
           Self_ID.Common.Compiler_Data.Pri_Stack_Info.Size *
-          SSE.Storage_Offset (Parameters.Sec_Stack_Percentage) / 100;
+            SSE.Storage_Offset (Parameters.Sec_Stack_Percentage) / 100;
 
       Secondary_Stack : aliased SSE.Storage_Array (1 .. Secondary_Stack_Size);
+      --  Actual area allocated for secondary stack
 
       Secondary_Stack_Address : System.Address := Secondary_Stack'Address;
       --  Address of secondary stack. In the fixed secondary stack case, this
@@ -1086,6 +1087,8 @@ package body System.Tasking.Stages is
          end if;
       end Search_Fall_Back_Handler;
 
+   --  Start of processing for Task_Wrapper
+
    begin
       pragma Assert (Self_ID.Deferral_Level = 1);