From cf9a473e6494aef4d6e36dfdab64b3c42bfe5958 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 25 Apr 2017 12:49:34 +0200 Subject: [PATCH] [multiple changes] 2017-04-25 Hristian Kirtchev * einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas. (Ignore_SPARK_Mode_Pragmas): New routine. (Set_Ignore_SPARK_Mode_Pragmas): New routine. (Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas. * einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update related entities. (Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline. (Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline. * opt.ads Rename flag Ignore_Pragma_SPARK_Mode to Ignore_SPARK_Mode_Pragmas_In_Instance. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either the corresponding spec or the body must ignore all SPARK_Mode pragmas found within. (Analyze_Subprogram_Declaration): Mark the spec when it needs to ignore all SPARK_Mode pragmas found within to allow the body to infer this property in case it is instantiated or inlined later. * sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the corresponding spec also ignored all SPARK_Mode pragmas found within. (Analyze_Package_Declaration): Mark the spec when it needs to ignore all SPARK_Mode pragmas found within to allow the body to infer this property in case it is instantiated or inlined later. * sem_ch12.adb (Analyze_Formal_Package_Declaration): Save and restore the value of flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the formal spec when it needs to ignore all SPARK_Mode pragmas found within to allow the body to infer this property in case it is instantiated or inlined later. (Analyze_Package_Instantiation): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the instance spec when it needs to ignore all SPARK_Mode pragmas found within to allow the body to infer this property in case it is instantiated or inlined later. (Analyze_Subprogram_Instantiation): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the instance spec and anonymous package when they need to ignore all SPARK_Mode pragmas found within to allow the body to infer this property in case it is instantiated or inlined later. (Instantiate_Package_Body): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the corresponding instance spec also ignored all SPARK_Mode pragmas found within. (Instantiate_Subprogram_Body): Save and restore the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the corresponding instance spec also ignored all SPARK_Mode pragmas found within. * sem_prag.adb (Analyze_Pragma): Update the reference to Ignore_Pragma_SPARK_Mode. * sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored all SPARK_Mode pragmas defined within yields mode "off". 2017-04-25 Hristian Kirtchev * bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting. 2017-04-25 Bob Duff * exp_atag.adb (Build_CW_Membership): Add "Suppress => All_Checks" to avoid generating unnecessary checks. * exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress => All_Checks". * sem.ads: Fix comment. * expander.ads: Fix comment. * exp_atag.ads: Fix comment: "Index = 0" should be "Index >= 0". 2017-04-25 Gary Dismukes * s-taprop-linux.adb: Minor editorial fixes. From-SVN: r247182 --- gcc/ada/ChangeLog | 82 ++++++++++++++++++++++ gcc/ada/bindgen.adb | 4 +- gcc/ada/einfo.adb | 49 ++++++++++++- gcc/ada/einfo.ads | 29 ++++++-- gcc/ada/errout.adb | 4 ++ gcc/ada/exp_atag.adb | 13 ++-- gcc/ada/exp_atag.ads | 4 +- gcc/ada/exp_ch4.adb | 6 +- gcc/ada/exp_dbug.adb | 18 ++--- gcc/ada/expander.ads | 8 +-- gcc/ada/fname.adb | 23 +++--- gcc/ada/opt.ads | 12 ++-- gcc/ada/s-taprop-linux.adb | 4 +- gcc/ada/sem.ads | 20 +++--- gcc/ada/sem_ch12.adb | 140 ++++++++++++++++++++++--------------- gcc/ada/sem_ch6.adb | 44 ++++++++++-- gcc/ada/sem_ch7.adb | 21 ++++++ gcc/ada/sem_prag.adb | 2 +- gcc/ada/sem_util.adb | 16 ++++- 19 files changed, 377 insertions(+), 122 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9e8581879dd..bec26bcc770 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,85 @@ +2017-04-25 Hristian Kirtchev + + * einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas. + (Ignore_SPARK_Mode_Pragmas): New routine. + (Set_Ignore_SPARK_Mode_Pragmas): New routine. + (Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas. + * einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update + related entities. + (Ignore_SPARK_Mode_Pragmas): New routine + along with pragma Inline. + (Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline. + * opt.ads Rename flag Ignore_Pragma_SPARK_Mode to + Ignore_SPARK_Mode_Pragmas_In_Instance. + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): + Save and restore the value of global flag + Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value + of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either + the corresponding spec or the body must ignore all SPARK_Mode + pragmas found within. + (Analyze_Subprogram_Declaration): Mark + the spec when it needs to ignore all SPARK_Mode pragmas found + within to allow the body to infer this property in case it is + instantiated or inlined later. + * sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the + value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set + the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance + when the corresponding spec also ignored all SPARK_Mode pragmas + found within. + (Analyze_Package_Declaration): Mark the spec when + it needs to ignore all SPARK_Mode pragmas found within to allow + the body to infer this property in case it is instantiated or + inlined later. + * sem_ch12.adb (Analyze_Formal_Package_Declaration): + Save and restore the value of flag + Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the + formal spec when it needs to ignore all SPARK_Mode + pragmas found within to allow the body to infer this + property in case it is instantiated or inlined later. + (Analyze_Package_Instantiation): Save and restore the value + of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark + the instance spec when it needs to ignore all SPARK_Mode + pragmas found within to allow the body to infer this + property in case it is instantiated or inlined later. + (Analyze_Subprogram_Instantiation): Save and restore the value + of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the + instance spec and anonymous package when they need to ignore + all SPARK_Mode pragmas found within to allow the body to infer + this property in case it is instantiated or inlined later. + (Instantiate_Package_Body): Save and restore the value of global + flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of + global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the + corresponding instance spec also ignored all SPARK_Mode pragmas + found within. + (Instantiate_Subprogram_Body): Save and restore the + value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set + the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance + when the corresponding instance spec also ignored all SPARK_Mode + pragmas found within. + * sem_prag.adb (Analyze_Pragma): Update the reference to + Ignore_Pragma_SPARK_Mode. + * sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored + all SPARK_Mode pragmas defined within yields mode "off". + +2017-04-25 Hristian Kirtchev + + * bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting. + +2017-04-25 Bob Duff + + * exp_atag.adb (Build_CW_Membership): Add "Suppress => + All_Checks" to avoid generating unnecessary checks. + * exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress => + All_Checks". + * sem.ads: Fix comment. + * expander.ads: Fix comment. + * exp_atag.ads: Fix comment: "Index = 0" should be + "Index >= 0". + +2017-04-25 Gary Dismukes + + * s-taprop-linux.adb: Minor editorial fixes. + 2017-04-25 Eric Botcazou * sem_util.adb (New_Copy_Tree): Put back the declarations of the diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb index 8ada7c1ae39..5544c8244b7 100644 --- a/gcc/ada/bindgen.adb +++ b/gcc/ada/bindgen.adb @@ -1120,8 +1120,8 @@ package body Bindgen is -- where we increment the elaboration entity if one exists. -- Likewise for lone specs with an elaboration entity defined - -- despite No_Elaboration_Code, e.g. when requested to - -- preserve control flow. + -- despite No_Elaboration_Code, e.g. when requested to preserve + -- control flow. if (U.Utype = Is_Body or else U.Utype = Is_Spec_Only) and then Units.Table (Unum_Spec).Set_Elab_Entity diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 118e09fde5c..5638bc09e08 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -620,7 +620,7 @@ package body Einfo is -- Body_Needed_For_Inlining Flag299 -- Has_Private_Extension Flag300 - -- (unused) Flag301 + -- Ignore_SPARK_Mode_Pragmas Flag301 -- (unused) Flag302 -- (unused) Flag303 -- (unused) Flag304 @@ -1981,6 +1981,29 @@ package body Einfo is return Node4 (Id); end Homonym; + function Ignore_SPARK_Mode_Pragmas (Id : E) return B is + begin + pragma Assert + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Operator, + E_Procedure, + E_Subprogram_Body) + or else + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); + return Flag301 (Id); + end Ignore_SPARK_Mode_Pragmas; + function Import_Pragma (Id : E) return E is begin pragma Assert (Is_Subprogram (Id)); @@ -5073,6 +5096,29 @@ package body Einfo is Set_Elist24 (Id, V); end Set_Incomplete_Actuals; + procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is + begin + pragma Assert + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Operator, + E_Procedure, + E_Subprogram_Body) + or else + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); + Set_Flag301 (Id, V); + end Set_Ignore_SPARK_Mode_Pragmas; + procedure Set_Import_Pragma (Id : E; V : E) is begin pragma Assert (Is_Subprogram (Id)); @@ -9402,6 +9448,7 @@ package body Einfo is W ("Has_Visible_Refinement", Flag263 (Id)); W ("Has_Volatile_Components", Flag87 (Id)); W ("Has_Xref_Entry", Flag182 (Id)); + W ("Ignore_SPARK_Mode_Pragmas", Flag301 (Id)); W ("In_Package_Body", Flag48 (Id)); W ("In_Private_Part", Flag45 (Id)); W ("In_Use", Flag8 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index dc63408bd49..9d8a33c7075 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2164,6 +2164,13 @@ package Einfo is -- scopes. Homonyms in the same scope are overloaded. Used for name -- resolution and for the generation of debugging information. +-- Ignore_SPARK_Mode_Pragmas (Flag301) +-- Present in concurrent type, entry, operator, [generic] package, +-- package body, [generic] subprogram, and subprogram body entities. +-- Set when the entity appears in an instance subject to SPARK_Mode +-- "off" and indicates that all SPARK_Mode pragmas found within must +-- be ignored. + -- Implementation_Base_Type (synthesized) -- Applies to all entities. For types, similar to Base_Type, but never -- returns a private type when applied to a non-private type. Instead in @@ -5922,14 +5929,15 @@ package Einfo is -- Extra_Formals (Node28) -- Contract (Node34) -- SPARK_Pragma (Node40) (protected kind) - -- Needs_No_Actuals (Flag22) - -- Uses_Sec_Stack (Flag95) -- Default_Expressions_Processed (Flag108) -- Entry_Accepted (Flag152) - -- Sec_Stack_Needed_For_Return (Flag167) -- Has_Expanded_Contract (Flag240) - -- SPARK_Pragma_Inherited (Flag265) (protected kind) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Is_Entry_Wrapper (Flag297) + -- Needs_No_Actuals (Flag22) + -- Sec_Stack_Needed_For_Return (Flag167) + -- SPARK_Pragma_Inherited (Flag265) (protected kind) + -- Uses_Sec_Stack (Flag95) -- Address_Clause (synth) -- Entry_Index_Type (synth) -- First_Formal (synth) @@ -6056,6 +6064,7 @@ package Einfo is -- Has_Nested_Subprogram (Flag282) -- Has_Out_Or_In_Out_Parameter (Flag110) -- Has_Recursive_Call (Flag143) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Is_Abstract_Subprogram (Flag19) (non-generic case only) -- Is_Called (Flag102) (non-generic case only) -- Is_Constructor (Flag76) @@ -6209,6 +6218,7 @@ package Einfo is -- SPARK_Pragma (Node40) -- Default_Expressions_Processed (Flag108) -- Has_Nested_Subprogram (Flag282) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Is_Intrinsic_Subprogram (Flag64) -- Is_Machine_Code_Subprogram (Flag137) -- Is_Primitive (Flag218) @@ -6272,6 +6282,7 @@ package Einfo is -- Has_Forward_Instantiation (Flag175) -- Has_Master_Entity (Flag21) -- Has_RACW (Flag214) (non-generic case only) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- In_Package_Body (Flag48) -- In_Use (Flag8) -- Is_Instantiated (Flag126) @@ -6299,6 +6310,7 @@ package Einfo is -- SPARK_Aux_Pragma (Node41) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Subprogram_Descriptors (Flag50) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- SPARK_Aux_Pragma_Inherited (Flag266) -- SPARK_Pragma_Inherited (Flag265) -- Scope_Depth (synth) @@ -6367,6 +6379,7 @@ package Einfo is -- Has_Master_Entity (Flag21) -- Has_Nested_Block_With_Handler (Flag101) -- Has_Nested_Subprogram (Flag282) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Is_Abstract_Subprogram (Flag19) (non-generic case only) -- Is_Asynchronous (Flag81) -- Is_Called (Flag102) (non-generic case only) @@ -6406,6 +6419,7 @@ package Einfo is -- E_Protected_Body -- SPARK_Pragma (Node40) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- SPARK_Pragma_Inherited (Flag265) -- (any others??? First/Last Entity, Scope_Depth???) @@ -6427,6 +6441,7 @@ package Einfo is -- Entry_Max_Queue_Lengths_Array (Node35) -- SPARK_Pragma (Node40) -- SPARK_Aux_Pragma (Node41) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Sec_Stack_Needed_For_Return (Flag167) ??? -- SPARK_Aux_Pragma_Inherited (Flag266) -- SPARK_Pragma_Inherited (Flag265) @@ -6557,6 +6572,7 @@ package Einfo is -- E_Task_Body -- Contract (Node34) -- SPARK_Pragma (Node40) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- SPARK_Pragma_Inherited (Flag265) -- (any others??? First/Last Entity, Scope_Depth???) @@ -6580,6 +6596,7 @@ package Einfo is -- Delay_Cleanups (Flag114) -- Has_Master_Entity (Flag21) -- Has_Storage_Size_Clause (Flag23) (base type only) + -- Ignore_SPARK_Mode_Pragmas (Flag301) -- Sec_Stack_Needed_For_Return (Flag167) ??? -- SPARK_Aux_Pragma_Inherited (Flag266) -- SPARK_Pragma_Inherited (Flag265) @@ -7103,6 +7120,7 @@ package Einfo is function Has_Xref_Entry (Id : E) return B; function Hiding_Loop_Variable (Id : E) return E; function Homonym (Id : E) return E; + function Ignore_SPARK_Mode_Pragmas (Id : E) return B; function Import_Pragma (Id : E) return E; function Incomplete_Actuals (Id : E) return L; function In_Package_Body (Id : E) return B; @@ -7788,6 +7806,7 @@ package Einfo is procedure Set_Has_Xref_Entry (Id : E; V : B := True); procedure Set_Hiding_Loop_Variable (Id : E; V : E); procedure Set_Homonym (Id : E; V : E); + procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True); procedure Set_Import_Pragma (Id : E; V : E); procedure Set_Incomplete_Actuals (Id : E; V : L); procedure Set_In_Package_Body (Id : E; V : B := True); @@ -8587,6 +8606,7 @@ package Einfo is pragma Inline (Has_Xref_Entry); pragma Inline (Hiding_Loop_Variable); pragma Inline (Homonym); + pragma Inline (Ignore_SPARK_Mode_Pragmas); pragma Inline (Import_Pragma); pragma Inline (Incomplete_Actuals); pragma Inline (In_Package_Body); @@ -9109,6 +9129,7 @@ package Einfo is pragma Inline (Set_Has_Xref_Entry); pragma Inline (Set_Hiding_Loop_Variable); pragma Inline (Set_Homonym); + pragma Inline (Set_Ignore_SPARK_Mode_Pragmas); pragma Inline (Set_Import_Pragma); pragma Inline (Set_Incomplete_Actuals); pragma Inline (Set_In_Package_Body); diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index d2c41fcb4ab..2d26d07e948 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -508,10 +508,12 @@ package body Errout is Error_Msg_Internal ("info: in inlined body #", Actual_Error_Loc, Flag_Location, Msg_Cont_Status); + elsif Is_Warning_Msg or Is_Style_Msg then Error_Msg_Internal (Warn_Insertion & "in inlined body #", Actual_Error_Loc, Flag_Location, Msg_Cont_Status); + else Error_Msg_Internal ("error in inlined body #", @@ -525,10 +527,12 @@ package body Errout is Error_Msg_Internal ("info: in instantiation #", Actual_Error_Loc, Flag_Location, Msg_Cont_Status); + elsif Is_Warning_Msg or else Is_Style_Msg then Error_Msg_Internal (Warn_Insertion & "in instantiation #", Actual_Error_Loc, Flag_Location, Msg_Cont_Status); + else Error_Msg_Internal ("instantiation error #", diff --git a/gcc/ada/exp_atag.adb b/gcc/ada/exp_atag.adb index bd5f9e26eca..dd25237fd8f 100644 --- a/gcc/ada/exp_atag.adb +++ b/gcc/ada/exp_atag.adb @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2006-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 2006-2016, 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- -- @@ -178,7 +178,7 @@ package body Exp_Atag is -- Typ_TSD : constant Type_Specific_Data_Ptr -- := Build_TSD (Address!(Typ_Tag)); -- Index : constant Integer := Obj_TSD.Idepth - Typ_TSD.Idepth - -- Index > 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag + -- Index >= 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag Insert_Action (Related_Nod, Make_Object_Declaration (Loc, @@ -199,7 +199,8 @@ package body Exp_Atag is Constant_Present => True, Object_Definition => New_Occurrence_Of (RTE (RE_Type_Specific_Data_Ptr), Loc), - Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc)))); + Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))), + Suppress => All_Checks); Insert_Action (Related_Nod, Make_Object_Declaration (Loc, @@ -209,7 +210,8 @@ package body Exp_Atag is (RTE (RE_Type_Specific_Data_Ptr), Loc), Expression => Build_TSD (Loc, Unchecked_Convert_To (RTE (RE_Address), - Typ_Tag_Node)))); + Typ_Tag_Node))), + Suppress => All_Checks); Insert_Action (Related_Nod, Make_Object_Declaration (Loc, @@ -230,7 +232,8 @@ package body Exp_Atag is Prefix => New_Occurrence_Of (Typ_TSD, Loc), Selector_Name => New_Occurrence_Of - (RTE_Record_Component (RE_Idepth), Loc))))); + (RTE_Record_Component (RE_Idepth), Loc)))), + Suppress => All_Checks); New_Node := Make_And_Then (Loc, diff --git a/gcc/ada/exp_atag.ads b/gcc/ada/exp_atag.ads index 6551f153aa9..d53466fc39c 100644 --- a/gcc/ada/exp_atag.ads +++ b/gcc/ada/exp_atag.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2006-2011, Free Software Foundation, Inc. -- +-- Copyright (C) 2006-2016, 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- -- @@ -54,7 +54,7 @@ package Exp_Atag is -- computed in constant time by the formula: -- -- Index := TSD (Obj'Tag).Idepth - TSD (Typ'Tag).Idepth; - -- Index > 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag + -- Index >= 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag -- -- Related_Nod is the node where the implicit declaration of variable Index -- is inserted. Obj_Tag_Node is relocated. diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 1fdc50cf564..8a2698befbf 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -5859,7 +5859,8 @@ package body Exp_Ch4 is if Tagged_Type_Expansion then Tagged_Membership (N, SCIL_Node, New_N); Rewrite (N, New_N); - Analyze_And_Resolve (N, Restyp); + Analyze_And_Resolve + (N, Restyp, Suppress => All_Checks); -- Update decoration of relocated node referenced by the -- SCIL node. @@ -10908,7 +10909,8 @@ package body Exp_Ch4 is Insert_Action (N, Make_Raise_Constraint_Error (Loc, Condition => Cond, - Reason => CE_Tag_Check_Failed)); + Reason => CE_Tag_Check_Failed), + Suppress => All_Checks); end Make_Tag_Check; -- Start of processing for Tagged_Conversion diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index d2cad8893dc..ede7e2ebc78 100644 --- a/gcc/ada/exp_dbug.adb +++ b/gcc/ada/exp_dbug.adb @@ -343,8 +343,10 @@ package body Exp_Dbug is begin Enable := - Enable or else (Ekind (T) in Array_Kind - and then Present (Packed_Array_Impl_Type (T))); + Enable + or else + (Ekind (T) in Array_Kind + and then Present (Packed_Array_Impl_Type (T))); end Enable_If_Packed_Array; ---------------------- @@ -359,7 +361,7 @@ package body Exp_Dbug is elsif Nkind (N) = N_Identifier and then Scope_Contains (Scope (Entity (N)), Ent) and then (Ekind (Entity (N)) = E_Constant - or else Ekind (Entity (N)) = E_In_Parameter) + or else Ekind (Entity (N)) = E_In_Parameter) then Prepend_String_To_Buffer (Get_Name_String (Chars (Entity (N)))); @@ -375,25 +377,25 @@ package body Exp_Dbug is -- Scope_Contains -- -------------------- - function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean - is + function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean is Cur : Node_Id := Scope (Ent); + begin while Present (Cur) loop if Cur = Sc then return True; end if; + Cur := Scope (Cur); end loop; + return False; end Scope_Contains; -- Start of processing for Debug_Renaming_Declaration begin - if not Comes_From_Source (N) - and then not Needs_Debug_Info (Ent) - then + if not Comes_From_Source (N) and then not Needs_Debug_Info (Ent) then return Empty; end if; diff --git a/gcc/ada/expander.ads b/gcc/ada/expander.ads index 6c8c649ac0d..92764763daa 100644 --- a/gcc/ada/expander.ads +++ b/gcc/ada/expander.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -66,9 +66,9 @@ -- always the case). -- In both these cases, Replace or Rewrite must be used to achieve the --- of the node, since the Expander routine is only passed the Node_Id --- of the node to be expanded, and the resulting expanded Node_Id must --- be the same (the parameter to Expand is mode in, not mode in-out). +-- expansion of the node, since the Expander routine is only passed the +-- Node_Id of the node to be expanded, and the resulting expanded Node_Id +-- must be the same (the parameter to Expand is mode in, not mode in-out). -- For nodes other than subexpressions, it is not necessary to preserve the -- original tree in the Expand routines, unlike the case for modifications diff --git a/gcc/ada/fname.adb b/gcc/ada/fname.adb index 5acd813d1d7..0487085e02c 100644 --- a/gcc/ada/fname.adb +++ b/gcc/ada/fname.adb @@ -59,14 +59,13 @@ package body Fname is function Has_Internal_Extension (Fname : String) return Boolean; pragma Inline (Has_Internal_Extension); - -- True if the extension is appropriate for an internal/predefined - -- unit. That means ".ads" or ".adb" for source files, and ".ali" for - -- ALI files. + -- True if the extension is appropriate for an internal/predefined unit. + -- That means ".ads" or ".adb" for source files, and ".ali" for ALI files. function Has_Prefix (X, Prefix : String) return Boolean; pragma Inline (Has_Prefix); -- True if Prefix is at the beginning of X. For example, - -- Has_Prefix("a-filename.ads", Prefix => "a-") is True. + -- Has_Prefix ("a-filename.ads", Prefix => "a-") is True. ---------------------------- -- Has_Internal_Extension -- @@ -145,14 +144,14 @@ package body Fname is subtype Str8 is String (1 .. 8); Renaming_Names : constant array (1 .. 8) of Str8 := - ("calendar", -- Calendar - "machcode", -- Machine_Code - "unchconv", -- Unchecked_Conversion - "unchdeal", -- Unchecked_Deallocation - "directio", -- Direct_IO - "ioexcept", -- IO_Exceptions - "sequenio", -- Sequential_IO - "text_io."); -- Text_IO + ("calendar", -- Calendar + "machcode", -- Machine_Code + "unchconv", -- Unchecked_Conversion + "unchdeal", -- Unchecked_Deallocation + "directio", -- Direct_IO + "ioexcept", -- IO_Exceptions + "sequenio", -- Sequential_IO + "text_io."); -- Text_IO -- Note: the implementation is optimized to perform uniform comparisons -- on string slices whose length is known at compile time and at most 8 diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 94fdd8a065c..bb6c5b37e13 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -814,18 +814,18 @@ package Opt is -- default value appropriate to the system (in Osint.Initialize), and then -- reset if a command line switch is used to change the setting. - Ignore_Pragma_SPARK_Mode : Boolean := False; - -- GNAT - -- Set True to ignore the semantics and effects of pragma SPARK_Mode when - -- the pragma appears inside an instance whose enclosing context is subject - -- to SPARK_Mode "off". - Ignore_Rep_Clauses : Boolean := False; -- GNAT -- Set True to ignore all representation clauses. Useful when compiling -- code from foreign compilers for checking or ASIS purposes. Can be -- set True by use of -gnatI. + Ignore_SPARK_Mode_Pragmas_In_Instance : Boolean := False; + -- GNAT + -- Set True to ignore the semantics and effects of pragma SPARK_Mode when + -- the pragma appears inside an instance whose enclosing context is subject + -- to SPARK_Mode "off". This property applies to nested instances. + Ignore_Style_Checks_Pragmas : Boolean := False; -- GNAT -- Set True to ignore all Style_Checks pragmas. Can be set True by use diff --git a/gcc/ada/s-taprop-linux.adb b/gcc/ada/s-taprop-linux.adb index 00cf9ceeb5c..a435617805b 100644 --- a/gcc/ada/s-taprop-linux.adb +++ b/gcc/ada/s-taprop-linux.adb @@ -849,8 +849,8 @@ package body System.Task_Primitives.Operations is end if; end loop; - -- Cover the odd situtation if someone decides to change - -- Parameters.Max_Task_Image_Length to less than 16 characters + -- Cover the odd situation where someone decides to change + -- Parameters.Max_Task_Image_Length to less than 16 characters. if Len > Parameters.Max_Task_Image_Length then Len := Parameters.Max_Task_Image_Length; diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads index 6cd050e7fb6..be5bc33245b 100644 --- a/gcc/ada/sem.ads +++ b/gcc/ada/sem.ads @@ -165,7 +165,7 @@ ------------------ -- For certain kind of expressions, such as aggregates, we need to defer --- expansion of the aggregate and its inner expressions after the whole +-- expansion of the aggregate and its inner expressions until after the whole -- set of expressions appearing inside the aggregate have been analyzed. -- Consider, for instance the following example: -- @@ -177,17 +177,17 @@ -- repeatedly (for instance in the above aggregate "new Thing (Function_Call)" -- needs to be called 100 times.) --- The reason why this mechanism does not work is that the expanded code for --- the children is typically inserted above the parent and thus when the --- father gets expanded no re-evaluation takes place. For instance in the case --- of aggregates if "new Thing (Function_Call)" is expanded before of the --- aggregate the expanded code will be placed outside of the aggregate and --- when expanding the aggregate the loop from 1 to 100 will not surround the +-- The reason this mechanism does not work is that the expanded code for the +-- children is typically inserted above the parent and thus when the father +-- gets expanded no re-evaluation takes place. For instance in the case of +-- aggregates if "new Thing (Function_Call)" is expanded before the aggregate +-- the expanded code will be placed outside of the aggregate and when +-- expanding the aggregate the loop from 1 to 100 will not surround the -- expanded code for "new Thing (Function_Call)". --- To remedy this situation we introduce a new flag which signals whether we --- want a full analysis (i.e. expansion is enabled) or a pre-analysis which --- performs Analysis and Resolution but no expansion. +-- To remedy this situation we introduce a flag that signals whether we want a +-- full analysis (i.e. expansion is enabled) or a pre-analysis which performs +-- Analysis and Resolution but no expansion. -- After the complete pre-analysis of an expression has been carried out we -- can transform the expression and then carry out the full three stage diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index bc824103ec9..3a450eb2a71 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2605,8 +2605,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; @@ -2782,7 +2782,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)); @@ -2843,7 +2848,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; --------------------------------- @@ -3622,8 +3627,8 @@ package body Sem_Ch12 is Inline_Now : Boolean := False; Has_Inline_Always : Boolean := False; - 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 Save_SM : constant SPARK_Mode_Type := SPARK_Mode; Save_SMP : constant Node_Id := SPARK_Mode_Pragma; @@ -3865,7 +3870,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); @@ -4433,11 +4444,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. @@ -4460,6 +4466,11 @@ 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; @@ -4474,10 +4485,10 @@ 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 := Save_ISMP; + SPARK_Mode := Save_SM; + SPARK_Mode_Pragma := Save_SMP; + Style_Check := Save_Style_Check; if Mode_Set then Restore_Ghost_Mode (Mode); @@ -5119,8 +5130,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 Save_SM : constant SPARK_Mode_Type := SPARK_Mode; Save_SMP : constant Node_Id := SPARK_Mode_Pragma; @@ -5201,15 +5212,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); @@ -5348,6 +5350,22 @@ package body Sem_Ch12 is 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; @@ -5421,10 +5439,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; <> @@ -5432,6 +5446,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; + if Mode_Set then Restore_Ghost_Mode (Mode); end if; @@ -5446,9 +5464,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 := Save_ISMP; + SPARK_Mode := Save_SM; + SPARK_Mode_Pragma := Save_SMP; if Mode_Set then Restore_Ghost_Mode (Mode); @@ -10847,7 +10865,8 @@ package body Sem_Ch12 is Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); Loc : constant Source_Ptr := Sloc (Inst_Node); - Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + Save_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; Save_Style_Check : constant Boolean := Style_Check; procedure Check_Initialized_Types; @@ -11009,13 +11028,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; @@ -11186,8 +11208,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 @@ -11209,7 +11229,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 @@ -11244,6 +11264,9 @@ 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); end Instantiate_Package_Body; @@ -11269,8 +11292,9 @@ package body Sem_Ch12 is Pack_Id : constant Entity_Id := Defining_Unit_Name (Parent (Act_Decl)); - Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; - Saved_Style_Check : constant Boolean := Style_Check; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + Saved_Style_Check : constant Boolean := Style_Check; Saved_Warnings : constant Warning_Record := Save_Warnings; Act_Body : Node_Id; @@ -11363,13 +11387,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; @@ -11473,8 +11500,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 @@ -11549,6 +11574,9 @@ package body Sem_Ch12 is Expander_Mode_Restore; <> + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; + Style_Check := Saved_Style_Check; + Restore_Ghost_Mode (Mode); end Instantiate_Subprogram_Body; @@ -11562,12 +11590,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; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 41f1e530f95..5bd4a7c4ef1 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3298,8 +3298,9 @@ package body Sem_Ch6 is -- Local variables - Mode : Ghost_Mode_Type; - Mode_Set : Boolean := False; + Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; + Mode : Ghost_Mode_Type; + Mode_Set : Boolean := False; -- Start of processing for Analyze_Subprogram_Body_Helper @@ -3371,7 +3372,7 @@ package body Sem_Ch6 is else Enter_Name (Body_Id); - return; + goto Leave; end if; -- Non-generic case, find the subprogram declaration, if one was seen, @@ -3381,7 +3382,7 @@ package body Sem_Ch6 is -- analysis. elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then - return; + goto Leave; else Body_Id := Analyze_Subprogram_Specification (Body_Spec); @@ -3868,6 +3869,29 @@ package body Sem_Ch6 is Set_SPARK_Pragma_Inherited (Body_Id); end if; + -- A subprogram body may be instantiated or inlined at a later pass. + -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when it + -- applied to the initial declaration of the body. + + if Present (Spec_Id) then + if Ignore_SPARK_Mode_Pragmas (Spec_Id) then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + end if; + + else + -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in + -- case the body is instantiated or inlined later and out of context. + -- The body uses this attribute to restore the value of the global + -- flag. + + if Ignore_SPARK_Mode_Pragmas_In_Instance then + Set_Ignore_SPARK_Mode_Pragmas (Body_Id); + + elsif Ignore_SPARK_Mode_Pragmas (Body_Id) then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + end if; + end if; + -- If this is the proper body of a stub, we must verify that the stub -- conforms to the body, and to the previous spec if one was present. -- We know already that the body conforms to that spec. This test is @@ -4056,6 +4080,7 @@ package body Sem_Ch6 is Protected_Body_Subprogram (Spec_Id); Prot_Ext_Formal : Entity_Id := Extra_Formals (Spec_Id); Impl_Ext_Formal : Entity_Id := Extra_Formals (Impl_Subp); + begin while Present (Prot_Ext_Formal) loop pragma Assert (Present (Impl_Ext_Formal)); @@ -4406,6 +4431,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; @@ -4470,6 +4497,15 @@ package body Sem_Ch6 is Set_SPARK_Pragma_Inherited (Designator); end if; + -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case + -- the body of this subprogram is instantiated or inlined later and out + -- of context. The body uses this attribute to restore the value of the + -- global flag. + + if Ignore_SPARK_Mode_Pragmas_In_Instance then + Set_Ignore_SPARK_Mode_Pragmas (Designator); + end if; + if Debug_Flag_C then Write_Str ("==> subprogram spec "); Write_Name (Chars (Designator)); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index e5879dfabb6..260f923beae 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -539,6 +539,8 @@ package body Sem_Ch7 is -- Local variables + Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; + Body_Id : Entity_Id; HSS : Node_Id; Last_Spec_Entity : Entity_Id; @@ -738,6 +740,14 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id); Set_SPARK_Aux_Pragma_Inherited (Body_Id); + + -- A package body may be instantiated or inlined at a later pass. + -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when + -- it applied to the package spec. + + if Ignore_SPARK_Mode_Pragmas (Spec_Id) then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + end if; end if; Set_Categorization_From_Pragmas (N); @@ -931,6 +941,8 @@ package body Sem_Ch7 is end if; end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; + Restore_Ghost_Mode (Mode); end Analyze_Package_Body_Helper; @@ -969,6 +981,15 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Id); Set_SPARK_Aux_Pragma_Inherited (Id); + + -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in + -- case the body of this package is instantiated or inlined later and + -- out of context. The body uses this attribute to restore the value + -- of the global flag. + + if Ignore_SPARK_Mode_Pragmas_In_Instance then + Set_Ignore_SPARK_Mode_Pragmas (Id); + end if; end if; -- Analyze aspect specifications immediately, since we need to recognize diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b0810d9210e..079e52a1db5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -21689,7 +21689,7 @@ package body Sem_Prag is -- enclosing context has SPARK_Mode set to "off", the pragma has -- no semantic effect. - if Ignore_Pragma_SPARK_Mode then + if Ignore_SPARK_Mode_Pragmas_In_Instance then Rewrite (N, Make_Null_Statement (Loc)); Analyze (N); return; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 69ba0cb3017..1cadd47af93 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3622,11 +3622,21 @@ package body Sem_Util is ----------------------- function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is - Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N)); + Id : constant Entity_Id := Defining_Entity (N); + Prag : constant Node_Id := SPARK_Pragma (Id); begin - return - Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off; + -- Default the mode to "off" when the context is an instance and all + -- SPARK_Mode pragmas found within are to be ignored. + + if Ignore_SPARK_Mode_Pragmas (Id) then + return True; + + else + return + Present (Prag) + and then Get_SPARK_Mode_From_Annotation (Prag) = Off; + end if; end SPARK_Mode_Is_Off; -- Start of processing for Check_State_Refinements -- 2.30.2