X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=gcc%2Fada%2Fsem_ch12.adb;h=3635319884b8def8eb69eb94f90ae7bcb9bb4a18;hb=5e9cb4046164bb8debe8b3c07c00158b7319739a;hp=8533af0ecc7c493c075cad28b83cee273f2c117c;hpb=0640c7d139ea91870c378de96cab14d708517593;p=gcc.git diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 8533af0ecc7..3635319884b 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -1074,7 +1074,7 @@ package body Sem_Ch12 is F_Copy : List_Id) return List_Id is Actuals_To_Freeze : constant Elist_Id := New_Elmt_List; - Assoc : constant List_Id := New_List; + Assoc_List : constant List_Id := New_List; Default_Actuals : constant List_Id := New_List; Gen_Unit : constant Entity_Id := Defining_Entity (Parent (F_Copy)); @@ -1204,6 +1204,7 @@ package body Sem_Ch12 is Prims : constant Elist_Id := Collect_Primitive_Operations (Typ); Elem : Elmt_Id; Formal : Node_Id; + Op : Entity_Id; begin -- Locate primitive operations of the type that are arithmetic @@ -1218,12 +1219,54 @@ package body Sem_Ch12 is -- to justify a warning. Formal := First_Non_Pragma (Formals); + Op := Alias (Node (Elem)); + while Present (Formal) loop if Nkind (Formal) = N_Formal_Concrete_Subprogram_Declaration and then Chars (Defining_Entity (Formal)) = Chars (Node (Elem)) then exit; + + elsif Nkind (Formal) = N_Formal_Package_Declaration then + declare + Assoc : Node_Id; + Ent : Entity_Id; + + begin + -- Locate corresponding actual, and check whether it + -- includes a fixed-point type. + + Assoc := First (Assoc_List); + while Present (Assoc) loop + exit when + Nkind (Assoc) = N_Package_Renaming_Declaration + and then Chars (Defining_Unit_Name (Assoc)) = + Chars (Defining_Identifier (Formal)); + + Next (Assoc); + end loop; + + if Present (Assoc) then + + -- If formal package declares a fixed-point type, + -- and the user-defined operator is derived from + -- a generic instance package, the fixed-point type + -- does not use the corresponding predefined op. + + Ent := First_Entity (Entity (Name (Assoc))); + while Present (Ent) loop + if Is_Fixed_Point_Type (Ent) + and then Present (Op) + and then Is_Generic_Instance (Scope (Op)) + then + return; + end if; + + Next_Entity (Ent); + end loop; + end if; + end; end if; Next (Formal); @@ -1414,7 +1457,7 @@ package body Sem_Ch12 is Set_Defining_Identifier (Decl, Id); end if; - Append (Decl, Assoc); + Append (Decl, Assoc_List); if No (Found_Assoc) then Default := @@ -1459,7 +1502,6 @@ package body Sem_Ch12 is Kind := Nkind (Analyzed_Formal); case Nkind (Formal) is - when N_Formal_Subprogram_Declaration => exit when Kind in N_Formal_Subprogram_Declaration and then @@ -1473,7 +1515,10 @@ package body Sem_Ch12 is N_Generic_Package_Declaration, N_Package_Declaration); - when N_Use_Package_Clause | N_Use_Type_Clause => exit; + when N_Use_Package_Clause + | N_Use_Type_Clause + => + exit; when others => @@ -1608,7 +1653,7 @@ package body Sem_Ch12 is else Append_List (Instantiate_Object (Formal, Match, Analyzed_Formal), - Assoc); + Assoc_List); -- For a defaulted in_parameter, create an entry in the -- the list of defaulted actuals, for GNATProve use. Do @@ -1665,8 +1710,8 @@ package body Sem_Ch12 is Analyze (Match); Append_List (Instantiate_Type - (Formal, Match, Analyzed_Formal, Assoc), - Assoc); + (Formal, Match, Analyzed_Formal, Assoc_List), + Assoc_List); if Is_Fixed_Point_Type (Entity (Match)) then Check_Fixed_Point_Actual (Match); @@ -1765,7 +1810,7 @@ package body Sem_Ch12 is end if; else - Append_To (Assoc, + Append_To (Assoc_List, Instantiate_Formal_Subprogram (Formal, Match, Analyzed_Formal)); @@ -1808,7 +1853,8 @@ package body Sem_Ch12 is if No (Match) and then Box_Present (Formal) then declare Subp : constant Entity_Id := - Defining_Unit_Name (Specification (Last (Assoc))); + Defining_Unit_Name + (Specification (Last (Assoc_List))); begin Append_To (Default_Actuals, @@ -1847,7 +1893,61 @@ package body Sem_Ch12 is Append_List (Instantiate_Formal_Package (Formal, Match, Analyzed_Formal), - Assoc); + Assoc_List); + + -- Determine whether the actual package needs an explicit + -- freeze node. This is only the case if the actual is + -- declared in the same unit and has a body. Normally + -- packages do not have explicit freeze nodes, and gigi + -- only uses them to elaborate entities in a package + -- body. + + declare + Actual : constant Entity_Id := Entity (Match); + + Needs_Freezing : Boolean; + S : Entity_Id; + + begin + if not Expander_Active + or else not Has_Completion (Actual) + or else not In_Same_Source_Unit (I_Node, Actual) + or else + (Present (Renamed_Entity (Actual)) + and then not + In_Same_Source_Unit + (I_Node, (Renamed_Entity (Actual)))) + then + null; + + else + -- Finally we want to exclude such freeze nodes + -- from statement sequences, which freeze + -- everything before them. + -- Is this strictly necessary ??? + + Needs_Freezing := True; + + S := Current_Scope; + while Present (S) loop + if Ekind_In (S, E_Block, + E_Function, + E_Loop, + E_Procedure) + then + Needs_Freezing := False; + exit; + end if; + + S := Scope (S); + end loop; + + if Needs_Freezing then + Set_Has_Delayed_Freeze (Actual); + Append_Elmt (Actual, Actuals_To_Freeze); + end if; + end if; + end; end if; -- For use type and use package appearing in the generic part, @@ -1855,20 +1955,20 @@ package body Sem_Ch12 is -- they belong (we mustn't recopy them since this would mess up -- the Sloc values). - when N_Use_Package_Clause | - N_Use_Type_Clause => + when N_Use_Package_Clause + | N_Use_Type_Clause + => if Nkind (Original_Node (I_Node)) = N_Formal_Package_Declaration then - Append (New_Copy_Tree (Formal), Assoc); + Append (New_Copy_Tree (Formal), Assoc_List); else Remove (Formal); - Append (Formal, Assoc); + Append (Formal, Assoc_List); end if; when others => raise Program_Error; - end case; Formal := Saved_Formal; @@ -1939,7 +2039,7 @@ package body Sem_Ch12 is Append_List (Default_Formals, Formals); end if; - return Assoc; + return Assoc_List; end Analyze_Associations; ------------------------------- @@ -2555,7 +2655,9 @@ package body Sem_Ch12 is (Generic_Formal_Declarations (Original_Node (Gen_Decl))); while Present (Formal_Decl) loop Append_To - (Decls, Copy_Generic_Node (Formal_Decl, Empty, True)); + (Decls, + Copy_Generic_Node + (Formal_Decl, Empty, Instantiating => True)); Next (Formal_Decl); end loop; end; @@ -2603,8 +2705,8 @@ package body Sem_Ch12 is -- Local variables - Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; - -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit + Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; + -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit Associations : Boolean := True; New_N : Node_Id; @@ -2656,13 +2758,13 @@ package body Sem_Ch12 is -- continue analysis to minimize cascaded errors. Error_Msg_N - ("generic parent cannot be used as formal package " - & "of a child unit", Gen_Id); + ("generic parent cannot be used as formal package of a child " + & "unit", Gen_Id); else Error_Msg_N - ("generic package cannot be used as a formal package " - & "within itself", Gen_Id); + ("generic package cannot be used as a formal package within " + & "itself", Gen_Id); Restore_Env; goto Leave; end if; @@ -2780,7 +2882,12 @@ package body Sem_Ch12 is -- all SPARK_Mode pragmas within the generic_package_name. if SPARK_Mode /= On then - Ignore_Pragma_SPARK_Mode := True; + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + + -- Mark the formal spec in case the body is instantiated at a later + -- pass. This preserves the original context in effect for the body. + + Set_Ignore_SPARK_Mode_Pragmas (Formal); end if; Analyze (Specification (N)); @@ -2841,7 +2948,7 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Pack_Id); end if; - Ignore_Pragma_SPARK_Mode := Save_IPSM; + Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; end Analyze_Formal_Package_Declaration; --------------------------------- @@ -3135,56 +3242,56 @@ package body Sem_Ch12 is -- Enter the new name, and branch to specific routine case Nkind (Def) is - when N_Formal_Private_Type_Definition => + when N_Formal_Private_Type_Definition => Analyze_Formal_Private_Type (N, T, Def); - when N_Formal_Derived_Type_Definition => + when N_Formal_Derived_Type_Definition => Analyze_Formal_Derived_Type (N, T, Def); - when N_Formal_Incomplete_Type_Definition => + when N_Formal_Incomplete_Type_Definition => Analyze_Formal_Incomplete_Type (T, Def); - when N_Formal_Discrete_Type_Definition => + when N_Formal_Discrete_Type_Definition => Analyze_Formal_Discrete_Type (T, Def); - when N_Formal_Signed_Integer_Type_Definition => + when N_Formal_Signed_Integer_Type_Definition => Analyze_Formal_Signed_Integer_Type (T, Def); - when N_Formal_Modular_Type_Definition => + when N_Formal_Modular_Type_Definition => Analyze_Formal_Modular_Type (T, Def); - when N_Formal_Floating_Point_Definition => + when N_Formal_Floating_Point_Definition => Analyze_Formal_Floating_Type (T, Def); when N_Formal_Ordinary_Fixed_Point_Definition => Analyze_Formal_Ordinary_Fixed_Point_Type (T, Def); - when N_Formal_Decimal_Fixed_Point_Definition => + when N_Formal_Decimal_Fixed_Point_Definition => Analyze_Formal_Decimal_Fixed_Point_Type (T, Def); when N_Array_Type_Definition => Analyze_Formal_Array_Type (T, Def); - when N_Access_To_Object_Definition | - N_Access_Function_Definition | - N_Access_Procedure_Definition => + when N_Access_Function_Definition + | N_Access_Procedure_Definition + | N_Access_To_Object_Definition + => Analyze_Generic_Access_Type (T, Def); -- Ada 2005: a interface declaration is encoded as an abstract -- record declaration or a abstract type derivation. - when N_Record_Definition => + when N_Record_Definition => Analyze_Formal_Interface_Type (N, T, Def); - when N_Derived_Type_Definition => + when N_Derived_Type_Definition => Analyze_Formal_Derived_Interface_Type (N, T, Def); - when N_Error => + when N_Error => null; - when others => + when others => raise Program_Error; - end case; Set_Is_Generic_Type (T); @@ -3331,12 +3438,12 @@ package body Sem_Ch12 is Set_Ekind (Id, E_Generic_Package); Set_Etype (Id, Standard_Void_Type); - -- A generic package declared within a Ghost region is rendered Ghost - -- (SPARK RM 6.9(2)). + -- Set SPARK_Mode from context - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; + Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Id); + Set_SPARK_Aux_Pragma_Inherited (Id); -- Analyze aspects now, so that generated pragmas appear in the -- declarations before building and analyzing the generic copy. @@ -3379,6 +3486,14 @@ package body Sem_Ch12 is End_Package_Scope (Id); Exit_Generic_Scope (Id); + -- If the generic appears within a package unit, the body of that unit + -- has to be present for instantiation and inlining. + + if Nkind (Unit (Cunit (Current_Sem_Unit))) = N_Package_Declaration then + Set_Body_Needed_For_Inlining + (Defining_Entity (Unit (Cunit (Current_Sem_Unit)))); + end if; + if Nkind (Parent (N)) /= N_Compilation_Unit then Move_Freeze_Nodes (Id, N, Visible_Declarations (Specification (N))); Move_Freeze_Nodes (Id, N, Private_Declarations (Specification (N))); @@ -3548,13 +3663,6 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); end if; - -- A generic subprogram declared within a Ghost region is rendered Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - -- For a library unit, we have reconstructed the entity for the unit, -- and must reset it in the library tables. We also make sure that -- Body_Required is set properly in the original compilation unit node. @@ -3564,6 +3672,16 @@ package body Sem_Ch12 is Set_Body_Required (Parent (N), Unit_Requires_Body (Id)); end if; + -- If the generic appears within a package unit, the body of that unit + -- has to be present for instantiation and inlining. + + if Nkind (Unit (Cunit (Current_Sem_Unit))) = N_Package_Declaration + and then Unit_Requires_Body (Id) + then + Set_Body_Needed_For_Inlining + (Defining_Entity (Unit (Cunit (Current_Sem_Unit)))); + end if; + Set_Categorization_From_Pragmas (N); Validate_Categorization_Dependency (N, Id); @@ -3587,45 +3705,17 @@ package body Sem_Ch12 is -- Analyze_Package_Instantiation -- ----------------------------------- - procedure Analyze_Package_Instantiation (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Gen_Id : constant Node_Id := Name (N); - - Act_Decl : Node_Id; - Act_Decl_Name : Node_Id; - Act_Decl_Id : Entity_Id; - Act_Spec : Node_Id; - Act_Tree : Node_Id; - - Gen_Decl : Node_Id; - Gen_Spec : Node_Id; - Gen_Unit : Entity_Id; - - Is_Actual_Pack : constant Boolean := - Is_Internal (Defining_Entity (N)); + -- WARNING: This routine manages Ghost and SPARK regions. Return statements + -- must be replaced by gotos which jump to the end of the routine in order + -- to restore the Ghost and SPARK modes. - Env_Installed : Boolean := False; - Parent_Installed : Boolean := False; - Renaming_List : List_Id; - Unit_Renaming : Node_Id; - Needs_Body : Boolean; - Inline_Now : Boolean := False; + procedure Analyze_Package_Instantiation (N : Node_Id) is Has_Inline_Always : Boolean := False; - Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; - -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit - - Save_SM : constant SPARK_Mode_Type := SPARK_Mode; - Save_SMP : constant Node_Id := SPARK_Mode_Pragma; - -- Save the SPARK_Mode-related data for restore on exit - - Save_Style_Check : constant Boolean := Style_Check; - -- Save style check mode for restore on exit - procedure Delay_Descriptors (E : Entity_Id); -- Delay generation of subprogram descriptors for given entity - function Might_Inline_Subp return Boolean; + function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean; -- If inlining is active and the generic contains inlined subprograms, -- we instantiate the body. This may cause superfluous instantiations, -- but it is simpler than detecting the need for the body at the point @@ -3647,7 +3737,7 @@ package body Sem_Ch12 is -- Might_Inline_Subp -- ----------------------- - function Might_Inline_Subp return Boolean is + function Might_Inline_Subp (Gen_Unit : Entity_Id) return Boolean is E : Entity_Id; begin @@ -3676,6 +3766,36 @@ package body Sem_Ch12 is -- Local declarations + Gen_Id : constant Node_Id := Name (N); + Is_Actual_Pack : constant Boolean := + Is_Internal (Defining_Entity (N)); + Loc : constant Source_Ptr := Sloc (N); + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the Ghost and SPARK mode-related data to restore on exit + + Saved_Style_Check : constant Boolean := Style_Check; + -- Save style check mode for restore on exit + + Act_Decl : Node_Id; + Act_Decl_Name : Node_Id; + Act_Decl_Id : Entity_Id; + Act_Spec : Node_Id; + Act_Tree : Node_Id; + Env_Installed : Boolean := False; + Gen_Decl : Node_Id; + Gen_Spec : Node_Id; + Gen_Unit : Entity_Id; + Inline_Now : Boolean := False; + Needs_Body : Boolean; + Parent_Installed : Boolean := False; + Renaming_List : List_Id; + Unit_Renaming : Node_Id; + Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation -- to match the visibility of the formal type @@ -3694,12 +3814,6 @@ package body Sem_Ch12 is Instantiation_Node := N; - -- Turn off style checking in instances. If the check is enabled on the - -- generic unit, a warning in an instance would just be noise. If not - -- enabled on the generic, then a warning in an instance is just wrong. - - Style_Check := False; - -- Case of instantiation of a generic package if Nkind (N) = N_Package_Instantiation then @@ -3732,6 +3846,14 @@ package body Sem_Ch12 is Preanalyze_Actuals (N, Act_Decl_Id); + -- Turn off style checking in instances. If the check is enabled on the + -- generic unit, a warning in an instance would just be noise. If not + -- enabled on the generic, then a warning in an instance is just wrong. + -- This must be done after analyzing the actuals, which do come from + -- source and are subject to style checking. + + Style_Check := False; + Init_Env; Env_Installed := True; @@ -3746,6 +3868,13 @@ package body Sem_Ch12 is Check_Generic_Child_Unit (Gen_Id, Parent_Installed); Gen_Unit := Entity (Gen_Id); + -- A package instantiation is Ghost when it is subject to pragma Ghost + -- or the generic template is Ghost. Set the mode now to ensure that + -- any nodes generated during analysis and expansion are marked as + -- Ghost. + + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit); + -- Verify that it is the name of a generic package -- A visibility glitch: if the instance is a child unit and the generic @@ -3842,7 +3971,13 @@ package body Sem_Ch12 is -- the instance. if SPARK_Mode /= On then - Ignore_Pragma_SPARK_Mode := True; + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + + -- Mark the instance spec in case the body is instantiated at a + -- later pass. This preserves the original context in effect for + -- the body. + + Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id); end if; Gen_Decl := Unit_Declaration_Node (Gen_Unit); @@ -4015,7 +4150,7 @@ package body Sem_Ch12 is if Expander_Active and then (not Is_Child_Unit (Gen_Unit) or else not Is_Generic_Unit (Scope (Gen_Unit))) - and then Might_Inline_Subp + and then Might_Inline_Subp (Gen_Unit) and then not Is_Actual_Pack then if not Back_End_Inlining @@ -4030,8 +4165,7 @@ package body Sem_Ch12 is -- predefined subprograms marked Inline_Always, to minimize -- the use of the run-time library. - elsif Is_Predefined_File_Name - (Unit_File_Name (Get_Source_Unit (Gen_Decl))) + elsif In_Predefined_Unit (Gen_Decl) and then Configurable_Run_Time_Mode and then Nkind (Parent (N)) /= N_Compilation_Unit then @@ -4064,7 +4198,8 @@ package body Sem_Ch12 is (Unit_Requires_Body (Gen_Unit) or else Enclosing_Body_Present or else Present (Corresponding_Body (Gen_Decl))) - and then (Is_In_Main_Unit (N) or else Might_Inline_Subp) + and then (Is_In_Main_Unit (N) + or else Might_Inline_Subp (Gen_Unit)) and then not Is_Actual_Pack and then not Inline_Now and then (Operating_Mode = Generate_Code @@ -4410,11 +4545,6 @@ package body Sem_Ch12 is Set_Defining_Identifier (N, Act_Decl_Id); end if; - Ignore_Pragma_SPARK_Mode := Save_IPSM; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - Style_Check := Save_Style_Check; - -- Check that if N is an instantiation of System.Dim_Float_IO or -- System.Dim_Integer_IO, the formal type has a dimension system. @@ -4437,6 +4567,11 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Style_Check := Saved_Style_Check; + exception when Instantiation_Error => if Parent_Installed then @@ -4447,16 +4582,20 @@ package body Sem_Ch12 is Restore_Env; end if; - Ignore_Pragma_SPARK_Mode := Save_IPSM; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - Style_Check := Save_Style_Check; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Style_Check := Saved_Style_Check; end Analyze_Package_Instantiation; -------------------------- -- Inline_Instance_Body -- -------------------------- + -- WARNING: This routine manages SPARK regions. Return statements must be + -- replaced by gotos which jump to the end of the routine and restore the + -- SPARK mode. + procedure Inline_Instance_Body (N : Node_Id; Gen_Unit : Entity_Id; @@ -4467,26 +4606,27 @@ package body Sem_Ch12 is Gen_Comp : constant Entity_Id := Cunit_Entity (Get_Source_Unit (Gen_Unit)); - Save_SM : constant SPARK_Mode_Type := SPARK_Mode; - Save_SMP : constant Node_Id := SPARK_Mode_Pragma; - -- Save all SPARK_Mode-related attributes as removing enclosing scopes - -- to provide a clean environment for analysis of the inlined body will - -- eliminate any previously set SPARK_Mode. + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the SPARK mode-related data to restore on exit. Removing + -- enclosing scopes to provide a clean environment for analysis of + -- the inlined body will eliminate any previously set SPARK_Mode. Scope_Stack_Depth : constant Pos := Scope_Stack.Last - Scope_Stack.First + 1; - Use_Clauses : array (1 .. Scope_Stack_Depth) of Node_Id; - Instances : array (1 .. Scope_Stack_Depth) of Entity_Id; Inner_Scopes : array (1 .. Scope_Stack_Depth) of Entity_Id; - Curr_Scope : Entity_Id := Empty; - List : Elist_Id; - Num_Inner : Nat := 0; - Num_Scopes : Nat := 0; - N_Instances : Nat := 0; - Removed : Boolean := False; - S : Entity_Id; - Vis : Boolean; + Instances : array (1 .. Scope_Stack_Depth) of Entity_Id; + Use_Clauses : array (1 .. Scope_Stack_Depth) of Node_Id; + + Curr_Scope : Entity_Id := Empty; + List : Elist_Id; + N_Instances : Nat := 0; + Num_Inner : Nat := 0; + Num_Scopes : Nat := 0; + Removed : Boolean := False; + S : Entity_Id; + Vis : Boolean; begin -- Case of generic unit defined in another unit. We must remove the @@ -4630,8 +4770,8 @@ package body Sem_Ch12 is Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, Warnings => Save_Warnings, - SPARK_Mode => Save_SM, - SPARK_Mode_Pragma => Save_SMP)), + SPARK_Mode => Saved_SM, + SPARK_Mode_Pragma => Saved_SMP)), Inlined_Body => True); Pop_Scope; @@ -4770,7 +4910,6 @@ package body Sem_Ch12 is (N : Node_Id; Subp : Entity_Id) return Boolean is - function Is_Inlined_Or_Child_Of_Inlined (E : Entity_Id) return Boolean; -- Return True if E is an inlined subprogram, an inlined renaming or a -- subprogram nested in an inlined subprogram. The inlining machinery @@ -4840,6 +4979,10 @@ package body Sem_Ch12 is -- Analyze_Subprogram_Instantiation -- -------------------------------------- + -- WARNING: This routine manages Ghost and SPARK regions. Return statements + -- must be replaced by gotos which jump to the end of the routine in order + -- to restore the Ghost and SPARK modes. + procedure Analyze_Subprogram_Instantiation (N : Node_Id; K : Entity_Kind) @@ -5084,12 +5227,12 @@ package body Sem_Ch12 is -- Local variables - Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; - -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit - - Save_SM : constant SPARK_Mode_Type := SPARK_Mode; - Save_SMP : constant Node_Id := SPARK_Mode_Pragma; - -- Save the SPARK_Mode-related data for restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the Ghost and SPARK mode-related data to restore on exit Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation @@ -5126,6 +5269,13 @@ package body Sem_Ch12 is Check_Generic_Child_Unit (Gen_Id, Parent_Installed); Gen_Unit := Entity (Gen_Id); + -- A subprogram instantiation is Ghost when it is subject to pragma + -- Ghost or the generic template is Ghost. Set the mode now to ensure + -- that any nodes generated during analysis and expansion are marked as + -- Ghost. + + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit); + Generate_Reference (Gen_Unit, Gen_Id); if Nkind (Gen_Id) = N_Identifier @@ -5137,7 +5287,7 @@ package body Sem_Ch12 is if Etype (Gen_Unit) = Any_Type then Restore_Env; - return; + goto Leave; end if; -- Verify that it is a generic subprogram of the right kind, and that @@ -5155,15 +5305,6 @@ package body Sem_Ch12 is Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit); else - -- If the context of the instance is subject to SPARK_Mode "off" or - -- the annotation is altogether missing, set the global flag which - -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within - -- the instance. - - if SPARK_Mode /= On then - Ignore_Pragma_SPARK_Mode := True; - end if; - Set_Entity (Gen_Id, Gen_Unit); Set_Is_Instantiated (Gen_Unit); @@ -5297,11 +5438,36 @@ package body Sem_Ch12 is Set_Has_Pragma_Inline (Act_Decl_Id, Has_Pragma_Inline (Gen_Unit)); Set_Has_Pragma_Inline (Anon_Id, Has_Pragma_Inline (Gen_Unit)); + -- Propagate No_Return if pragma applied to generic unit. This must + -- be done explicitly because pragma does not appear in generic + -- declaration (unlike the aspect case). + + if No_Return (Gen_Unit) then + Set_No_Return (Act_Decl_Id); + Set_No_Return (Anon_Id); + end if; + Set_Has_Pragma_Inline_Always (Act_Decl_Id, Has_Pragma_Inline_Always (Gen_Unit)); Set_Has_Pragma_Inline_Always (Anon_Id, Has_Pragma_Inline_Always (Gen_Unit)); + -- If the context of the instance is subject to SPARK_Mode "off" or + -- the annotation is altogether missing, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within + -- the instance. + + if SPARK_Mode /= On then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + + -- Mark both the instance spec and the anonymous package in case + -- the body is instantiated at a later pass. This preserves the + -- original context in effect for the body. + + Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id); + Set_Ignore_SPARK_Mode_Pragmas (Anon_Id); + end if; + if not Is_Intrinsic_Subprogram (Gen_Unit) then Check_Elab_Instantiation (N); end if; @@ -5322,8 +5488,8 @@ package body Sem_Ch12 is Error_Msg_NE ("access parameter& is controlling,", N, Formal); Error_Msg_NE - ("\corresponding parameter of & must be " - & "explicitly null-excluding", N, Gen_Id); + ("\corresponding parameter of & must be explicitly " + & "null-excluding", N, Gen_Id); end if; Next_Formal (Formal); @@ -5375,10 +5541,6 @@ package body Sem_Ch12 is Env_Installed := False; Generic_Renamings.Set_Last (0); Generic_Renamings_HTable.Reset; - - Ignore_Pragma_SPARK_Mode := Save_IPSM; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; end if; <> @@ -5386,6 +5548,10 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + exception when Instantiation_Error => if Parent_Installed then @@ -5396,9 +5562,9 @@ package body Sem_Ch12 is Restore_Env; end if; - Ignore_Pragma_SPARK_Mode := Save_IPSM; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Subprogram_Instantiation; ------------------------- @@ -5429,7 +5595,7 @@ package body Sem_Ch12 is Assoc := Associated_Node (Assoc); end loop; - -- Follow and additional link in case the final node was rewritten. + -- Follow an additional link in case the final node was rewritten. -- This can only happen with nested generic units. if (Nkind (Assoc) = N_Identifier or else Nkind (Assoc) in N_Op) @@ -5446,7 +5612,7 @@ package body Sem_Ch12 is -- An additional special case: an unconstrained type in an object -- declaration may have been rewritten as a local subtype constrained -- by the expression in the declaration. We need to recover the - -- original entity which may be global. + -- original entity, which may be global. if Present (Original_Node (Assoc)) and then Nkind (Parent (N)) = N_Object_Declaration @@ -5551,6 +5717,7 @@ package body Sem_Ch12 is Decl : Node_Id; Expr : Node_Id; + pragma Warnings (Off, Expr); F1, F2 : Entity_Id; Func : Entity_Id; Op_Name : Name_Id; @@ -5787,8 +5954,9 @@ package body Sem_Ch12 is (Formal_Pack : Entity_Id; Actual_Pack : Entity_Id) is - E1 : Entity_Id := First_Entity (Actual_Pack); - E2 : Entity_Id := First_Entity (Formal_Pack); + E1 : Entity_Id := First_Entity (Actual_Pack); + E2 : Entity_Id := First_Entity (Formal_Pack); + Prev_E1 : Entity_Id; Expr1 : Node_Id; Expr2 : Node_Id; @@ -5954,6 +6122,7 @@ package body Sem_Ch12 is -- Start of processing for Check_Formal_Package_Instance begin + Prev_E1 := E1; while Present (E1) and then Present (E2) loop exit when Ekind (E1) = E_Package and then Renamed_Entity (E1) = Renamed_Entity (Actual_Pack); @@ -5983,6 +6152,14 @@ package body Sem_Ch12 is if No (E1) then return; + -- Entities may be declared without full declaration, such as + -- itypes and predefined operators (concatenation for arrays, eg). + -- Skip it and keep the formal entity to find a later match for it. + + elsif No (Parent (E2)) and then Ekind (E1) /= Ekind (E2) then + E1 := Prev_E1; + goto Next_E; + -- If the formal entity comes from a formal declaration, it was -- defaulted in the formal package, and no check is needed on it. @@ -5990,6 +6167,13 @@ package body Sem_Ch12 is N_Formal_Object_Declaration, N_Formal_Type_Declaration) then + -- If the formal is a tagged type the corresponding class-wide + -- type has been generated as well, and it must be skipped. + + if Is_Type (E2) and then Is_Tagged_Type (E2) then + Next_Entity (E2); + end if; + goto Next_E; -- Ditto for defaulted formal subprograms. @@ -6144,6 +6328,7 @@ package body Sem_Ch12 is end if; <> + Prev_E1 := E1; Next_Entity (E1); Next_Entity (E2); end loop; @@ -6320,8 +6505,7 @@ package body Sem_Ch12 is Set_Is_Generic_Actual_Type (E, True); Set_Is_Hidden (E, False); - Set_Is_Potentially_Use_Visible (E, - In_Use (Instance)); + Set_Is_Potentially_Use_Visible (E, In_Use (Instance)); -- We constructed the generic actual type as a subtype of the -- supplied type. This means that it normally would not inherit @@ -7275,7 +7459,16 @@ package body Sem_Ch12 is (New_N, Copy_Generic_List (Aspect_Specifications (N), Parent_Id)); end if; - if Instantiating then + -- If we are instantiating, we want to adjust the sloc based on the + -- current S_Adjustment. However, if this is the root node of a subunit, + -- we need to defer that adjustment to below (see "elsif Instantiating + -- and Was_Stub"), so it comes after Create_Instantiation_Source has + -- computed the adjustment. + + if Instantiating + and then not (Nkind (N) in N_Proper_Body + and then Was_Originally_Stub (N)) + then Adjust_Instantiation_Sloc (New_N, S_Adjustment); end if; @@ -7419,18 +7612,16 @@ package body Sem_Ch12 is Set_Selector_Name (New_N, Copy_Generic_Node (Selector_Name (N), New_N, Instantiating)); - -- For operators, we must copy the right operand + -- For operators, copy the operands elsif Nkind (N) in N_Op then - Set_Right_Opnd (New_N, - Copy_Generic_Node (Right_Opnd (N), New_N, Instantiating)); - - -- And for binary operators, the left operand as well - if Nkind (N) in N_Binary_Op then Set_Left_Opnd (New_N, Copy_Generic_Node (Left_Opnd (N), New_N, Instantiating)); end if; + + Set_Right_Opnd (New_N, + Copy_Generic_Node (Right_Opnd (N), New_N, Instantiating)); end if; -- Establish a link between an entity from the generic template and the @@ -7576,14 +7767,16 @@ package body Sem_Ch12 is Copy_Generic_List (Context_Items (N), New_N)); Set_Unit (New_N, - Copy_Generic_Node (Unit (N), New_N, False)); + Copy_Generic_Node (Unit (N), New_N, Instantiating => False)); Set_First_Inlined_Subprogram (New_N, Copy_Generic_Node - (First_Inlined_Subprogram (N), New_N, False)); + (First_Inlined_Subprogram (N), New_N, Instantiating => False)); - Set_Aux_Decls_Node (New_N, - Copy_Generic_Node (Aux_Decls_Node (N), New_N, False)); + Set_Aux_Decls_Node + (New_N, + Copy_Generic_Node + (Aux_Decls_Node (N), New_N, Instantiating => False)); -- For an assignment node, the assignment is known to be semantically -- legal if we are instantiating the template. This avoids incorrect @@ -7698,13 +7891,14 @@ package body Sem_Ch12 is elsif Nkind (N) in N_Proper_Body then declare Save_Adjustment : constant Sloc_Adjustment := S_Adjustment; - begin if Instantiating and then Was_Originally_Stub (N) then Create_Instantiation_Source (Instantiation_Node, Defining_Entity (N), S_Adjustment); + + Adjust_Instantiation_Sloc (New_N, S_Adjustment); end if; -- Now copy the fields of the proper body, using the new @@ -7712,7 +7906,7 @@ package body Sem_Ch12 is Copy_Descendants; - -- Restore the original adjustment factor in case changed + -- Restore the original adjustment factor S_Adjustment := Save_Adjustment; end; @@ -7722,7 +7916,7 @@ package body Sem_Ch12 is -- Do not copy Comment or Ident pragmas their content is relevant to -- the generic unit, not to the instantiating unit. - if Nam_In (Pragma_Name (N), Name_Comment, Name_Ident) then + if Nam_In (Pragma_Name_Unmapped (N), Name_Comment, Name_Ident) then New_N := Make_Null_Statement (Sloc (N)); -- Do not copy pragmas generated from aspects because the pragmas do @@ -8930,7 +9124,6 @@ package body Sem_Ch12 is Gen_Body : Node_Id; Gen_Decl : Node_Id) is - function In_Same_Scope (Gen_Id, Act_Id : Node_Id) return Boolean; -- Check if the generic definition and the instantiation come from -- a common scope, in which case the instance must be frozen after @@ -8972,12 +9165,12 @@ package body Sem_Ch12 is --------------- function True_Sloc (N, Act_Unit : Node_Id) return Source_Ptr is - Res : Source_Ptr; N1 : Node_Id; + Res : Source_Ptr; begin Res := Sloc (N); - N1 := N; + N1 := N; while Present (N1) and then N1 /= Act_Unit loop if Sloc (N1) > Res then Res := Sloc (N1); @@ -8995,11 +9188,11 @@ package body Sem_Ch12 is Par : constant Entity_Id := Scope (Gen_Id); Gen_Unit : constant Node_Id := Unit (Cunit (Get_Source_Unit (Gen_Decl))); - Orig_Body : Node_Id := Gen_Body; - F_Node : Node_Id; - Body_Unit : Node_Id; + Body_Unit : Node_Id; + F_Node : Node_Id; Must_Delay : Boolean; + Orig_Body : Node_Id := Gen_Body; -- Start of processing for Install_Body @@ -9062,13 +9255,13 @@ package body Sem_Ch12 is Must_Delay := (Gen_Unit = Act_Unit - and then (Nkind_In (Gen_Unit, N_Package_Declaration, - N_Generic_Package_Declaration) + and then (Nkind_In (Gen_Unit, N_Generic_Package_Declaration, + N_Package_Declaration) or else (Gen_Unit = Body_Unit and then True_Sloc (N, Act_Unit) < Sloc (Orig_Body))) and then Is_In_Main_Unit (Original_Node (Gen_Unit)) - and then (In_Same_Scope (Gen_Id, Act_Id))); + and then In_Same_Scope (Gen_Id, Act_Id)); -- If this is an early instantiation, the freeze node is placed after -- the generic body. Otherwise, if the generic appears in an instance, @@ -9624,18 +9817,20 @@ package body Sem_Ch12 is begin case Nkind (Original_Node (F)) is - when N_Formal_Object_Declaration | - N_Formal_Type_Declaration => + when N_Formal_Object_Declaration + | N_Formal_Type_Declaration + => Formal_Ent := Defining_Identifier (F); while Chars (Act) /= Chars (Formal_Ent) loop Next_Entity (Act); end loop; - when N_Formal_Subprogram_Declaration | - N_Formal_Package_Declaration | - N_Package_Declaration | - N_Generic_Package_Declaration => + when N_Formal_Package_Declaration + | N_Formal_Subprogram_Declaration + | N_Generic_Package_Declaration + | N_Package_Declaration + => Formal_Ent := Defining_Entity (F); while Chars (Act) /= Chars (Formal_Ent) loop @@ -9729,19 +9924,19 @@ package body Sem_Ch12 is Kind : constant Node_Kind := Nkind (Original_Node (N)); begin case Kind is - when N_Formal_Object_Declaration => + when N_Formal_Object_Declaration => return Defining_Identifier (N); - when N_Formal_Type_Declaration => + when N_Formal_Type_Declaration => return Defining_Identifier (N); when N_Formal_Subprogram_Declaration => return Defining_Unit_Name (Specification (N)); - when N_Formal_Package_Declaration => + when N_Formal_Package_Declaration => return Defining_Identifier (Original_Node (N)); - when N_Generic_Package_Declaration => + when N_Generic_Package_Declaration => return Defining_Identifier (Original_Node (N)); -- All other declarations are introduced by semantic analysis and @@ -10757,37 +10952,27 @@ package body Sem_Ch12 is -- Instantiate_Package_Body -- ------------------------------ + -- WARNING: This routine manages Ghost and SPARK regions. Return statements + -- must be replaced by gotos which jump to the end of the routine in order + -- to restore the Ghost and SPARK modes. + procedure Instantiate_Package_Body (Body_Info : Pending_Body_Info; Inlined_Body : Boolean := False; Body_Optional : Boolean := False) is Act_Decl : constant Node_Id := Body_Info.Act_Decl; + Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl); + Act_Spec : constant Node_Id := Specification (Act_Decl); Inst_Node : constant Node_Id := Body_Info.Inst_Node; - Loc : constant Source_Ptr := Sloc (Inst_Node); - Gen_Id : constant Node_Id := Name (Inst_Node); Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); - Act_Spec : constant Node_Id := Specification (Act_Decl); - Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec); - - Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; - Save_Style_Check : constant Boolean := Style_Check; - - Act_Body : Node_Id; - Act_Body_Id : Entity_Id; - Act_Body_Name : Node_Id; - Gen_Body : Node_Id; - Gen_Body_Id : Node_Id; - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; - - Parent_Installed : Boolean := False; + Loc : constant Source_Ptr := Sloc (Inst_Node); - Vis_Prims_List : Elist_Id := No_Elist; - -- List of primitives made temporarily visible in the instantiation - -- to match the visibility of the formal type + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_Style_Check : constant Boolean := Style_Check; procedure Check_Initialized_Types; -- In a generic package body, an entity of a generic private type may @@ -10857,6 +11042,26 @@ package body Sem_Ch12 is end loop; end Check_Initialized_Types; + -- Local variables + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the Ghost and SPARK mode-related data to restore on exit + + Act_Body : Node_Id; + Act_Body_Id : Entity_Id; + Act_Body_Name : Node_Id; + Gen_Body : Node_Id; + Gen_Body_Id : Node_Id; + Par_Ent : Entity_Id := Empty; + Par_Vis : Boolean := False; + Parent_Installed : Boolean := False; + + Vis_Prims_List : Elist_Id := No_Elist; + -- List of primitives made temporarily visible in the instantiation + -- to match the visibility of the formal type. + -- Start of processing for Instantiate_Package_Body begin @@ -10869,6 +11074,12 @@ package body Sem_Ch12 is return; end if; + -- The package being instantiated may be subject to pragma Ghost. Set + -- the mode now to ensure that any nodes generated during instantiation + -- are properly marked as Ghost. + + Set_Ghost_Mode (Act_Decl_Id); + Expander_Mode_Save_And_Set (Body_Info.Expander_Status); -- Re-establish the state of information on which checks are suppressed. @@ -10881,8 +11092,10 @@ package body Sem_Ch12 is Opt.Ada_Version := Body_Info.Version; Opt.Ada_Version_Pragma := Body_Info.Version_Pragma; Restore_Warnings (Body_Info.Warnings); - Opt.SPARK_Mode := Body_Info.SPARK_Mode; - Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma; + + -- Install the SPARK mode which applies to the package body + + Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma); if No (Gen_Body_Id) then @@ -10894,7 +11107,7 @@ package body Sem_Ch12 is if not Unit_Requires_Body (Defining_Entity (Gen_Decl)) and then Body_Optional then - return; + goto Leave; else Load_Parent_Of_Generic (Inst_Node, Specification (Gen_Decl), Body_Optional); @@ -10925,13 +11138,16 @@ package body Sem_Ch12 is Save_Env (Gen_Unit, Act_Decl_Id); Style_Check := False; - -- If the context of the instance is subject to SPARK_Mode "off" or - -- the annotation is altogether missing, set the global flag which - -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within - -- the instance. + -- If the context of the instance is subject to SPARK_Mode "off", the + -- annotation is missing, or the body is instantiated at a later pass + -- and its spec ignored SPARK_Mode pragma, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the + -- instance. - if SPARK_Mode /= On then - Ignore_Pragma_SPARK_Mode := True; + if SPARK_Mode /= On + or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id) + then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; end if; Current_Sem_Unit := Body_Info.Current_Sem_Unit; @@ -11069,8 +11285,7 @@ package body Sem_Ch12 is -- interested in finding possible runtime errors. if not CodePeer_Mode - and then Is_Predefined_File_Name - (Unit_File_Name (Get_Source_Unit (Gen_Decl))) + and then In_Predefined_Unit (Gen_Decl) then Analyze (Act_Body, Suppress => All_Checks); else @@ -11102,8 +11317,6 @@ package body Sem_Ch12 is end if; Restore_Env; - Ignore_Pragma_SPARK_Mode := Save_IPSM; - Style_Check := Save_Style_Check; -- If we have no body, and the unit requires a body, then complain. This -- complaint is suppressed if we have detected other errors (since a @@ -11125,7 +11338,7 @@ package body Sem_Ch12 is -- was already detected, since this can cause blowups. else - return; + goto Leave; end if; -- Case of package that does not need a body @@ -11158,28 +11371,43 @@ package body Sem_Ch12 is end if; Expander_Mode_Restore; + + <> + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Style_Check := Saved_Style_Check; end Instantiate_Package_Body; --------------------------------- -- Instantiate_Subprogram_Body -- --------------------------------- + -- WARNING: This routine manages Ghost and SPARK regions. Return statements + -- must be replaced by gotos which jump to the end of the routine in order + -- to restore the Ghost and SPARK modes. + procedure Instantiate_Subprogram_Body (Body_Info : Pending_Body_Info; Body_Optional : Boolean := False) is Act_Decl : constant Node_Id := Body_Info.Act_Decl; + Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl); Inst_Node : constant Node_Id := Body_Info.Inst_Node; - Loc : constant Source_Ptr := Sloc (Inst_Node); Gen_Id : constant Node_Id := Name (Inst_Node); Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); - Act_Decl_Id : constant Entity_Id := - Defining_Unit_Name (Specification (Act_Decl)); + Loc : constant Source_Ptr := Sloc (Inst_Node); Pack_Id : constant Entity_Id := Defining_Unit_Name (Parent (Act_Decl)); - Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the Ghost and SPARK mode-related data to restore on exit + Saved_Style_Check : constant Boolean := Style_Check; Saved_Warnings : constant Warning_Record := Save_Warnings; @@ -11205,6 +11433,12 @@ package body Sem_Ch12 is return; end if; + -- The subprogram being instantiated may be subject to pragma Ghost. Set + -- the mode now to ensure that any nodes generated during instantiation + -- are properly marked as Ghost. + + Set_Ghost_Mode (Act_Decl_Id); + Expander_Mode_Save_And_Set (Body_Info.Expander_Status); -- Re-establish the state of information on which checks are suppressed. @@ -11217,8 +11451,10 @@ package body Sem_Ch12 is Opt.Ada_Version := Body_Info.Version; Opt.Ada_Version_Pragma := Body_Info.Version_Pragma; Restore_Warnings (Body_Info.Warnings); - Opt.SPARK_Mode := Body_Info.SPARK_Mode; - Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma; + + -- Install the SPARK mode which applies to the subprogram body + + Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma); if No (Gen_Body_Id) then @@ -11231,7 +11467,7 @@ package body Sem_Ch12 is Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit)); Set_Convention (Act_Decl_Id, Convention (Gen_Unit)); Set_Has_Completion (Act_Decl_Id); - return; + goto Leave; -- For other cases, compile the body @@ -11256,24 +11492,26 @@ package body Sem_Ch12 is if Expander_Active and then Operating_Mode = Generate_Code then - Error_Msg_N - ("missing proper body for instantiation", Gen_Body); + Error_Msg_N ("missing proper body for instantiation", Gen_Body); end if; Set_Has_Completion (Act_Decl_Id); - return; + goto Leave; end if; Save_Env (Gen_Unit, Act_Decl_Id); Style_Check := False; - -- If the context of the instance is subject to SPARK_Mode "off" or - -- the annotation is altogether missing, set the global flag which - -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within - -- the instance. + -- If the context of the instance is subject to SPARK_Mode "off", the + -- annotation is missing, or the body is instantiated at a later pass + -- and its spec ignored SPARK_Mode pragma, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the + -- instance. - if SPARK_Mode /= On then - Ignore_Pragma_SPARK_Mode := True; + if SPARK_Mode /= On + or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id) + then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; end if; Current_Sem_Unit := Body_Info.Current_Sem_Unit; @@ -11377,8 +11615,6 @@ package body Sem_Ch12 is end if; Restore_Env; - Ignore_Pragma_SPARK_Mode := Saved_IPSM; - Style_Check := Saved_Style_Check; Restore_Warnings (Saved_Warnings); -- Body not found. Error was emitted already. If there were no previous @@ -11393,27 +11629,25 @@ package body Sem_Ch12 is and then Nkind (Parent (Inst_Node)) /= N_Compilation_Unit then if Body_Optional then - return; + goto Leave; elsif Ekind (Act_Decl_Id) = E_Procedure then Act_Body := Make_Subprogram_Body (Loc, - Specification => - Make_Procedure_Specification (Loc, - Defining_Unit_Name => - Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), - Parameter_Specifications => - New_Copy_List - (Parameter_Specifications (Parent (Act_Decl_Id)))), - - Declarations => Empty_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => - New_List ( - Make_Raise_Program_Error (Loc, - Reason => - PE_Access_Before_Elaboration)))); + Specification => + Make_Procedure_Specification (Loc, + Defining_Unit_Name => + Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), + Parameter_Specifications => + New_Copy_List + (Parameter_Specifications (Parent (Act_Decl_Id)))), + + Declarations => Empty_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Make_Raise_Program_Error (Loc, + Reason => PE_Access_Before_Elaboration)))); else Ret_Expr := @@ -11427,9 +11661,9 @@ package body Sem_Ch12 is Make_Subprogram_Body (Loc, Specification => Make_Function_Specification (Loc, - Defining_Unit_Name => + Defining_Unit_Name => Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), - Parameter_Specifications => + Parameter_Specifications => New_Copy_List (Parameter_Specifications (Parent (Act_Decl_Id))), Result_Definition => @@ -11438,9 +11672,8 @@ package body Sem_Ch12 is Declarations => Empty_List, Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, - Statements => - New_List - (Make_Simple_Return_Statement (Loc, Ret_Expr)))); + Statements => New_List ( + Make_Simple_Return_Statement (Loc, Ret_Expr)))); end if; Pack_Body := @@ -11454,6 +11687,12 @@ package body Sem_Ch12 is end if; Expander_Mode_Restore; + + <> + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Style_Check := Saved_Style_Check; end Instantiate_Subprogram_Body; ---------------------- @@ -11466,12 +11705,12 @@ package body Sem_Ch12 is Analyzed_Formal : Node_Id; Actual_Decls : List_Id) return List_Id is - Gen_T : constant Entity_Id := Defining_Identifier (Formal); A_Gen_T : constant Entity_Id := Defining_Identifier (Analyzed_Formal); - Ancestor : Entity_Id := Empty; Def : constant Node_Id := Formal_Type_Definition (Formal); + Gen_T : constant Entity_Id := Defining_Identifier (Formal); Act_T : Entity_Id; + Ancestor : Entity_Id := Empty; Decl_Node : Node_Id; Decl_Nodes : List_Id; Loc : Source_Ptr; @@ -12754,19 +12993,19 @@ package body Sem_Ch12 is when N_Access_To_Object_Definition => Validate_Access_Type_Instance; - when N_Access_Function_Definition | - N_Access_Procedure_Definition => + when N_Access_Function_Definition + | N_Access_Procedure_Definition + => Validate_Access_Subprogram_Instance; - when N_Record_Definition => + when N_Record_Definition => Validate_Interface_Type_Instance; - when N_Derived_Type_Definition => + when N_Derived_Type_Definition => Validate_Derived_Interface_Type_Instance; when others => raise Program_Error; - end case; end if; @@ -12896,7 +13135,6 @@ package body Sem_Ch12 is end if; Current_Unit := Parent (N); - while Present (Current_Unit) and then Nkind (Current_Unit) /= N_Compilation_Unit loop @@ -13094,8 +13332,8 @@ package body Sem_Ch12 is -- package, in which case the usual generic rule applies. declare - Exp_Status : Boolean := True; - Scop : Entity_Id; + Exp_Status : Boolean := True; + Scop : Entity_Id; begin -- Loop through scopes looking for generic package @@ -13169,8 +13407,7 @@ package body Sem_Ch12 is -- Package instance - if - Nkind (Node (Decl)) = N_Package_Instantiation + if Nkind (Node (Decl)) = N_Package_Instantiation then Instantiate_Package_Body (Info, Body_Optional => True); @@ -13185,8 +13422,9 @@ package body Sem_Ch12 is -- these result in the corresponding pragmas, -- inserted after the subprogram declaration. -- They must be skipped as well when retrieving - -- the desired spec. A direct link would be - -- more robust ??? + -- the desired spec. Some of them may have been + -- rewritten as null statements. + -- A direct link would be more robust ??? declare Decl : Node_Id := @@ -13194,7 +13432,9 @@ package body Sem_Ch12 is (Specification (Info.Act_Decl)))); begin while Nkind_In (Decl, - N_Subprogram_Renaming_Declaration, N_Pragma) + N_Null_Statement, + N_Pragma, + N_Subprogram_Renaming_Declaration) loop Decl := Prev (Decl); end loop; @@ -13456,7 +13696,7 @@ package body Sem_Ch12 is Cur : Entity_Id := Empty; -- Current homograph of the instance name - Vis : Boolean; + Vis : Boolean := False; -- Saved visibility status of the current homograph begin @@ -14243,7 +14483,6 @@ package body Sem_Ch12 is then Copy_Dimensions (N2, N); end if; - end Set_Global_Type; ------------------ @@ -14319,7 +14558,7 @@ package body Sem_Ch12 is if Is_Global (Entity (Original_Node (N2))) then N2 := Original_Node (N2); Set_Associated_Node (N, N2); - Set_Global_Type (N, N2); + Set_Global_Type (N, N2); -- Renaming is local, and will be resolved in instance @@ -14361,7 +14600,7 @@ package body Sem_Ch12 is if Is_Global (Entity (Parent (N2))) then Change_Selected_Component_To_Expanded_Name (Parent (N)); Set_Associated_Node (Parent (N), Parent (N2)); - Set_Global_Type (Parent (N), Parent (N2)); + Set_Global_Type (Parent (N), Parent (N2)); Save_Entity_Descendants (N); -- If this is a reference to the current generic entity, replace @@ -14420,7 +14659,7 @@ package body Sem_Ch12 is if Is_Global (Entity (Name (Parent (N2)))) then Change_Selected_Component_To_Expanded_Name (Parent (N)); Set_Associated_Node (Parent (N), Name (Parent (N2))); - Set_Global_Type (Parent (N), Name (Parent (N2))); + Set_Global_Type (Parent (N), Name (Parent (N2))); Save_Entity_Descendants (N); else @@ -14464,14 +14703,16 @@ package body Sem_Ch12 is when N_Unary_Op => Save_Global_Descendant (Union_Id (Right_Opnd (N))); - when N_Expanded_Name | - N_Selected_Component => + when N_Expanded_Name + | N_Selected_Component + => Save_Global_Descendant (Union_Id (Prefix (N))); Save_Global_Descendant (Union_Id (Selector_Name (N))); - when N_Identifier | - N_Character_Literal | - N_Operator_Symbol => + when N_Character_Literal + | N_Identifier + | N_Operator_Symbol + => null; when others => @@ -15287,13 +15528,18 @@ package body Sem_Ch12 is -- Set_Instance_Env -- ---------------------- + -- WARNING: This routine manages SPARK regions + procedure Set_Instance_Env (Gen_Unit : Entity_Id; Act_Unit : Entity_Id) is - Assertion_Status : constant Boolean := Assertions_Enabled; - Save_SPARK_Mode : constant SPARK_Mode_Type := SPARK_Mode; - Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma; + Saved_AE : constant Boolean := Assertions_Enabled; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the SPARK mode-related data because utilizing the configuration + -- values of pragmas and switches will eliminate any previously set + -- SPARK_Mode. begin -- Regardless of the current mode, predefined units are analyzed in the @@ -15301,10 +15547,7 @@ package body Sem_Ch12 is -- to predefined units. Nothing needs to be done for non-internal units. -- These are always analyzed in the current mode. - if Is_Internal_File_Name - (Fname => Unit_File_Name (Get_Source_Unit (Gen_Unit)), - Renamings_Included => True) - then + if In_Internal_Unit (Gen_Unit) then Set_Opt_Config_Switches (True, Current_Sem_Unit = Main_Unit); -- In Ada2012 we may want to enable assertions in an instance of a @@ -15314,14 +15557,13 @@ package body Sem_Ch12 is -- as is already the case for some numeric libraries. if Ada_Version >= Ada_2012 then - Assertions_Enabled := Assertion_Status; + Assertions_Enabled := Saved_AE; end if; - -- SPARK_Mode for an instance is the one applicable at the point of + -- Reinstall the SPARK_Mode which was in effect at the point of -- instantiation. - SPARK_Mode := Save_SPARK_Mode; - SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma; + Install_SPARK_Mode (Saved_SM, Saved_SMP); end if; Current_Instantiated_Parent := @@ -15420,27 +15662,43 @@ package body Sem_Ch12 is end loop; case Attr_Id is - when Attribute_Adjacent | Attribute_Ceiling | Attribute_Copy_Sign | - Attribute_Floor | Attribute_Fraction | Attribute_Machine | - Attribute_Model | Attribute_Remainder | Attribute_Rounding | - Attribute_Unbiased_Rounding => + when Attribute_Adjacent + | Attribute_Ceiling + | Attribute_Copy_Sign + | Attribute_Floor + | Attribute_Fraction + | Attribute_Machine + | Attribute_Model + | Attribute_Remainder + | Attribute_Rounding + | Attribute_Unbiased_Rounding + => OK := Is_Fun and then Num_F = 1 and then Is_Floating_Point_Type (T); - when Attribute_Image | Attribute_Pred | Attribute_Succ | - Attribute_Value | Attribute_Wide_Image | - Attribute_Wide_Value => - OK := (Is_Fun and then Num_F = 1 and then Is_Scalar_Type (T)); + when Attribute_Image + | Attribute_Pred + | Attribute_Succ + | Attribute_Value + | Attribute_Wide_Image + | Attribute_Wide_Value + => + OK := Is_Fun and then Num_F = 1 and then Is_Scalar_Type (T); - when Attribute_Max | Attribute_Min => - OK := (Is_Fun and then Num_F = 2 and then Is_Scalar_Type (T)); + when Attribute_Max + | Attribute_Min + => + OK := Is_Fun and then Num_F = 2 and then Is_Scalar_Type (T); when Attribute_Input => OK := (Is_Fun and then Num_F = 1); - when Attribute_Output | Attribute_Read | Attribute_Write => - OK := (not Is_Fun and then Num_F = 2); + when Attribute_Output + | Attribute_Read + | Attribute_Write + => + OK := not Is_Fun and then Num_F = 2; when others => OK := False;