From cf9a473e6494aef4d6e36dfdab64b3c42bfe5958 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 25 Apr 2017 12:49:34 +0200 Subject: [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/sem_ch12.adb | 140 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 84 insertions(+), 56 deletions(-) (limited to 'gcc/ada/sem_ch12.adb') diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index bc82410..3a450eb 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; -- cgit v1.1