Patchwork [Ada] Define a light expansion mode for formal verification

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 30, 2011, 1:42 p.m.
Message ID <20110830134243.GA18660@adacore.com>
Download mbox | patch
Permalink /patch/112295/
State New
Headers show

Comments

Arnaud Charlet - Aug. 30, 2011, 1:42 p.m.
Instead of the full expansion targetting code generation, a light expansion is
now used in formal verification mode. Light expansion has three main objectives:

1. Perform limited expansion to explicit some Ada rules and constructs
2. Facilitate treatment for the formal verification back-end
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)

Also remove special exits from full expansion that were previously needed.

Note that this is an intermediate step/change. A better/cleaner approach
will follow using exp_alfa.ad{s,b} files.

Tested on x86_64-pc-linux-gnu, committed on trunk

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_light.adb, exp_light.ads: New package defining light expansion.
	* expander.adb (Expand): Call light expansion in Alfa mode
	* exp_ch6_light.adb, exp_ch6_light.ads: Light expansion of chapter 6
	constructs.
	* exp_ch7_light.adb, exp_ch7_light.ads: Light expansion of chapter 7
	constructs.
	* exp_attr_light.adb, exp_attr_light.ads: Light expansion of attributes
	* gnat1drv.adb (Adjust_Global_Switches): Comment

Patch

Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 178293)
+++ exp_prag.adb	(working copy)
@@ -321,15 +321,6 @@ 
       --  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
Index: exp_ch6_light.adb
===================================================================
--- exp_ch6_light.adb	(revision 0)
+++ exp_ch6_light.adb	(revision 0)
@@ -0,0 +1,193 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_ch6_light.ads
===================================================================
--- exp_ch6_light.ads	(revision 0)
+++ exp_ch6_light.ads	(revision 0)
@@ -0,0 +1,44 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: expander.adb
===================================================================
--- expander.adb	(revision 178293)
+++ expander.adb	(working copy)
@@ -39,6 +39,7 @@ 
 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;
@@ -131,326 +132,332 @@ 
          --  routines.
 
          begin
-            case Nkind (N) is
+            if ALFA_Mode then
+               Expand_Light (N);
 
-               when N_Abort_Statement =>
-                  Expand_N_Abort_Statement (N);
+            else
+               case Nkind (N) is
 
-               when N_Accept_Statement =>
-                  Expand_N_Accept_Statement (N);
+                  when N_Abort_Statement =>
+                     Expand_N_Abort_Statement (N);
 
-               when N_Aggregate =>
-                  Expand_N_Aggregate (N);
+                  when N_Accept_Statement =>
+                     Expand_N_Accept_Statement (N);
 
-               when N_Allocator =>
-                  Expand_N_Allocator (N);
+                  when N_Aggregate =>
+                     Expand_N_Aggregate (N);
 
-               when N_And_Then =>
-                  Expand_N_And_Then (N);
+                  when N_Allocator =>
+                     Expand_N_Allocator (N);
 
-               when N_Assignment_Statement =>
-                  Expand_N_Assignment_Statement (N);
+                  when N_And_Then =>
+                     Expand_N_And_Then (N);
 
-               when N_Asynchronous_Select =>
-                  Expand_N_Asynchronous_Select (N);
+                  when N_Assignment_Statement =>
+                     Expand_N_Assignment_Statement (N);
 
-               when N_Attribute_Definition_Clause =>
-                  Expand_N_Attribute_Definition_Clause (N);
+                  when N_Asynchronous_Select =>
+                     Expand_N_Asynchronous_Select (N);
 
-               when N_Attribute_Reference =>
-                  Expand_N_Attribute_Reference (N);
+                  when N_Attribute_Definition_Clause =>
+                     Expand_N_Attribute_Definition_Clause (N);
 
-               when N_Block_Statement =>
-                  Expand_N_Block_Statement (N);
+                  when N_Attribute_Reference =>
+                     Expand_N_Attribute_Reference (N);
 
-               when N_Case_Expression =>
-                  Expand_N_Case_Expression (N);
+                  when N_Block_Statement =>
+                     Expand_N_Block_Statement (N);
 
