From 93b3110d75423001107785967a9f9c962e96d2e9 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 10 Jan 2020 14:46:25 +0100 Subject: [PATCH] [Ada] Improve handling of SPARK_Mode in generic instances 2020-06-03 Yannick Moy gcc/ada/ * rtsfind.adb (Load_RTU): Correctly set/reset global variable to ignore SPARK_Mode in instances around loading. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Accept Off without prior On. * sem_ch7.adb (Analyze_Package_Body_Helper): Likewise. * sem_prag.adb (Analyze_Pragma): Always take into account SPARK_Mode Off. --- gcc/ada/rtsfind.adb | 4 ++++ gcc/ada/sem_ch6.adb | 9 +++++++++ gcc/ada/sem_ch7.adb | 9 +++++++++ gcc/ada/sem_prag.adb | 27 +++++++++++++++++---------- 4 files changed, 39 insertions(+), 10 deletions(-) diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index 18b828eaf49a..14371b4bb895 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -931,6 +931,8 @@ package body Rtsfind is Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + 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 Ghost and SPARK mode-related data to restore on exit @@ -946,6 +948,7 @@ package body Rtsfind is -- Provide a clean environment for the unit + Ignore_SPARK_Mode_Pragmas_In_Instance := False; Install_Ghost_Region (None, Empty); Install_SPARK_Mode (None, Empty); @@ -1044,6 +1047,7 @@ package body Rtsfind is Set_Is_Potentially_Use_Visible (U.Entity, True); end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; Restore_Ghost_Region (Saved_GM, Saved_IGR); Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Load_RTU; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 0b002eb59276..e723480517b4 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4592,6 +4592,15 @@ package body Sem_Ch6 is elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then null; + -- SPARK_Mode Off could complete no SPARK_Mode in a generic, either + -- as specified in source code, or because SPARK_Mode On is ignored + -- in an instance where the context is SPARK_Mode Off/Auto. + + elsif Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = Off + and then (Is_Generic_Unit (Spec_Id) or else In_Instance) + then + null; + else Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode #", N); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index d44943ece697..e5bb88808169 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -956,6 +956,15 @@ package body Sem_Ch7 is ("\value Off was set for SPARK_Mode on & #", N, Spec_Id); end if; + -- SPARK_Mode Off could complete no SPARK_Mode in a generic, either + -- as specified in source code, or because SPARK_Mode On is ignored + -- in an instance where the context is SPARK_Mode Off/Auto. + + elsif Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = Off + and then (Is_Generic_Unit (Spec_Id) or else In_Instance) + then + null; + else Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0d4c21d70055..cbb012d1ed51 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23448,6 +23448,11 @@ package body Sem_Prag is -- pragma in which case the current pragma is illegal as -- it cannot "complete". + elsif Get_SPARK_Mode_From_Annotation (N) = Off + and then (Is_Generic_Unit (Entity) or else In_Instance) + then + null; + else Error_Msg_N ("incorrect use of SPARK_Mode", Err_N); Error_Msg_Sloc := Sloc (Err_Id); @@ -23773,16 +23778,6 @@ package body Sem_Prag is -- Start of processing for Do_SPARK_Mode begin - -- When a SPARK_Mode pragma appears inside an instantiation whose - -- enclosing context has SPARK_Mode set to "off", the pragma has - -- no semantic effect. - - if Ignore_SPARK_Mode_Pragmas_In_Instance then - Rewrite (N, Make_Null_Statement (Loc)); - Analyze (N); - return; - end if; - GNAT_Pragma; Check_No_Identifiers; Check_At_Most_N_Arguments (1); @@ -23799,6 +23794,18 @@ package body Sem_Prag is Mode_Id := Get_SPARK_Mode_Type (Mode); Context := Parent (N); + -- When a SPARK_Mode pragma appears inside an instantiation whose + -- enclosing context has SPARK_Mode set to "off", the pragma has + -- no semantic effect. + + if Ignore_SPARK_Mode_Pragmas_In_Instance + and then Mode_Id /= Off + then + Rewrite (N, Make_Null_Statement (Loc)); + Analyze (N); + return; + end if; + -- The pragma appears in a configuration file if No (Context) then -- 2.39.2