diff mbox series

[Ada] Improve handling of SPARK_Mode in generic instances

Message ID 20200603100304.GA6542@adacore.com
State New
Headers show
Series [Ada] Improve handling of SPARK_Mode in generic instances | expand

Commit Message

Pierre-Marie de Rodat June 3, 2020, 10:03 a.m. UTC 
SPARK_Mode aspect/pragma used to signal parts of the code in SPARK is
now allowed to be Off inside generic instantiations for parts of the
code that should not be considered in SPARK.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox series

Patch

--- gcc/ada/rtsfind.adb
+++ 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;

--- gcc/ada/sem_ch6.adb
+++ 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);

--- gcc/ada/sem_ch7.adb
+++ 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);

--- gcc/ada/sem_prag.adb
+++ 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