-               when N_Case_Statement =>
-                  Expand_N_Case_Statement (N);
+                  when N_Case_Expression =>
+                     Expand_N_Case_Expression (N);
 
-               when N_Conditional_Entry_Call =>
-                  Expand_N_Conditional_Entry_Call (N);
+                  when N_Case_Statement =>
+                     Expand_N_Case_Statement (N);
 
-               when N_Conditional_Expression =>
-                  Expand_N_Conditional_Expression (N);
+                  when N_Conditional_Entry_Call =>
+                     Expand_N_Conditional_Entry_Call (N);
 
-               when N_Delay_Relative_Statement =>
-                  Expand_N_Delay_Relative_Statement (N);
+                  when N_Conditional_Expression =>
+                     Expand_N_Conditional_Expression (N);
 
-               when N_Delay_Until_Statement =>
-                  Expand_N_Delay_Until_Statement (N);
+                  when N_Delay_Relative_Statement =>
+                     Expand_N_Delay_Relative_Statement (N);
 
-               when N_Entry_Body =>
-                  Expand_N_Entry_Body (N);
+                  when N_Delay_Until_Statement =>
+                     Expand_N_Delay_Until_Statement (N);
 
-               when N_Entry_Call_Statement =>
-                  Expand_N_Entry_Call_Statement (N);
+                  when N_Entry_Body =>
+                     Expand_N_Entry_Body (N);
 
-               when N_Entry_Declaration =>
-                  Expand_N_Entry_Declaration (N);
+                  when N_Entry_Call_Statement =>
+                     Expand_N_Entry_Call_Statement (N);
 
-               when N_Exception_Declaration =>
-                  Expand_N_Exception_Declaration (N);
+                  when N_Entry_Declaration =>
+                     Expand_N_Entry_Declaration (N);
 
-               when N_Exception_Renaming_Declaration =>
-                  Expand_N_Exception_Renaming_Declaration (N);
+                  when N_Exception_Declaration =>
+                     Expand_N_Exception_Declaration (N);
 
-               when N_Exit_Statement =>
-                  Expand_N_Exit_Statement (N);
+                  when N_Exception_Renaming_Declaration =>
+                     Expand_N_Exception_Renaming_Declaration (N);
 
-               when N_Expanded_Name =>
-                  Expand_N_Expanded_Name (N);
+                  when N_Exit_Statement =>
+                     Expand_N_Exit_Statement (N);
 
-               when N_Explicit_Dereference =>
-                  Expand_N_Explicit_Dereference (N);
+                  when N_Expanded_Name =>
+                     Expand_N_Expanded_Name (N);
 
-               when N_Expression_With_Actions =>
-                  Expand_N_Expression_With_Actions (N);
+                  when N_Explicit_Dereference =>
+                     Expand_N_Explicit_Dereference (N);
 
-               when N_Extended_Return_Statement =>
-                  Expand_N_Extended_Return_Statement (N);
+                  when N_Expression_With_Actions =>
+                     Expand_N_Expression_With_Actions (N);
 
-               when N_Extension_Aggregate =>
-                  Expand_N_Extension_Aggregate (N);
+                  when N_Extended_Return_Statement =>
+                     Expand_N_Extended_Return_Statement (N);
 
-               when N_Free_Statement =>
-                  Expand_N_Free_Statement (N);
+                  when N_Extension_Aggregate =>
+                     Expand_N_Extension_Aggregate (N);
 
-               when N_Freeze_Entity =>
-                  Expand_N_Freeze_Entity (N);
+                  when N_Free_Statement =>
+                     Expand_N_Free_Statement (N);
 
-               when N_Full_Type_Declaration =>
-                  Expand_N_Full_Type_Declaration (N);
+                  when N_Freeze_Entity =>
+                     Expand_N_Freeze_Entity (N);
 
-               when N_Function_Call =>
-                  Expand_N_Function_Call (N);
+                  when N_Full_Type_Declaration =>
+                     Expand_N_Full_Type_Declaration (N);
 
