[multiple changes]

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

	* exp_aggr.adb, exp_ch11.adb, exp_prag.adb: Remove early exit during
	expansion in Alfa mode.
	* exp_ch6.adb, exp_ch6.ads (Expand_Actuals): Make subprogram public
	* exp_alfa.adb, exp_alfa.ads: New package defining light expansion for
	Alfa mode.
	* gnat1drv.adb (Adjust_Global_Switches): Update Comment.
	* sem_res.adb: Ditto.

2011-08-30  Thomas Quinot  <quinot@adacore.com>

	* g-socket.ads: Minor documentation adjustment.

From-SVN: r178317

12 files changed, 386 insertions, 58 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 81574bb..ab5c1b1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2011-08-30  Yannick Moy  <moy@adacore.com>
+
+	* exp_aggr.adb, exp_ch11.adb, exp_prag.adb: Remove early exit during
+	expansion in Alfa mode.
+	* exp_ch6.adb, exp_ch6.ads (Expand_Actuals): Make subprogram public
+	* exp_alfa.adb, exp_alfa.ads: New package defining light expansion for
+	Alfa mode.
+	* gnat1drv.adb (Adjust_Global_Switches): Update Comment.
+	* sem_res.adb: Ditto.
+
+2011-08-30  Thomas Quinot  <quinot@adacore.com>
+
+	* g-socket.ads: Minor documentation adjustment.
+
 2011-08-30  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch9.adb, s-tassta.adb, s-secsta.adb: Minor reformatting.
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 037a8dc..a54ebe8 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4664,12 +4664,6 @@ 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_alfa.adb b/gcc/ada/exp_alfa.adb
new file mode 100644
index 0000000..5d2bb66
--- /dev/null
+++ b/gcc/ada/exp_alfa.adb
@@ -0,0 +1,270 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                             E X P _ A L F A                              --
+--                                                                          --
+--                                 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_Attr; use Exp_Attr;
+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 Snames;   use Snames;
+with Stand;    use Stand;
+with Tbuild;   use Tbuild;
+
+package body Exp_Alfa is
+
+   -----------------------
+   -- Local Subprograms --
+   -----------------------
+
+   procedure Expand_Alfa_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_Alfa_N_Attribute_Reference (N : Node_Id);
+   --  Expand attributes 'Old and 'Result only
+
+   procedure Expand_Alfa_N_Package_Declaration (N : Node_Id);
+   --  Fully qualify names of enclosed entities
+
+   procedure Expand_Alfa_N_Simple_Return_Statement (N : Node_Id);
+   --  Insert conversion on function return if necessary
+
+   procedure Expand_Alfa_N_Subprogram_Body (N : Node_Id);
+   --  Fully qualify names of enclosed entities
+
+   procedure Expand_Alfa_Simple_Function_Return (N : Node_Id);
+   --  Expand simple return from function
+
+   -----------------
+   -- Expand_Alfa --
+   -----------------
+
+   procedure Expand_Alfa (N : Node_Id) is
+   begin
+      case Nkind (N) is
+
+         when N_Package_Declaration =>
+            Expand_Alfa_N_Package_Declaration (N);
+
+         when N_Simple_Return_Statement =>
+            Expand_Alfa_N_Simple_Return_Statement (N);
+
+         when N_Subprogram_Body =>
+            Expand_Alfa_N_Subprogram_Body (N);
+
+         when N_Function_Call            |
+              N_Procedure_Call_Statement =>
+            Expand_Alfa_Call (N);
+
+         when N_Attribute_Reference =>
+            Expand_Alfa_N_Attribute_Reference (N);
+
+         when others =>
+            null;
+
+      end case;
+   end Expand_Alfa;
+
+   ----------------------
+   -- Expand_Alfa_Call --
+   ----------------------
+
+   procedure Expand_Alfa_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_Alfa_Call;
+
+   ---------------------------------------
+   -- Expand_Alfa_N_Attribute_Reference --
+   ---------------------------------------
+
+   procedure Expand_Alfa_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_Alfa_N_Attribute_Reference;
+
+   ---------------------------------------
+   -- Expand_Alfa_N_Package_Declaration --
+   ---------------------------------------
+
+   procedure Expand_Alfa_N_Package_Declaration (N : Node_Id) is
+   begin
+      Qualify_Entity_Names (N);
+   end Expand_Alfa_N_Package_Declaration;
+
+   -------------------------------------------
+   -- Expand_Alfa_N_Simple_Return_Statement --
+   -------------------------------------------
+
+   procedure Expand_Alfa_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_Alfa_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_Alfa_N_Simple_Return_Statement;
+
+   -----------------------------------
+   -- Expand_Alfa_N_Subprogram_Body --
+   -----------------------------------
+
+   procedure Expand_Alfa_N_Subprogram_Body (N : Node_Id) is
+   begin
+      Qualify_Entity_Names (N);
+   end Expand_Alfa_N_Subprogram_Body;
+
+   ----------------------------------------
+   -- Expand_Alfa_Simple_Function_Return --
+   ----------------------------------------
+
+   procedure Expand_Alfa_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_Alfa_Simple_Function_Return;
+
+end Exp_Alfa;
diff --git a/gcc/ada/exp_alfa.ads b/gcc/ada/exp_alfa.ads
new file mode 100644
index 0000000..a5c0786
--- /dev/null
+++ b/gcc/ada/exp_alfa.ads
@@ -0,0 +1,52 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                             E X P _ A L F A                              --
+--                                                                          --
+--                                 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 Alfa expansion targets generation of intermediate code
+--  for formal verification.
+
+--  Expand_Alfa is called directly by Expander.Expand.
+
+--  Alfa 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_Alfa is
+
+   procedure Expand_Alfa (N : Node_Id);
+
+end Exp_Alfa;
diff --git a/gcc/ada/exp_ch11.adb b/gcc/ada/exp_ch11.adb
index caf66cc..dca021f 100644
--- a/gcc/ada/exp_ch11.adb
+++ b/gcc/ada/exp_ch11.adb
@@ -1673,7 +1673,6 @@ 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 b390db4..6780f6e8 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -156,36 +156,6 @@ 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 1896ce2..95a10ec 100644
--- a/gcc/ada/exp_ch6.ads
+++ b/gcc/ada/exp_ch6.ads
@@ -37,6 +37,36 @@ 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_prag.adb b/gcc/ada/exp_prag.adb
index 5c3d2ca..22e9bb0 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -321,15 +321,6 @@ 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 95b5d97..f14fca0 100644
--- a/gcc/ada/expander.adb
+++ b/gcc/ada/expander.adb
@@ -27,6 +27,7 @@ with Atree;     use Atree;
 with Debug_A;   use Debug_A;
 with Errout;    use Errout;
 with Exp_Aggr;  use Exp_Aggr;
