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 <m...@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.--- 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