-               when N_Generic_Instantiation =>
-                  Expand_N_Generic_Instantiation (N);
+                  when N_Function_Call =>
+                     Expand_N_Function_Call (N);
 
-               when N_Goto_Statement =>
-                  Expand_N_Goto_Statement (N);
+                  when N_Generic_Instantiation =>
+                     Expand_N_Generic_Instantiation (N);
 
-               when N_Handled_Sequence_Of_Statements =>
-                  Expand_N_Handled_Sequence_Of_Statements (N);
+                  when N_Goto_Statement =>
+                     Expand_N_Goto_Statement (N);
 
-               when N_Identifier =>
-                  Expand_N_Identifier (N);
+                  when N_Handled_Sequence_Of_Statements =>
+                     Expand_N_Handled_Sequence_Of_Statements (N);
 
-               when N_Indexed_Component =>
-                  Expand_N_Indexed_Component (N);
+                  when N_Identifier =>
+                     Expand_N_Identifier (N);
 
-               when N_If_Statement =>
-                  Expand_N_If_Statement (N);
+                  when N_Indexed_Component =>
+                     Expand_N_Indexed_Component (N);
 
-               when N_In =>
-                  Expand_N_In (N);
+                  when N_If_Statement =>
+                     Expand_N_If_Statement (N);
 
-               when N_Loop_Statement =>
-                  Expand_N_Loop_Statement (N);
+                  when N_In =>
+                     Expand_N_In (N);
 
-               when N_Not_In =>
-                  Expand_N_Not_In (N);
+                  when N_Loop_Statement =>
+                     Expand_N_Loop_Statement (N);
 
-               when N_Null =>
-                  Expand_N_Null (N);
+                  when N_Not_In =>
+                     Expand_N_Not_In (N);
 
-               when N_Object_Declaration =>
-                  Expand_N_Object_Declaration (N);
+                  when N_Null =>
+                     Expand_N_Null (N);
 
-               when N_Object_Renaming_Declaration =>
-                  Expand_N_Object_Renaming_Declaration (N);
+                  when N_Object_Declaration =>
+                     Expand_N_Object_Declaration (N);
 
-               when N_Op_Add =>
-                  Expand_N_Op_Add (N);
+                  when N_Object_Renaming_Declaration =>
+                     Expand_N_Object_Renaming_Declaration (N);
 
-               when N_Op_Abs =>
-                  Expand_N_Op_Abs (N);
+                  when N_Op_Add =>
+                     Expand_N_Op_Add (N);
 
-               when N_Op_And =>
-                  Expand_N_Op_And (N);
+                  when N_Op_Abs =>
+                     Expand_N_Op_Abs (N);
 
-               when N_Op_Concat =>
-                  Expand_N_Op_Concat (N);
+                  when N_Op_And =>
+                     Expand_N_Op_And (N);
 
-               when N_Op_Divide =>
-                  Expand_N_Op_Divide (N);
+                  when N_Op_Concat =>
+                     Expand_N_Op_Concat (N);
 
-               when N_Op_Eq =>
-                  Expand_N_Op_Eq (N);
+                  when N_Op_Divide =>
+                     Expand_N_Op_Divide (N);
 
-               when N_Op_Expon =>
-                  Expand_N_Op_Expon (N);
+                  when N_Op_Eq =>
+                     Expand_N_Op_Eq (N);
 
-               when N_Op_Ge =>
-                  Expand_N_Op_Ge (N);
+                  when N_Op_Expon =>
+                     Expand_N_Op_Expon (N);
 
-               when N_Op_Gt =>
-                  Expand_N_Op_Gt (N);
+                  when N_Op_Ge =>
+                     Expand_N_Op_Ge (N);
 
-               when N_Op_Le =>
-                  Expand_N_Op_Le (N);
+                  when N_Op_Gt =>
+                     Expand_N_Op_Gt (N);
 
-               when N_Op_Lt =>
-                  Expand_N_Op_Lt (N);
+                  when N_Op_Le =>
+                     Expand_N_Op_Le (N);
 
