From: Hristian Kirtchev Date: Tue, 25 Apr 2017 13:30:56 +0000 (+0000) Subject: contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Add a warning about SPARK... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9a8f9105771efaf9188cb1c6c979cea3f677c63;p=gcc.git contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Add a warning about SPARK mode management. 2017-04-25 Hristian Kirtchev * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. (Analyze_Entry_Or_Subprogram_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. (Analyze_Object_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. (Analyze_Package_Body_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. (Analyze_Package_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. (Analyze_Task_Contract): Add a warning about SPARK mode management. The routine now saves and restores both the mode and associated pragma. * expander.adb (Expand): Change the way the Ghost mode is saved and restored. * exp_ch3.adb (Freeze_Type): Change the way the Ghost mode is saved and restored. * exp_disp.adb (Make_DT): Change the way the Ghost mode is saved and restored. * exp_util.adb (Build_DIC_Procedure_Body): Change the way the Ghost mode is saved and restored. (Build_DIC_Procedure_Declaration): Change the way the Ghost mode is saved and restored. (Build_Invariant_Procedure_Body): Change the way the Ghost mode is saved and restored. (Build_Invariant_Procedure_Declaration): Change the way the Ghost mode is saved and restored. (Make_Predicate_Call): Change the way the Ghost mode is saved and restored. * freeze.adb (Freeze_Entity): Change the way the Ghost mode is saved and restored. * ghost.adb (Mark_And_Set_Ghost_Assignment): Remove parameter Mode and its assignment. (Mark_And_Set_Ghost_Body): Remove parameter Mode and its assignment. (Mark_And_Set_Ghost_Completion): Remove parameter Mode and its assignment. (Mark_And_Set_Ghost_Declaration): Remove parameter Mode and its assignment. (Mark_And_Set_Ghost_Instantiation): Remove parameter Mode and its assignment. (Mark_And_Set_Ghost_Procedure_Call): Remove parameter Mode and its assignment. (Set_Ghost_Mode): Remove parameter Mode and its assignment. * ghost.ads (Mark_And_Set_Ghost_Assignment): Remove parameter Mode and update the comment on usage. (Mark_And_Set_Ghost_Body): Remove parameter Mode and update the comment on usage. (Mark_And_Set_Ghost_Completion): Remove parameter Mode and update the comment on usage. (Mark_And_Set_Ghost_Declaration): Remove parameter Mode and update the comment on usage. (Mark_And_Set_Ghost_Instantiation): Remove parameter Mode and update the comment on usage. (Mark_And_Set_Ghost_Procedure_Call): Remove parameter Mode and update the comment on usage. (Set_Ghost_Mode): Remove parameter Mode and update the comment on usage. * lib.ads Remove obsolete fields SPARK_Mode_Pragma from various types. * lib-load.adb (Create_Dummy_Package_Unit): Remove the assignment of obsolete field SPARK_Mode_Pragma. (Load_Main_Source): Remove the assignment of obsolete field SPARK_Mode_Pragma. (Load_Unit): Remove the assignment of obsolete field SPARK_Mode_Pragma. * lib-writ.adb (Add_Preprocessing_Dependency): Remove the assignment of obsolete field SPARK_Mode_Pragma. (Ensure_System_Dependency): Remove the assignment of obsolete field SPARK_Mode_Pragma. * rtsfind.adb (Load_RTU): Add a warning about Ghost and SPARK mode management. Change the way Ghost and SPARK modes are saved and restored. * sem.adb (Analyze): Change the way the Ghost mode is saved and restored. * sem_ch3.adb (Analyze_Object_Declaration): Change the way the Ghost mode is saved and restored. (Process_Full_View): Change the way the Ghost mode is saved and restored. * sem_ch5.adb (Analyze_Assignment): Change the way the Ghost mode is saved and restored. * sem_ch6.adb (Analyze_Procedure_Call): Change the way the Ghost mode is saved and restored. (Analyze_Subprogram_Body_Helper): Change the way the Ghost mode is saved and restored. * sem_ch7.adb (Analyze_Package_Body_Helper): Change the way the Ghost mode is saved and restored. * sem_ch10.adb (Analyze_Subunit): Add a warning about SPARK mode management. Save the SPARK mode-related data prior to any changes to the scope stack and contexts. The mode is then reinstalled before the subunit is analyzed in order to restore the original view of the subunit. * sem_ch12.adb (Analyze_Package_Instantiation): Update the warning on region management. Change the way the Ghost and SPARK modes are saved and restored. (Inline_Instance_Body): Add a warning about SPARK mode management. Code clean up. (Analyze_Subprogram_Instantiation): Update the warning on region management. Change the way the Ghost and SPARK modes are saved and restored. (Instantiate_Package_Body): Update the warning on region management. Change the way the Ghost and SPARK modes are saved and restored. (Instantiate_Subprogram_Body): Update the warning on region management. Change the way the Ghost and SPARK modes are saved and restored. (Set_Instance_Env): Add a warning about SPARK mode management. Change the way SPARK mode is saved and restored. * sem_ch13.adb (Build_Predicate_Functions): Change the way the Ghost mode is saved and restored. (Build_Predicate_Function_Declaration): Change the way the Ghost mode is saved and restored. * sem_elab.adb (Check_Elab_Calls): Add a warning about SPARK mode management. Change the way SPARK mode is saved and restored. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Change the way the Ghost mode is saved and restored. (Analyze_Initial_Condition_In_Decl_Part): Change the way the Ghost mode is saved and restored. (Analyze_Pragma): Change the way the Ghost mode is saved and restored. (Analyze_Pre_Post_Condition_In_Decl_Part): Change the way the Ghost mode is saved and restored. * sem_util.adb (Install_SPARK_Mode): New routine. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): Removed. (Set_SPARK_Mode): New routine. * sem_util.ads (Install_SPARK_Mode): New routine. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): Removed. (Set_SPARK_Mode): New routine. From-SVN: r247230 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6badf78f337..fc2de1da12c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,141 @@ +2017-04-25 Hristian Kirtchev + + * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): + Add a warning about SPARK mode management. The routine now + saves and restores both the mode and associated pragma. + (Analyze_Entry_Or_Subprogram_Contract): Add a warning about + SPARK mode management. The routine now saves and restores both + the mode and associated pragma. + (Analyze_Object_Contract): + Add a warning about SPARK mode management. The routine + now saves and restores both the mode and associated pragma. + (Analyze_Package_Body_Contract): Add a warning about SPARK mode + management. The routine now saves and restores both the mode + and associated pragma. (Analyze_Package_Contract): Add a warning + about SPARK mode management. The routine now saves and restores + both the mode and associated pragma. + (Analyze_Task_Contract): + Add a warning about SPARK mode management. The routine now saves + and restores both the mode and associated pragma. + * expander.adb (Expand): Change the way the Ghost mode is saved + and restored. + * exp_ch3.adb (Freeze_Type): Change the way the Ghost mode is + saved and restored. + * exp_disp.adb (Make_DT): Change the way the Ghost mode is saved + and restored. + * exp_util.adb (Build_DIC_Procedure_Body): + Change the way the Ghost mode is saved and restored. + (Build_DIC_Procedure_Declaration): Change the way the Ghost + mode is saved and restored. + (Build_Invariant_Procedure_Body): + Change the way the Ghost mode is saved and restored. + (Build_Invariant_Procedure_Declaration): Change the way the Ghost + mode is saved and restored. + (Make_Predicate_Call): Change the + way the Ghost mode is saved and restored. + * freeze.adb (Freeze_Entity): Change the way the Ghost mode is + saved and restored. + * ghost.adb (Mark_And_Set_Ghost_Assignment): Remove parameter Mode + and its assignment. + (Mark_And_Set_Ghost_Body): Remove parameter + Mode and its assignment. + (Mark_And_Set_Ghost_Completion): + Remove parameter Mode and its assignment. + (Mark_And_Set_Ghost_Declaration): Remove parameter Mode and its + assignment. + (Mark_And_Set_Ghost_Instantiation): Remove parameter + Mode and its assignment. + (Mark_And_Set_Ghost_Procedure_Call): + Remove parameter Mode and its assignment. + (Set_Ghost_Mode): + Remove parameter Mode and its assignment. + * ghost.ads (Mark_And_Set_Ghost_Assignment): Remove parameter Mode + and update the comment on usage. + (Mark_And_Set_Ghost_Body): + Remove parameter Mode and update the comment on usage. + (Mark_And_Set_Ghost_Completion): Remove parameter Mode and + update the comment on usage. + (Mark_And_Set_Ghost_Declaration): + Remove parameter Mode and update the comment on usage. + (Mark_And_Set_Ghost_Instantiation): Remove parameter Mode and + update the comment on usage. + (Mark_And_Set_Ghost_Procedure_Call): + Remove parameter Mode and update the comment on usage. + (Set_Ghost_Mode): Remove parameter Mode and update the comment + on usage. + * lib.ads Remove obsolete fields SPARK_Mode_Pragma from various + types. + * lib-load.adb (Create_Dummy_Package_Unit): Remove the assignment + of obsolete field SPARK_Mode_Pragma. + (Load_Main_Source): Remove + the assignment of obsolete field SPARK_Mode_Pragma. + (Load_Unit): Remove the assignment of obsolete field SPARK_Mode_Pragma. + * lib-writ.adb (Add_Preprocessing_Dependency): Remove + the assignment of obsolete field SPARK_Mode_Pragma. + (Ensure_System_Dependency): Remove the assignment of obsolete + field SPARK_Mode_Pragma. + * rtsfind.adb (Load_RTU): Add a warning about Ghost and SPARK + mode management. Change the way Ghost and SPARK modes are saved + and restored. + * sem.adb (Analyze): Change the way the Ghost mode is saved + and restored. + * sem_ch3.adb (Analyze_Object_Declaration): Change the way the + Ghost mode is saved and restored. + (Process_Full_View): Change + the way the Ghost mode is saved and restored. + * sem_ch5.adb (Analyze_Assignment): Change the way the Ghost + mode is saved and restored. + * sem_ch6.adb (Analyze_Procedure_Call): Change the way the Ghost + mode is saved and restored. + (Analyze_Subprogram_Body_Helper): + Change the way the Ghost mode is saved and restored. + * sem_ch7.adb (Analyze_Package_Body_Helper): Change the way the + Ghost mode is saved and restored. + * sem_ch10.adb (Analyze_Subunit): Add a warning about SPARK mode + management. Save the SPARK mode-related data prior to any changes + to the scope stack and contexts. The mode is then reinstalled + before the subunit is analyzed in order to restore the original + view of the subunit. + * sem_ch12.adb (Analyze_Package_Instantiation): Update the + warning on region management. Change the way the Ghost and + SPARK modes are saved and restored. + (Inline_Instance_Body): + Add a warning about SPARK mode management. Code clean up. + (Analyze_Subprogram_Instantiation): Update the warning on region + management. Change the way the Ghost and SPARK modes are saved + and restored. + (Instantiate_Package_Body): Update the warning + on region management. Change the way the Ghost and SPARK modes + are saved and restored. + (Instantiate_Subprogram_Body): Update + the warning on region management. Change the way the Ghost and + SPARK modes are saved and restored. + (Set_Instance_Env): Add a + warning about SPARK mode management. Change the way SPARK mode + is saved and restored. + * sem_ch13.adb (Build_Predicate_Functions): + Change the way the Ghost mode is saved and restored. + (Build_Predicate_Function_Declaration): Change the way the Ghost + mode is saved and restored. + * sem_elab.adb (Check_Elab_Calls): Add a warning about SPARK + mode management. Change the way SPARK mode is saved and restored. + * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): + Change the way the Ghost mode is saved and restored. + (Analyze_Initial_Condition_In_Decl_Part): Change the way + the Ghost mode is saved and restored. + (Analyze_Pragma): + Change the way the Ghost mode is saved and restored. + (Analyze_Pre_Post_Condition_In_Decl_Part): Change the way the + Ghost mode is saved and restored. + * sem_util.adb (Install_SPARK_Mode): New routine. + (Restore_SPARK_Mode): New routine. + (Save_SPARK_Mode_And_Set): Removed. + (Set_SPARK_Mode): New routine. + * sem_util.ads (Install_SPARK_Mode): New routine. + (Restore_SPARK_Mode): New routine. + (Save_SPARK_Mode_And_Set): Removed. + (Set_SPARK_Mode): New routine. + 2017-04-25 Ed Schonberg * sem_util.adb, sem_util.ads (From_Nested_Package): New predicate diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 61f05c5dd69..e4dc59ece28 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -444,11 +444,18 @@ package body Contracts is -- Analyze_Entry_Or_Subprogram_Body_Contract -- ----------------------------------------------- + -- 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 Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); Items : constant Node_Id := Contract (Body_Id); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); - Mode : SPARK_Mode_Type; + + 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 begin -- When a subprogram body declaration is illegal, its defining entity is @@ -473,7 +480,7 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related subprogram body. - Save_SPARK_Mode_And_Set (Body_Id, Mode); + Set_SPARK_Mode (Body_Id); -- Ensure that the contract cases or postconditions mention 'Result or -- define a post-state. @@ -499,7 +506,7 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - Restore_SPARK_Mode (Mode); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); -- Capture all global references in a generic subprogram body now that -- the contract has been analyzed. @@ -523,6 +530,10 @@ package body Contracts is -- Analyze_Entry_Or_Subprogram_Contract -- ------------------------------------------ + -- 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 Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id; Freeze_Id : Entity_Id := Empty) @@ -530,6 +541,10 @@ package body Contracts is Items : constant Node_Id := Contract (Subp_Id); Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + 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 + Skip_Assert_Exprs : constant Boolean := Ekind_In (Subp_Id, E_Entry, E_Entry_Family) and then not ASIS_Mode @@ -537,7 +552,6 @@ package body Contracts is Depends : Node_Id := Empty; Global : Node_Id := Empty; - Mode : SPARK_Mode_Type; Prag : Node_Id; Prag_Nam : Name_Id; @@ -557,7 +571,7 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related subprogram body. - Save_SPARK_Mode_And_Set (Subp_Id, Mode); + Set_SPARK_Mode (Subp_Id); -- All subprograms carry a contract, but for some it is not significant -- and should not be processed. @@ -667,7 +681,7 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - Restore_SPARK_Mode (Mode); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); -- Capture all global references in a generic subprogram now that the -- contract has been analyzed. @@ -683,21 +697,28 @@ package body Contracts is -- Analyze_Object_Contract -- ----------------------------- + -- 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 Analyze_Object_Contract (Obj_Id : Entity_Id; Freeze_Id : Entity_Id := Empty) is - Obj_Typ : constant Entity_Id := Etype (Obj_Id); - AR_Val : Boolean := False; - AW_Val : Boolean := False; - ER_Val : Boolean := False; - EW_Val : Boolean := False; - Items : Node_Id; - Mode : SPARK_Mode_Type; - Prag : Node_Id; - Ref_Elmt : Elmt_Id; - Restore_Mode : Boolean := False; - Seen : Boolean := False; + Obj_Typ : constant Entity_Id := Etype (Obj_Id); + + 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 + + AR_Val : Boolean := False; + AW_Val : Boolean := False; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + Items : Node_Id; + Prag : Node_Id; + Ref_Elmt : Elmt_Id; + Seen : Boolean := False; begin -- The loop parameter in an element iterator over a formal container @@ -728,8 +749,7 @@ package body Contracts is if Is_Single_Concurrent_Object (Obj_Id) and then Present (SPARK_Pragma (Obj_Id)) then - Restore_Mode := True; - Save_SPARK_Mode_And_Set (Obj_Id, Mode); + Set_SPARK_Mode (Obj_Id); end if; -- Constant-related checks @@ -929,15 +949,17 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - if Restore_Mode then - Restore_SPARK_Mode (Mode); - end if; + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Object_Contract; ----------------------------------- -- Analyze_Package_Body_Contract -- ----------------------------------- + -- 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 Analyze_Package_Body_Contract (Body_Id : Entity_Id; Freeze_Id : Entity_Id := Empty) @@ -945,7 +967,11 @@ package body Contracts is Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); Items : constant Node_Id := Contract (Body_Id); Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); - Mode : SPARK_Mode_Type; + + 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 + Ref_State : Node_Id; begin @@ -964,7 +990,7 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related package body. - Save_SPARK_Mode_And_Set (Body_Id, Mode); + Set_SPARK_Mode (Body_Id); Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); @@ -978,7 +1004,7 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - Restore_SPARK_Mode (Mode); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); -- Capture all global references in a generic package body now that the -- contract has been analyzed. @@ -994,12 +1020,20 @@ package body Contracts is -- Analyze_Package_Contract -- ------------------------------ + -- 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 Analyze_Package_Contract (Pack_Id : Entity_Id) is Items : constant Node_Id := Contract (Pack_Id); Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); + + 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 + Init : Node_Id := Empty; Init_Cond : Node_Id := Empty; - Mode : SPARK_Mode_Type; Prag : Node_Id; Prag_Nam : Name_Id; @@ -1019,7 +1053,7 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related package. - Save_SPARK_Mode_And_Set (Pack_Id, Mode); + Set_SPARK_Mode (Pack_Id); if Present (Items) then @@ -1066,7 +1100,7 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - Restore_SPARK_Mode (Mode); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); -- Capture all global references in a generic package now that the -- contract has been analyzed. @@ -1204,10 +1238,18 @@ package body Contracts is -- Analyze_Task_Contract -- --------------------------- + -- 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 Analyze_Task_Contract (Task_Id : Entity_Id) is Items : constant Node_Id := Contract (Task_Id); - Mode : SPARK_Mode_Type; - Prag : Node_Id; + + 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 + + Prag : Node_Id; begin -- Do not analyze a contract multiple times @@ -1225,7 +1267,7 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related task unit. - Save_SPARK_Mode_And_Set (Task_Id, Mode); + Set_SPARK_Mode (Task_Id); -- Analyze Global first, as Depends may mention items classified in the -- global categorization. @@ -1248,7 +1290,7 @@ package body Contracts is -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. - Restore_SPARK_Mode (Mode); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Task_Contract; ------------------------------------------------- diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index b67ee2d4254..094f70e0eab 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.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- -- @@ -7193,9 +7193,10 @@ package body Exp_Ch3 is Def_Id : constant Entity_Id := Entity (N); - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; - Result : Boolean := False; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + + Result : Boolean := False; -- Start of processing for Freeze_Type @@ -7204,8 +7205,7 @@ package body Exp_Ch3 is -- now to ensure that any nodes generated during freezing are properly -- marked as Ghost. - Set_Ghost_Mode (Def_Id, Mode); - Mode_Set := True; + Set_Ghost_Mode (Def_Id); -- Process any remote access-to-class-wide types designating the type -- being frozen. @@ -7548,17 +7548,13 @@ package body Exp_Ch3 is Build_Invariant_Procedure_Body (Def_Id); end if; - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Restore_Ghost_Mode (Saved_GM); return Result; exception when RE_Not_Available => - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Restore_Ghost_Mode (Saved_GM); return False; end Freeze_Type; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 65eb6328457..96f62a0f4b4 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.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- -- @@ -4396,6 +4396,9 @@ package body Exp_Disp is Name_TSD : constant Name_Id := New_External_Name (Tname, 'B', Suffix_Index => -1); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + AI : Elmt_Id; AI_Tag_Elmt : Elmt_Id; AI_Tag_Comp : Elmt_Id; @@ -4408,7 +4411,6 @@ package body Exp_Disp is ITable : Node_Id; I_Depth : Nat := 0; Iface_Table_Node : Node_Id; - Mode : Ghost_Mode_Type; Name_ITable : Name_Id; Nb_Predef_Prims : Nat := 0; Nb_Prim : Nat := 0; @@ -4436,7 +4438,7 @@ package body Exp_Disp is -- the mode now to ensure that any nodes generated during dispatch table -- creation are properly marked as Ghost. - Set_Ghost_Mode (Typ, Mode); + Set_Ghost_Mode (Typ); -- Handle cases in which there is no need to build the dispatch table @@ -6242,7 +6244,7 @@ package body Exp_Disp is Register_CG_Node (Typ); <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); return Result; end Make_DT; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 19ba42b024a..16e33e8ebb7 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.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- -- @@ -1529,11 +1529,13 @@ package body Exp_Util is Loc : constant Source_Ptr := Sloc (Typ); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + DIC_Prag : Node_Id; DIC_Typ : Entity_Id; Dummy_1 : Entity_Id; Dummy_2 : Entity_Id; - Mode : Ghost_Mode_Type; Proc_Body : Node_Id; Proc_Body_Id : Entity_Id; Proc_Decl : Node_Id; @@ -1582,7 +1584,7 @@ package body Exp_Util is -- The working type may be subject to pragma Ghost. Set the mode now to -- ensure that the DIC procedure is properly marked as Ghost. - Set_Ghost_Mode (Work_Typ, Mode); + Set_Ghost_Mode (Work_Typ); -- The working type must be either define a DIC pragma of its own or -- inherit one from a parent type. @@ -1762,7 +1764,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Build_DIC_Procedure_Body; ------------------------------------- @@ -1776,9 +1778,11 @@ package body Exp_Util is procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is Loc : constant Source_Ptr := Sloc (Typ); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + DIC_Prag : Node_Id; DIC_Typ : Entity_Id; - Mode : Ghost_Mode_Type; Proc_Decl : Node_Id; Proc_Id : Entity_Id; Typ_Decl : Node_Id; @@ -1835,7 +1839,7 @@ package body Exp_Util is -- The working type may be subject to pragma Ghost. Set the mode now to -- ensure that the DIC procedure is properly marked as Ghost. - Set_Ghost_Mode (Work_Typ, Mode); + Set_Ghost_Mode (Work_Typ); -- The type must be either subject to a DIC pragma or inherit one from a -- parent type. @@ -1959,7 +1963,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Build_DIC_Procedure_Declaration; ------------------------------------ @@ -2889,8 +2893,10 @@ package body Exp_Util is -- Local variables + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Dummy : Entity_Id; - Mode : Ghost_Mode_Type; Priv_Item : Node_Id; Proc_Body : Node_Id; Proc_Body_Id : Entity_Id; @@ -2944,7 +2950,7 @@ package body Exp_Util is -- The working type may be subject to pragma Ghost. Set the mode now to -- ensure that the invariant procedure is properly marked as Ghost. - Set_Ghost_Mode (Work_Typ, Mode); + Set_Ghost_Mode (Work_Typ); -- The type must either have invariants of its own, inherit class-wide -- invariants from parent types or interfaces, or be an array or record @@ -3228,7 +3234,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Build_Invariant_Procedure_Body; ------------------------------------------- @@ -3245,7 +3251,9 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Typ); - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Proc_Decl : Node_Id; Proc_Id : Entity_Id; Proc_Nam : Name_Id; @@ -3295,7 +3303,7 @@ package body Exp_Util is -- The working type may be subject to pragma Ghost. Set the mode now to -- ensure that the invariant procedure is properly marked as Ghost. - Set_Ghost_Mode (Work_Typ, Mode); + Set_Ghost_Mode (Work_Typ); -- The type must either have invariants of its own, inherit class-wide -- invariants from parent or interface types, or be an array or record @@ -3452,7 +3460,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Build_Invariant_Procedure_Declaration; -------------------------- @@ -9288,9 +9296,11 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Expr); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Call : Node_Id; Func_Id : Entity_Id; - Mode : Ghost_Mode_Type; begin pragma Assert (Present (Predicate_Function (Typ))); @@ -9298,7 +9308,7 @@ package body Exp_Util is -- The related type may be subject to pragma Ghost. Set the mode now to -- ensure that the call is properly marked as Ghost. - Set_Ghost_Mode (Typ, Mode); + Set_Ghost_Mode (Typ); -- Call special membership version if requested and available @@ -9315,7 +9325,8 @@ package body Exp_Util is Name => New_Occurrence_Of (Func_Id, Loc), Parameter_Associations => New_List (Relocate_Node (Expr))); - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); + return Call; end Make_Predicate_Call; diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index 23dd9197156..259618d62e7 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.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- -- @@ -82,7 +82,8 @@ package body Expander is -- Ghost mode. procedure Expand (N : Node_Id) is - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit begin -- If we were analyzing a default expression (or other spec expression) @@ -98,7 +99,7 @@ package body Expander is -- Establish the Ghost mode of the context to ensure that any generated -- nodes during expansion are marked as Ghost. - Set_Ghost_Mode (N, Mode); + Set_Ghost_Mode (N); -- The GNATprove_Mode flag indicates that a light expansion for formal -- verification should be used. This expansion is never done inside @@ -529,7 +530,7 @@ package body Expander is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Expand; --------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 5afdc6666e2..890a6a7c9d0 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -5107,7 +5107,8 @@ package body Freeze is -- Local variables - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit -- Start of processing for Freeze_Entity @@ -5116,7 +5117,7 @@ package body Freeze is -- now to ensure that any nodes generated during freezing are properly -- flagged as Ghost. - Set_Ghost_Mode (E, Mode); + Set_Ghost_Mode (E); -- We are going to test for various reasons why this entity need not be -- frozen here, but in the case of an Itype that's defined within a @@ -6723,7 +6724,8 @@ package body Freeze is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); + return Result; end Freeze_Entity; diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index ec4c1d646c4..0e65b7b21db 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2014-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2014-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- -- @@ -1099,17 +1099,10 @@ package body Ghost is -- Mark_And_Set_Ghost_Assignment -- ----------------------------------- - procedure Mark_And_Set_Ghost_Assignment - (N : Node_Id; - Mode : out Ghost_Mode_Type) - is + procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is Id : Entity_Id; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- An assignment statement becomes Ghost when its target denotes a Ghost -- object. Install the Ghost mode of the target. @@ -1134,17 +1127,12 @@ package body Ghost is procedure Mark_And_Set_Ghost_Body (N : Node_Id; - Spec_Id : Entity_Id; - Mode : out Ghost_Mode_Type) + Spec_Id : Entity_Id) is Body_Id : constant Entity_Id := Defining_Entity (N); Policy : Name_Id := No_Name; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- A body becomes Ghost when it is subject to aspect or pragma Ghost if Is_Subject_To_Ghost (N) then @@ -1193,17 +1181,12 @@ package body Ghost is procedure Mark_And_Set_Ghost_Completion (N : Node_Id; - Prev_Id : Entity_Id; - Mode : out Ghost_Mode_Type) + Prev_Id : Entity_Id) is Compl_Id : constant Entity_Id := Defining_Entity (N); Policy : Name_Id := No_Name; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- A completion elaborated in a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). @@ -1243,18 +1226,11 @@ package body Ghost is -- Mark_And_Set_Ghost_Declaration -- ------------------------------------ - procedure Mark_And_Set_Ghost_Declaration - (N : Node_Id; - Mode : out Ghost_Mode_Type) - is + procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is Par_Id : Entity_Id; Policy : Name_Id := No_Name; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- A declaration becomes Ghost when it is subject to aspect or pragma -- Ghost. @@ -1309,16 +1285,11 @@ package body Ghost is procedure Mark_And_Set_Ghost_Instantiation (N : Node_Id; - Gen_Id : Entity_Id; - Mode : out Ghost_Mode_Type) + Gen_Id : Entity_Id) is Policy : Name_Id := No_Name; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- An instantiation becomes Ghost when it is subject to pragma Ghost if Is_Subject_To_Ghost (N) then @@ -1355,17 +1326,10 @@ package body Ghost is -- Mark_And_Set_Ghost_Procedure_Call -- --------------------------------------- - procedure Mark_And_Set_Ghost_Procedure_Call - (N : Node_Id; - Mode : out Ghost_Mode_Type) - is + procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is Id : Entity_Id; begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- A procedure call becomes Ghost when the procedure being invoked is -- Ghost. Install the Ghost mode of the procedure. @@ -1695,10 +1659,7 @@ package body Ghost is -- Set_Ghost_Mode -- -------------------- - procedure Set_Ghost_Mode - (N : Node_Or_Entity_Id; - Mode : out Ghost_Mode_Type) - is + procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); -- Install the Ghost mode of entity Id @@ -1724,10 +1685,6 @@ package body Ghost is -- Start of processing for Set_Ghost_Mode begin - -- Save the previous Ghost mode in effect - - Mode := Ghost_Mode; - -- The Ghost mode of an assignment statement depends on the Ghost mode -- of the target. diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index e0211c02f10..90983abcad4 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2014-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2014-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- -- @@ -101,21 +101,17 @@ package Ghost is procedure Lock; -- Lock internal tables before calling backend - procedure Mark_And_Set_Ghost_Assignment - (N : Node_Id; - Mode : out Ghost_Mode_Type); + procedure Mark_And_Set_Ghost_Assignment (N : Node_Id); -- Mark assignment statement N as Ghost when: -- -- * The left hand side denotes a Ghost entity -- - -- Install the Ghost mode of the assignment statement. Mode is the Ghost - -- mode in effect prior to processing the assignment. This routine starts + -- Install the Ghost mode of the assignment statement. This routine starts -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode. procedure Mark_And_Set_Ghost_Body (N : Node_Id; - Spec_Id : Entity_Id; - Mode : out Ghost_Mode_Type); + Spec_Id : Entity_Id); -- Mark package or subprogram body N as Ghost when: -- -- * The body is subject to pragma Ghost @@ -125,14 +121,12 @@ package Ghost is -- -- * The body appears within a Ghost region -- - -- Install the Ghost mode of the body. Mode is the Ghost mode prior to - -- processing the body. This routine starts a Ghost region and must be - -- used in conjunction with Restore_Ghost_Mode. + -- Install the Ghost mode of the body. This routine starts a Ghost region + -- and must be used in conjunction with Restore_Ghost_Mode. procedure Mark_And_Set_Ghost_Completion (N : Node_Id; - Prev_Id : Entity_Id; - Mode : out Ghost_Mode_Type); + Prev_Id : Entity_Id); -- Mark completion N of a deferred constant or private type [extension] -- Ghost when: -- @@ -140,13 +134,10 @@ package Ghost is -- -- * The completion appears within a Ghost region -- - -- Install the Ghost mode of the completion. Mode is the Ghost mode prior - -- to processing the completion. This routine starts a Ghost region and - -- must be used in conjunction with Restore_Ghost_Mode. + -- Install the Ghost mode of the completion. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. - procedure Mark_And_Set_Ghost_Declaration - (N : Node_Id; - Mode : out Ghost_Mode_Type); + procedure Mark_And_Set_Ghost_Declaration (N : Node_Id); -- Mark declaration N as Ghost when: -- -- * The declaration is subject to pragma Ghost @@ -156,14 +147,12 @@ package Ghost is -- -- * The declaration appears within a Ghost region -- - -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior - -- to processing the declaration. This routine starts a Ghost region and - -- must be used in conjunction with Restore_Ghost_Mode. + -- Install the Ghost mode of the declaration. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. procedure Mark_And_Set_Ghost_Instantiation (N : Node_Id; - Gen_Id : Entity_Id; - Mode : out Ghost_Mode_Type); + Gen_Id : Entity_Id); -- Mark instantiation N as Ghost when: -- -- * The instantiation is subject to pragma Ghost @@ -172,20 +161,16 @@ package Ghost is -- -- * The instantiation appears within a Ghost region -- - -- Install the Ghost mode of the instantiation. Mode is the Ghost mode - -- prior to processing the instantiation. This routine starts a Ghost + -- Install the Ghost mode of the instantiation. This routine starts a Ghost -- region and must be used in conjunction with Restore_Ghost_Mode. - procedure Mark_And_Set_Ghost_Procedure_Call - (N : Node_Id; - Mode : out Ghost_Mode_Type); + procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id); -- Mark procedure call N as Ghost when: -- -- * The procedure being invoked is a Ghost entity -- - -- Install the Ghost mode of the procedure call. Mode is the Ghost mode - -- prior to processing the procedure call. This routine starts a Ghost - -- region and must be used in conjunction with Restore_Ghost_Mode. + -- Install the Ghost mode of the procedure call. This routine starts a + -- Ghost region and must be used in conjunction with Restore_Ghost_Mode. procedure Mark_Ghost_Clause (N : Node_Id); -- Mark use package, use type, or with clause N as Ghost when: @@ -220,12 +205,9 @@ package Ghost is -- region denoted by Mode. This routine must be used in conjunction -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode. - procedure Set_Ghost_Mode - (N : Node_Or_Entity_Id; - Mode : out Ghost_Mode_Type); - -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior - -- to processing the node. This routine starts a Ghost region and must be - -- used in conjunction with Restore_Ghost_Mode. + procedure Set_Ghost_Mode (N : Node_Or_Entity_Id); + -- Install the Ghost mode of arbitrary node N. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. procedure Set_Is_Ghost_Entity (Id : Entity_Id); -- Set the relevant Ghost attributes of entity Id depending on the current diff --git a/gcc/ada/lib-load.adb b/gcc/ada/lib-load.adb index f68e40e962f..dc8deb571f5 100644 --- a/gcc/ada/lib-load.adb +++ b/gcc/ada/lib-load.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- -- @@ -227,8 +227,7 @@ package body Lib.Load is Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False), Unit_Name => Spec_Name, Version => 0, - OA_Setting => 'O', - SPARK_Mode_Pragma => Empty); + OA_Setting => 'O'); Set_Comes_From_Source_Default (Save_CS); Set_Error_Posted (Cunit_Entity); @@ -334,8 +333,7 @@ package body Lib.Load is Unit_File_Name => Fname, Unit_Name => No_Unit_Name, Version => Version, - OA_Setting => 'O', - SPARK_Mode_Pragma => Empty); + OA_Setting => 'O'); end if; end Load_Main_Source; @@ -700,8 +698,7 @@ package body Lib.Load is Unit_File_Name => Fname, Unit_Name => Uname_Actual, Version => Source_Checksum (Src_Ind), - OA_Setting => 'O', - SPARK_Mode_Pragma => Empty); + OA_Setting => 'O'); -- Parse the new unit diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index 981656552af..f69e4ac16ec 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.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- -- @@ -95,8 +95,7 @@ package body Lib.Writ is Serial_Number => 0, Version => 0, Error_Location => No_Location, - OA_Setting => 'O', - SPARK_Mode_Pragma => Empty); + OA_Setting => 'O'); end Add_Preprocessing_Dependency; ------------------------------ @@ -153,8 +152,7 @@ package body Lib.Writ is Serial_Number => 0, Version => 0, Error_Location => No_Location, - OA_Setting => 'O', - SPARK_Mode_Pragma => Empty); + OA_Setting => 'O'); -- Parse system.ads so that the checksum is set right. Style checks are -- not applied. The Ekind is set to ensure that this reference is always diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index 3ee4125f59f..54480e485bf 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- 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- -- @@ -811,7 +811,6 @@ private Filler : Boolean; Loading : Boolean; OA_Setting : Character; - SPARK_Mode_Pragma : Node_Id; end record; -- The following representation clause ensures that the above record @@ -841,10 +840,9 @@ private Filler at 61 range 0 .. 7; OA_Setting at 62 range 0 .. 7; Loading at 63 range 0 .. 7; - SPARK_Mode_Pragma at 64 range 0 .. 31; end record; - for Unit_Record'Size use 68 * 8; + for Unit_Record'Size use 64 * 8; -- This ensures that we did not leave out any fields package Units is new Table.Table ( diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index 40d6cfc16ab..0c8a3ee43c0 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.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- -- @@ -864,6 +864,10 @@ package body Rtsfind is -- Load_RTU -- -------------- + -- 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 Load_RTU (U_Id : RTU_Id; Id : RE_Id := RE_Null; @@ -926,7 +930,10 @@ package body Rtsfind is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Save_GM : constant Ghost_Mode_Type := Ghost_Mode; + Save_SM : constant SPARK_Mode_Type := SPARK_Mode; + Save_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save Ghost and SPARK mode-related data to restore on exit -- Start of processing for Load_RTU @@ -940,6 +947,7 @@ package body Rtsfind is -- Provide a clean environment for the unit Install_Ghost_Mode (None); + Install_SPARK_Mode (None, Empty); -- Note if secondary stack is used @@ -1042,7 +1050,8 @@ package body Rtsfind is Set_Is_Potentially_Use_Visible (U.Entity, True); end if; - Restore_Ghost_Mode (Save_Ghost_Mode); + Restore_Ghost_Mode (Save_GM); + Restore_SPARK_Mode (Save_SM, Save_SMP); end Load_RTU; -------------------- diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 9b7c4903974..eb6c8c41164 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.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- -- @@ -102,8 +102,8 @@ package body Sem is -- Ghost mode. procedure Analyze (N : Node_Id) is - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit begin Debug_A_Entry ("analyzing ", N); @@ -120,8 +120,7 @@ package body Sem is -- marked as Ghost. if Is_Declaration (N) then - Mark_And_Set_Ghost_Declaration (N, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Declaration (N); end if; -- Otherwise processing depends on the node kind @@ -762,9 +761,7 @@ package body Sem is Expand_SPARK_Potential_Renaming (N); end if; - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Restore_Ghost_Mode (Saved_GM); end Analyze; -- Version with check(s) suppressed diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 3559e8e7f09..c4ae58a2030 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.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- -- @@ -2058,6 +2058,10 @@ package body Sem_Ch10 is -- context before analyzing the proper body itself. On exit, we remove only -- the explicit context of the subunit. + -- 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 Analyze_Subunit (N : Node_Id) is Lib_Unit : constant Node_Id := Library_Unit (N); Par_Unit : constant Entity_Id := Current_Scope; @@ -2290,6 +2294,12 @@ package body Sem_Ch10 is Pop_Scope; end Remove_Scope; + 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 + -- eclosing scopes and contexts to provide a clean environment for the + -- context of the subunit will eliminate any previously set SPARK_Mode. + -- Start of processing for Analyze_Subunit begin @@ -2386,6 +2396,12 @@ package body Sem_Ch10 is end if; Generate_Parent_References (Unit (N), Par_Unit); + + -- Reinstall the SPARK_Mode which was in effect prior to any scope and + -- context manipulations. + + Install_SPARK_Mode (Saved_SM, Saved_SMP); + Analyze (Proper_Body (Unit (N))); Remove_Context (N); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 2f2262d925e..e5981370c50 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3598,49 +3598,17 @@ package body Sem_Ch12 is -- Analyze_Package_Instantiation -- ----------------------------------- - -- WARNING: This routine manages Ghost regions. Return statements must be - -- replaced by gotos which jump to the end of the routine and restore the - -- Ghost mode. + -- 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_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)); - - Env_Installed : Boolean := False; - Parent_Installed : Boolean := False; - Renaming_List : List_Id; - Unit_Renaming : Node_Id; - Needs_Body : Boolean; - Inline_Now : Boolean := False; Has_Inline_Always : Boolean := False; - Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; - -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance 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 @@ -3662,7 +3630,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 @@ -3691,8 +3659,35 @@ package body Sem_Ch12 is -- Local declarations - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + 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 @@ -3771,8 +3766,7 @@ package body Sem_Ch12 is -- any nodes generated during analysis and expansion are marked as -- Ghost. - Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit); -- Verify that it is the name of a generic package @@ -4049,7 +4043,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 @@ -4098,7 +4092,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 @@ -4466,14 +4461,10 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - Style_Check := Save_Style_Check; - - if Mode_Set then - Restore_Ghost_Mode (Mode); - 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 => @@ -4485,20 +4476,20 @@ package body Sem_Ch12 is Restore_Env; end if; - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - Style_Check := Save_Style_Check; - - if Mode_Set then - Restore_Ghost_Mode (Mode); - 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; 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; @@ -4509,26 +4500,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 @@ -4672,8 +4664,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; @@ -4812,7 +4804,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 @@ -4882,9 +4873,9 @@ package body Sem_Ch12 is -- Analyze_Subprogram_Instantiation -- -------------------------------------- - -- WARNING: This routine manages Ghost regions. Return statements must be - -- replaced by gotos which jump to the end of the routine and restore the - -- Ghost mode. + -- 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; @@ -5130,15 +5121,12 @@ package body Sem_Ch12 is -- Local variables - Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; - -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance 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 - - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + 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 @@ -5180,8 +5168,7 @@ package body Sem_Ch12 is -- that any nodes generated during analysis and expansion are marked as -- Ghost. - Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit); Generate_Reference (Gen_Unit, Gen_Id); @@ -5446,13 +5433,9 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - - if Mode_Set then - Restore_Ghost_Mode (Mode); - 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 => @@ -5464,13 +5447,9 @@ package body Sem_Ch12 is Restore_Env; end if; - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - SPARK_Mode := Save_SM; - SPARK_Mode_Pragma := Save_SMP; - - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Subprogram_Instantiation; ------------------------- @@ -10847,9 +10826,9 @@ package body Sem_Ch12 is -- Instantiate_Package_Body -- ------------------------------ - -- WARNING: This routine manages Ghost regions. Return statements must be - -- replaced by gotos which jump to the end of the routine and restore the - -- Ghost mode. + -- 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; @@ -10865,9 +10844,9 @@ package body Sem_Ch12 is Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); Loc : constant Source_Ptr := Sloc (Inst_Node); - Save_ISMP : constant Boolean := + Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; - Save_Style_Check : constant Boolean := Style_Check; + Saved_Style_Check : constant Boolean := Style_Check; procedure Check_Initialized_Types; -- In a generic package body, an entity of a generic private type may @@ -10939,15 +10918,18 @@ package body Sem_Ch12 is -- Local variables - Act_Body : Node_Id; - Act_Body_Id : Entity_Id; - Act_Body_Name : Node_Id; - Gen_Body : Node_Id; - Gen_Body_Id : Node_Id; - Mode : Ghost_Mode_Type; - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; - + 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; @@ -10970,7 +10952,7 @@ package body Sem_Ch12 is -- the mode now to ensure that any nodes generated during instantiation -- are properly marked as Ghost. - Set_Ghost_Mode (Act_Decl_Id, Mode); + Set_Ghost_Mode (Act_Decl_Id); Expander_Mode_Save_And_Set (Body_Info.Expander_Status); @@ -10984,8 +10966,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 @@ -11264,19 +11248,19 @@ package body Sem_Ch12 is Expander_Mode_Restore; <> - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - Style_Check := Save_Style_Check; - - Restore_Ghost_Mode (Mode); + 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 regions. Return statements must be - -- replaced by gotos which jump to the end of the routine and restore the - -- Ghost mode. + -- 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; @@ -11292,16 +11276,20 @@ package body Sem_Ch12 is Pack_Id : constant Entity_Id := Defining_Unit_Name (Parent (Act_Decl)); - Saved_ISMP : constant Boolean := - Ignore_SPARK_Mode_Pragmas_In_Instance; - Saved_Style_Check : constant Boolean := Style_Check; + 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; Act_Body : Node_Id; Act_Body_Id : Entity_Id; Gen_Body : Node_Id; Gen_Body_Id : Node_Id; - Mode : Ghost_Mode_Type; Pack_Body : Node_Id; Par_Ent : Entity_Id := Empty; Par_Vis : Boolean := False; @@ -11324,7 +11312,7 @@ package body Sem_Ch12 is -- the mode now to ensure that any nodes generated during instantiation -- are properly marked as Ghost. - Set_Ghost_Mode (Act_Decl_Id, Mode); + Set_Ghost_Mode (Act_Decl_Id); Expander_Mode_Save_And_Set (Body_Info.Expander_Status); @@ -11338,8 +11326,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 @@ -11575,9 +11565,9 @@ package body Sem_Ch12 is <> 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; - - Restore_Ghost_Mode (Mode); end Instantiate_Subprogram_Body; ---------------------- @@ -15413,13 +15403,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 @@ -15440,14 +15435,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 := diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index c80ca5c00bf..833770624e8 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -8566,7 +8566,8 @@ package body Sem_Ch13 is -- Local variables - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit -- Start of processing for Build_Predicate_Functions @@ -8583,7 +8584,7 @@ package body Sem_Ch13 is -- The related type may be subject to pragma Ghost. Set the mode now to -- ensure that the predicate functions are properly marked as Ghost. - Set_Ghost_Mode (Typ, Mode); + Set_Ghost_Mode (Typ); -- Prepare to construct predicate expression @@ -8937,7 +8938,7 @@ package body Sem_Ch13 is end; end if; - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Build_Predicate_Functions; ------------------------------------------ @@ -8953,16 +8954,18 @@ package body Sem_Ch13 is is Loc : constant Source_Ptr := Sloc (Typ); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Func_Decl : Node_Id; Func_Id : Entity_Id; - Mode : Ghost_Mode_Type; Spec : Node_Id; begin -- The related type may be subject to pragma Ghost. Set the mode now to -- ensure that the predicate functions are properly marked as Ghost. - Set_Ghost_Mode (Typ, Mode); + Set_Ghost_Mode (Typ); Func_Id := Make_Defining_Identifier (Loc, @@ -8996,7 +8999,7 @@ package body Sem_Ch13 is Insert_After (Parent (Typ), Func_Decl); Analyze (Func_Decl); - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); return Func_Decl; end Build_Predicate_Function_Declaration; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 7a9e52d43aa..5379a856bd8 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.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- -- @@ -3688,8 +3688,9 @@ package body Sem_Ch3 is -- Local variables - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Related_Id : Entity_Id; -- Start of processing for Analyze_Object_Declaration @@ -3760,8 +3761,7 @@ package body Sem_Ch3 is -- The object declaration is Ghost when it completes a deferred Ghost -- constant. - Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Completion (N, Prev_Entity); Constant_Redeclaration (Id, N, T); @@ -4700,9 +4700,7 @@ package body Sem_Ch3 is Check_No_Hidden_State (Id); end if; - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Restore_Ghost_Mode (Saved_GM); end Analyze_Object_Declaration; --------------------------- @@ -19858,15 +19856,16 @@ package body Sem_Ch3 is -- Local variables + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Full_Indic : Node_Id; Full_Parent : Entity_Id; - Mode : Ghost_Mode_Type; Priv_Parent : Entity_Id; -- Start of processing for Process_Full_View begin - Mark_And_Set_Ghost_Completion (N, Priv_T, Mode); + Mark_And_Set_Ghost_Completion (N, Priv_T); -- First some sanity checks that must be done after semantic -- decoration of the full view and thus cannot be placed with other @@ -20519,7 +20518,7 @@ package body Sem_Ch3 is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Process_Full_View; ----------------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 33282a0a698..27c3a530915 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.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- -- @@ -284,7 +284,8 @@ package body Sem_Ch5 is -- Local variables - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit -- Start of processing for Analyze_Assignment @@ -310,7 +311,7 @@ package body Sem_Ch5 is Current_Assignment := Empty; end if; - Mark_And_Set_Ghost_Assignment (N, Mode); + Mark_And_Set_Ghost_Assignment (N); Analyze (Rhs); -- Ensure that we never do an assignment on a variable marked as @@ -939,7 +940,7 @@ package body Sem_Ch5 is Analyze_Dimension (N); <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); -- If the right-hand side contains target names, expansion has been -- disabled to prevent expansion that might move target names out of diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index e52d285a48d..300f6def70c 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.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- -- @@ -1553,9 +1553,12 @@ package body Sem_Ch6 is Actuals : constant List_Id := Parameter_Associations (N); Loc : constant Source_Ptr := Sloc (N); P : constant Node_Id := Name (N); - Actual : Node_Id; - Mode : Ghost_Mode_Type; - New_N : Node_Id; + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + + Actual : Node_Id; + New_N : Node_Id; -- Start of processing for Analyze_Procedure_Call @@ -1598,7 +1601,7 @@ package body Sem_Ch6 is -- Set the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Mark_And_Set_Ghost_Procedure_Call (N, Mode); + Mark_And_Set_Ghost_Procedure_Call (N); -- Otherwise analyze the parameters @@ -1793,7 +1796,7 @@ package body Sem_Ch6 is end if; <> - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Analyze_Procedure_Call; ------------------------------ @@ -3314,9 +3317,10 @@ package body Sem_Ch6 is -- Local variables - Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + -- Save the Ghost and SPARK mode-related data to restore on exit -- Start of processing for Analyze_Subprogram_Body_Helper @@ -3368,8 +3372,7 @@ package body Sem_Ch6 is -- the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Body (N, Spec_Id); Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id)); @@ -3414,8 +3417,7 @@ package body Sem_Ch6 is -- Ghost. Set the mode now to ensure that any nodes generated -- during analysis and expansion are properly marked as Ghost. - Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Body (N, Spec_Id); else Spec_Id := Find_Corresponding_Spec (N); @@ -3425,8 +3427,7 @@ package body Sem_Ch6 is -- Ghost. Set the mode now to ensure that any nodes generated -- during analysis and expansion are properly marked as Ghost. - Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Body (N, Spec_Id); -- In GNATprove mode, if the body has no previous spec, create -- one so that the inlining machinery can operate properly. @@ -3527,8 +3528,7 @@ package body Sem_Ch6 is -- the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); - Mode_Set := True; + Mark_And_Set_Ghost_Body (N, Spec_Id); end if; end if; @@ -4447,11 +4447,8 @@ package body Sem_Ch6 is end if; <> - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - - if Mode_Set then - Restore_Ghost_Mode (Mode); - end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); end Analyze_Subprogram_Body_Helper; ------------------------------------ diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 260f923beae..2174f2b08f6 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.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- -- @@ -539,12 +539,14 @@ package body Sem_Ch7 is -- Local variables - Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + -- Save the Ghost and SPARK mode-related data to restore on exit Body_Id : Entity_Id; HSS : Node_Id; Last_Spec_Entity : Entity_Id; - Mode : Ghost_Mode_Type; New_N : Node_Id; Pack_Decl : Node_Id; Spec_Id : Entity_Id; @@ -647,7 +649,7 @@ package body Sem_Ch7 is -- the mode now to ensure that any nodes generated during analysis and -- expansion are properly flagged as ignored Ghost. - Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); + Mark_And_Set_Ghost_Body (N, Spec_Id); Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Style.Check_Identifier (Body_Id, Spec_Id); @@ -941,9 +943,8 @@ package body Sem_Ch7 is end if; end if; - Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; - - Restore_Ghost_Mode (Mode); + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Restore_Ghost_Mode (Saved_GM); end Analyze_Package_Body_Helper; --------------------------------- diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 45241c3e529..26a6852cbe4 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -1937,8 +1937,11 @@ package body Sem_Elab is -- Check_Elab_Calls -- ---------------------- + -- WARNING: This routine manages SPARK regions + procedure Check_Elab_Calls is - Save_SPARK_Mode : SPARK_Mode_Type; + Saved_SM : SPARK_Mode_Type; + Saved_SMP : Node_Id; begin -- If expansion is disabled, do not generate any checks, unless we @@ -1966,9 +1969,10 @@ package body Sem_Elab is From_Elab_Code := Delay_Check.Table (J).From_Elab_Code; In_Task_Activation := Delay_Check.Table (J).In_Task_Activation; - -- Set appropriate value of SPARK_Mode + Saved_SM := SPARK_Mode; + Saved_SMP := SPARK_Mode_Pragma; - Save_SPARK_Mode := SPARK_Mode; + -- Set appropriate value of SPARK_Mode if Delay_Check.Table (J).From_SPARK_Code then SPARK_Mode := On; @@ -1980,7 +1984,7 @@ package body Sem_Elab is Outer_Scope => Delay_Check.Table (J).Outer_Scope, Orig_Ent => Delay_Check.Table (J).Orig_Ent); - SPARK_Mode := Save_SPARK_Mode; + Restore_SPARK_Mode (Saved_SM, Saved_SMP); Pop_Scope; end loop; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 133662503c6..da8bd89d5a4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -472,8 +472,10 @@ package body Sem_Prag is CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + CCase : Node_Id; - Mode : Ghost_Mode_Type; Restore_Scope : Boolean := False; -- Start of processing for Analyze_Contract_Cases_In_Decl_Part @@ -490,7 +492,7 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N, Mode); + Set_Ghost_Mode (N); -- Single and multiple contract cases must appear in aggregate form. If -- this is not the case, then either the parser of the analysis of the @@ -537,7 +539,8 @@ package body Sem_Prag is end if; Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Mode); + + Restore_Ghost_Mode (Saved_GM); end Analyze_Contract_Cases_In_Decl_Part; ---------------------------------- @@ -2672,7 +2675,8 @@ package body Sem_Prag is Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); - Mode : Ghost_Mode_Type; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit begin -- Do not analyze the pragma multiple times @@ -2686,7 +2690,7 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N, Mode); + Set_Ghost_Mode (N); -- The expression is preanalyzed because it has not been moved to its -- final place yet. A direct analysis may generate side effects and this @@ -2695,7 +2699,7 @@ package body Sem_Prag is Preanalyze_Assert_Expression (Expr, Standard_Boolean); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Analyze_Initial_Condition_In_Decl_Part; -------------------------------------- @@ -12662,10 +12666,12 @@ package body Sem_Prag is -- restore the Ghost mode. when Pragma_Check => Check : declare + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Cname : Name_Id; Eloc : Source_Ptr; Expr : Node_Id; - Mode : Ghost_Mode_Type; Str : Node_Id; begin @@ -12673,7 +12679,7 @@ package body Sem_Prag is -- the mode now to ensure that any nodes generated during analysis -- and expansion are marked as Ghost. - Set_Ghost_Mode (N, Mode); + Set_Ghost_Mode (N); GNAT_Pragma; Check_At_Least_N_Arguments (2); @@ -12857,7 +12863,7 @@ package body Sem_Prag is In_Assertion_Expr := In_Assertion_Expr - 1; end if; - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Check; -------------------------- @@ -24031,8 +24037,10 @@ package body Sem_Prag is Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the Ghost mode to restore on exit + Errors : Nat; - Mode : Ghost_Mode_Type; Restore_Scope : Boolean := False; -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part @@ -24049,7 +24057,7 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N, Mode); + Set_Ghost_Mode (N); -- Ensure that the subprogram and its formals are visible when analyzing -- the expression of the pragma. @@ -24120,7 +24128,7 @@ package body Sem_Prag is Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Mode); + Restore_Ghost_Mode (Saved_GM); end Analyze_Pre_Post_Condition_In_Decl_Part; ------------------------------------------ diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d2cdf5520b2..7c050d45e21 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -11694,6 +11694,16 @@ package body Sem_Util is end loop; end Install_Generic_Formals; + ------------------------ + -- Install_SPARK_Mode -- + ------------------------ + + procedure Install_SPARK_Mode (Mode : SPARK_Mode_Type; Prag : Node_Id) is + begin + SPARK_Mode := Mode; + SPARK_Mode_Pragma := Prag; + end Install_SPARK_Mode; + ----------------------------- -- Is_Actual_Out_Parameter -- ----------------------------- @@ -19830,9 +19840,13 @@ package body Sem_Util is -- Restore_SPARK_Mode -- ------------------------ - procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type) is + procedure Restore_SPARK_Mode + (Mode : SPARK_Mode_Type; + Prag : Node_Id) + is begin - SPARK_Mode := Mode; + SPARK_Mode := Mode; + SPARK_Mode_Pragma := Prag; end Restore_SPARK_Mode; -------------------------------- @@ -20156,28 +20170,23 @@ package body Sem_Util is end if; end Same_Value; - ----------------------------- - -- Save_SPARK_Mode_And_Set -- - ----------------------------- + -------------------- + -- Set_SPARK_Mode -- + -------------------- - procedure Save_SPARK_Mode_And_Set - (Context : Entity_Id; - Mode : out SPARK_Mode_Type) - is + procedure Set_SPARK_Mode (Context : Entity_Id) is begin - -- Save the current mode in effect - - Mode := SPARK_Mode; - -- Do not consider illegal or partially decorated constructs if Ekind (Context) = E_Void or else Error_Posted (Context) then null; elsif Present (SPARK_Pragma (Context)) then - SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context)); + Install_SPARK_Mode + (Mode => Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context)), + Prag => SPARK_Pragma (Context)); end if; - end Save_SPARK_Mode_And_Set; + end Set_SPARK_Mode; ------------------------- -- Scalar_Part_Present -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index e494f14bc84..c8a484d260b 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1331,6 +1331,9 @@ package Sem_Util is -- Install both the generic formal parameters and the formal parameters of -- generic subprogram Subp_Id into visibility. + procedure Install_SPARK_Mode (Mode : SPARK_Mode_Type; Prag : Node_Id); + -- Establish the SPARK_Mode and SPARK_Mode_Pragma currently in effect + function Is_Actual_Out_Parameter (N : Node_Id) return Boolean; -- Determines if N is an actual parameter of out mode in a subprogram call @@ -2209,9 +2212,11 @@ package Sem_Util is procedure Reset_Analyzed_Flags (N : Node_Id); -- Reset the Analyzed flags in all nodes of the tree whose root is N - procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type); - -- Set the current SPARK_Mode to whatever Mode denotes. This routime must - -- be used in tandem with Save_SPARK_Mode_And_Set. + procedure Restore_SPARK_Mode + (Mode : SPARK_Mode_Type; + Prag : Node_Id); + -- Set the current SPARK_Mode to Mode and SPARK_Mode_Pragma to Prag. This + -- routine must be used in tandem with Set_SPARK_Mode. function Returns_Unconstrained_Type (Subp : Entity_Id) return Boolean; -- Return true if Subp is a function that returns an unconstrained type @@ -2269,13 +2274,6 @@ package Sem_Util is -- A result of False does not necessarily mean they have different values, -- just that it is not possible to determine they have the same value. - procedure Save_SPARK_Mode_And_Set - (Context : Entity_Id; - Mode : out SPARK_Mode_Type); - -- Save the current SPARK_Mode in effect in Mode. Establish the SPARK_Mode - -- (if any) of a package or a subprogram denoted by Context. This routine - -- must be used in tandem with Restore_SPARK_Mode. - function Scalar_Part_Present (T : Entity_Id) return Boolean; -- Tests if type T can be determined at compile time to have at least one -- scalar part in the sense of the Valid_Scalars attribute. Returns True if @@ -2371,6 +2369,11 @@ package Sem_Util is -- value from T2 to T1. It does NOT copy the RM_Size field, which must be -- separately set if this is required to be copied also. + procedure Set_SPARK_Mode (Context : Entity_Id); + -- Establish the SPARK_Mode and SPARK_Mode_Pragma (if any) of a package or + -- a subprogram denoted by Context. This routine must be used in tandem + -- with Restore_SPARK_Mode. + function Scope_Is_Transient return Boolean; -- True if the current scope is transient