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 <m...@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
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