+with Exp_Alfa;  use Exp_Alfa;
 with Exp_Attr;  use Exp_Attr;
 with Exp_Ch2;   use Exp_Ch2;
 with Exp_Ch3;   use Exp_Ch3;
@@ -131,7 +132,12 @@ package body Expander is
          --  routines.
 
          begin
-            case Nkind (N) is
+            if ALFA_Mode then
+               Expand_Alfa (N);
+
+            else
+
+               case Nkind (N) is
 
                when N_Abort_Statement =>
                   Expand_N_Abort_Statement (N);
@@ -449,7 +455,9 @@ package body Expander is
 
                when others => null;
 
-            end case;
+               end case;
+
+            end if;
 
          exception
             when RE_Not_Available =>
diff --git a/gcc/ada/g-socket.ads b/gcc/ada/g-socket.ads
index 0ac9889..0198328 100644
--- a/gcc/ada/g-socket.ads
+++ b/gcc/ada/g-socket.ads
@@ -427,17 +427,16 @@ package GNAT.Sockets is
 
    --  Timeval_Duration is a subtype of Standard.Duration because the full
    --  range of Standard.Duration cannot be represented in the equivalent C
-   --  structure. Moreover, negative values are not allowed to avoid system
-   --  incompatibilities.
+   --  structure (struct timeval). Moreover, negative values are not allowed
+   --  to avoid system incompatibilities.
 
    Immediate : constant Duration := 0.0;
 
-   Timeval_Forever : constant := 1.0 * SOSC.MAX_tv_sec;
    Forever         : constant Duration :=
-                       Duration'Min (Duration'Last, Timeval_Forever);
+                       Duration'Min (Duration'Last, 1.0 * SOSC.MAX_tv_sec);
+   --  Largest possible Duration that is also a valid value for struct timeval
+
    subtype Timeval_Duration is Duration range Immediate .. Forever;
-   --  These needs commenting, in particular we should explain what these is
-   --  used for, and how the Timeval_Forever value is chosen (see r176463) ???
 
    subtype Selector_Duration is Timeval_Duration;
    --  Timeout value for selector operations
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index f371afa..b538f4b 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -435,8 +435,9 @@ procedure Gnat1drv is
 
          Polling_Required := False;
 
-         --  Set operating mode to Generate_Code to benefit from full front-end
-         --  expansion (e.g. default arguments).
+         --  Set operating mode to Generate_Code, but full front-end expansion
+         --  is not desirable in ALFA mode, so a light expansion is performed
+         --  instead.
 
          Operating_Mode := Generate_Code;
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 074f5f2..2b0bb02 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -8094,8 +8094,8 @@ package body Sem_Res is
          Resolve (Condition (N), Typ);
          Expander_Mode_Restore;
 
-      --  In ALFA_Mode, no magic needed, we just resolve the underlying nodes
-      --  But why is this special handling for ALFA_Mode required ???
+      --  In ALFA mode, we need expansion in order to introduce properly the
+      --  necessary transient scopes.
 
       else
          Resolve (Condition (N), Typ);