-               when N_Op_Minus =>
-                  Expand_N_Op_Minus (N);
+                  when N_Op_Lt =>
+                     Expand_N_Op_Lt (N);
 
-               when N_Op_Mod =>
-                  Expand_N_Op_Mod (N);
+                  when N_Op_Minus =>
+                     Expand_N_Op_Minus (N);
 
-               when N_Op_Multiply =>
-                  Expand_N_Op_Multiply (N);
+                  when N_Op_Mod =>
+                     Expand_N_Op_Mod (N);
 
-               when N_Op_Ne =>
-                  Expand_N_Op_Ne (N);
+                  when N_Op_Multiply =>
+                     Expand_N_Op_Multiply (N);
 
-               when N_Op_Not =>
-                  Expand_N_Op_Not (N);
+                  when N_Op_Ne =>
+                     Expand_N_Op_Ne (N);
 
-               when N_Op_Or =>
-                  Expand_N_Op_Or (N);
+                  when N_Op_Not =>
+                     Expand_N_Op_Not (N);
 
-               when N_Op_Plus =>
-                  Expand_N_Op_Plus (N);
+                  when N_Op_Or =>
+                     Expand_N_Op_Or (N);
 
-               when N_Op_Rem =>
-                  Expand_N_Op_Rem (N);
+                  when N_Op_Plus =>
+                     Expand_N_Op_Plus (N);
 
-               when N_Op_Rotate_Left =>
-                  Expand_N_Op_Rotate_Left (N);
+                  when N_Op_Rem =>
+                     Expand_N_Op_Rem (N);
 
-               when N_Op_Rotate_Right =>
-                  Expand_N_Op_Rotate_Right (N);
+                  when N_Op_Rotate_Left =>
+                     Expand_N_Op_Rotate_Left (N);
 
-               when N_Op_Shift_Left =>
-                  Expand_N_Op_Shift_Left (N);
+                  when N_Op_Rotate_Right =>
+                     Expand_N_Op_Rotate_Right (N);
 
-               when N_Op_Shift_Right =>
-                  Expand_N_Op_Shift_Right (N);
+                  when N_Op_Shift_Left =>
+                     Expand_N_Op_Shift_Left (N);
 
-               when N_Op_Shift_Right_Arithmetic =>
-                  Expand_N_Op_Shift_Right_Arithmetic (N);
+                  when N_Op_Shift_Right =>
+                     Expand_N_Op_Shift_Right (N);
 
-               when N_Op_Subtract =>
-                  Expand_N_Op_Subtract (N);
+                  when N_Op_Shift_Right_Arithmetic =>
+                     Expand_N_Op_Shift_Right_Arithmetic (N);
 
-               when N_Op_Xor =>
-                  Expand_N_Op_Xor (N);
+                  when N_Op_Subtract =>
+                     Expand_N_Op_Subtract (N);
 
-               when N_Or_Else =>
-                  Expand_N_Or_Else (N);
+                  when N_Op_Xor =>
+                     Expand_N_Op_Xor (N);
 
-               when N_Package_Body =>
-                  Expand_N_Package_Body (N);
+                  when N_Or_Else =>
+                     Expand_N_Or_Else (N);
 
-               when N_Package_Declaration =>
-                  Expand_N_Package_Declaration (N);
+                  when N_Package_Body =>
+                     Expand_N_Package_Body (N);
 
-               when N_Package_Renaming_Declaration =>
-                  Expand_N_Package_Renaming_Declaration (N);
+                  when N_Package_Declaration =>
+                     Expand_N_Package_Declaration (N);
 
-               when N_Subprogram_Renaming_Declaration =>
-                  Expand_N_Subprogram_Renaming_Declaration (N);
+                  when N_Package_Renaming_Declaration =>
+                     Expand_N_Package_Renaming_Declaration (N);
 
-               when N_Pragma =>
-                  Expand_N_Pragma (N);
+                  when N_Subprogram_Renaming_Declaration =>
+                     Expand_N_Subprogram_Renaming_Declaration (N);
 
-               when N_Procedure_Call_Statement =>
-                  Expand_N_Procedure_Call_Statement (N);
+                  when N_Pragma =>
+                     Expand_N_Pragma (N);
 
