[Ada] Improve handling of SPARK_Mode in generic instances

2020-06-03  Yannick Moy  <moy@adacore.com>

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.

4 files changed, 39 insertions, 10 deletions

diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb
index 18b828e..14371b4 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 0b002eb..e723480 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 d44943e..e5bb888 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 0d4c21d..cbb012d 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