-               when N_Protected_Type_Declaration =>
-                  Expand_N_Protected_Type_Declaration (N);
+                  when N_Procedure_Call_Statement =>
+                     Expand_N_Procedure_Call_Statement (N);
 
-               when N_Protected_Body =>
-                  Expand_N_Protected_Body (N);
+                  when N_Protected_Type_Declaration =>
+                     Expand_N_Protected_Type_Declaration (N);
 
-               when N_Qualified_Expression =>
-                  Expand_N_Qualified_Expression (N);
+                  when N_Protected_Body =>
+                     Expand_N_Protected_Body (N);
 
-               when N_Quantified_Expression  =>
-                  Expand_N_Quantified_Expression (N);
+                  when N_Qualified_Expression =>
+                     Expand_N_Qualified_Expression (N);
 
-               when N_Raise_Statement =>
-                  Expand_N_Raise_Statement (N);
+                  when N_Quantified_Expression  =>
+                     Expand_N_Quantified_Expression (N);
 
-               when N_Raise_Constraint_Error =>
-                  Expand_N_Raise_Constraint_Error (N);
+                  when N_Raise_Statement =>
+                     Expand_N_Raise_Statement (N);
 
-               when N_Raise_Program_Error =>
-                  Expand_N_Raise_Program_Error (N);
+                  when N_Raise_Constraint_Error =>
+                     Expand_N_Raise_Constraint_Error (N);
 
-               when N_Raise_Storage_Error =>
-                  Expand_N_Raise_Storage_Error (N);
+                  when N_Raise_Program_Error =>
+                     Expand_N_Raise_Program_Error (N);
 
-               when N_Real_Literal =>
-                  Expand_N_Real_Literal (N);
+                  when N_Raise_Storage_Error =>
+                     Expand_N_Raise_Storage_Error (N);
 
-               when N_Record_Representation_Clause =>
-                  Expand_N_Record_Representation_Clause (N);
+                  when N_Real_Literal =>
+                     Expand_N_Real_Literal (N);
 
-               when N_Requeue_Statement =>
-                  Expand_N_Requeue_Statement (N);
+                  when N_Record_Representation_Clause =>
+                     Expand_N_Record_Representation_Clause (N);
 
-               when N_Simple_Return_Statement =>
-                  Expand_N_Simple_Return_Statement (N);
+                  when N_Requeue_Statement =>
+                     Expand_N_Requeue_Statement (N);
 
-               when N_Selected_Component =>
-                  Expand_N_Selected_Component (N);
+                  when N_Simple_Return_Statement =>
+                     Expand_N_Simple_Return_Statement (N);
 
-               when N_Selective_Accept =>
-                  Expand_N_Selective_Accept (N);
+                  when N_Selected_Component =>
+                     Expand_N_Selected_Component (N);
 
-               when N_Single_Task_Declaration =>
-                  Expand_N_Single_Task_Declaration (N);
+                  when N_Selective_Accept =>
+                     Expand_N_Selective_Accept (N);
 
-               when N_Slice =>
-                  Expand_N_Slice (N);
+                  when N_Single_Task_Declaration =>
+                     Expand_N_Single_Task_Declaration (N);
 
-               when N_Subtype_Indication =>
-                  Expand_N_Subtype_Indication (N);
+                  when N_Slice =>
+                     Expand_N_Slice (N);
 
-               when N_Subprogram_Body =>
-                  Expand_N_Subprogram_Body (N);
+                  when N_Subtype_Indication =>
+                     Expand_N_Subtype_Indication (N);
 
-               when N_Subprogram_Body_Stub =>
-                  Expand_N_Subprogram_Body_Stub (N);
+                  when N_Subprogram_Body =>
+                     Expand_N_Subprogram_Body (N);
 
-               when N_Subprogram_Declaration =>
-                  Expand_N_Subprogram_Declaration (N);
+                  when N_Subprogram_Body_Stub =>
+                     Expand_N_Subprogram_Body_Stub (N);
 
-               when N_Subprogram_Info =>
-                  Expand_N_Subprogram_Info (N);
+                  when N_Subprogram_Declaration =>
+                     Expand_N_Subprogram_Declaration (N);
 
-               when N_Task_Body =>
-                  Expand_N_Task_Body (N);
+                  when N_Subprogram_Info =>
+                     Expand_N_Subprogram_Info (N);
 
-               when N_Task_Type_Declaration =>
-                  Expand_N_Task_Type_Declaration (N);
+                  when N_Task_Body =>
+                     Expand_N_Task_Body (N);
 
-               when N_Timed_Entry_Call =>
-                  Expand_N_Timed_Entry_Call (N);
+                  when N_Task_Type_Declaration =>
+                     Expand_N_Task_Type_Declaration (N);
 
-               when N_Type_Conversion =>
-                  Expand_N_Type_Conversion (N);
+                  when N_Timed_Entry_Call =>
+                     Expand_N_Timed_Entry_Call (N);
 
-               when N_Unchecked_Expression =>
-                  Expand_N_Unchecked_Expression (N);
+                  when N_Type_Conversion =>
+                     Expand_N_Type_Conversion (N);
 
-               when N_Unchecked_Type_Conversion =>
-                  Expand_N_Unchecked_Type_Conversion (N);
+                  when N_Unchecked_Expression =>
+                     Expand_N_Unchecked_Expression (N);
 
-               when N_Variant_Part =>
-                  Expand_N_Variant_Part (N);
+                  when N_Unchecked_Type_Conversion =>
+                     Expand_N_Unchecked_Type_Conversion (N);
 
-               --  For all other node kinds, no expansion activity is required
+                  when N_Variant_Part =>
+                     Expand_N_Variant_Part (N);
 
-               when others => null;
+                  --  For all other node kinds, no expansion activity is
+                  --  required.
 
-            end case;
+                  when others => null;
 
+               end case;
+            end if;
+
          exception
             when RE_Not_Available =>
                return;
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 178293)
+++ gnat1drv.adb	(working copy)
@@ -435,8 +435,9 @@ 
 
          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;
 
Index: exp_ch11.adb
===================================================================
--- exp_ch11.adb	(revision 178293)
+++ exp_ch11.adb	(working copy)
@@ -1673,7 +1673,6 @@ 
 
          if VM_Target = No_VM
            and then not CodePeer_Mode
-           and then not ALFA_Mode
            and then Exception_Mechanism = Back_End_Exceptions
          then
             return;
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 178303)
+++ exp_ch6.adb	(working copy)
@@ -156,36 +156,6 @@ 
    --  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
Index: exp_ch6.ads
===================================================================
--- exp_ch6.ads	(revision 178293)
+++ exp_ch6.ads	(working copy)
@@ -37,6 +37,36 @@ 
    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.
Index: exp_attr_light.adb
===================================================================
--- exp_attr_light.adb	(revision 0)
+++ exp_attr_light.adb	(revision 0)
@@ -0,0 +1,49 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_attr_light.ads
===================================================================
--- exp_attr_light.ads	(revision 0)
+++ exp_attr_light.ads	(revision 0)
@@ -0,0 +1,35 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_ch7_light.adb
===================================================================
--- exp_ch7_light.adb	(revision 0)
+++ exp_ch7_light.adb	(revision 0)
@@ -0,0 +1,35 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_ch7_light.ads
===================================================================
--- exp_ch7_light.ads	(revision 0)
+++ exp_ch7_light.ads	(revision 0)
@@ -0,0 +1,35 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_light.adb
===================================================================
--- exp_light.adb	(revision 0)
+++ exp_light.adb	(revision 0)
@@ -0,0 +1,64 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_light.ads
===================================================================
--- exp_light.ads	(revision 0)
+++ exp_light.ads	(revision 0)
@@ -0,0 +1,52 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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;
Index: exp_aggr.adb
===================================================================
--- exp_aggr.adb	(revision 178293)
+++ exp_aggr.adb	(working copy)
@@ -4664,12 +4664,6 @@ 
          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