This patch modifies the generic instantiation to ensure that a context with a missing SPARK_Mode annotation is treated as having SPARK_Mode set to Off. This ensures that the following SPARK UG rule 9.4.1
Code where SPARK_Mode is Off shall not enclose code where Spark_Mode is On. However, if an instance of a generic unit is enclosed by code where SPARK_Mode is Off and if any SPARK_Mode specifications occur within the generic unit, then the corresponding SPARK_Mode specifications occurring within the instance have no semantic effect. does not lead to spurious errors. ------------ -- Source -- ------------ -- gen_pack.ads generic type T is private; package Gen_Pack with SPARK_Mode is procedure Force_Body; generic type Inner_T is private; package Inner_Gen_Pack with SPARK_Mode => Off is type Inner_T_Ptr is access Inner_T; end Inner_Gen_Pack; package Inner_Inst is new Inner_Gen_Pack (Inner_T => T); type T_Ptr is private; private pragma SPARK_Mode (Off); type T_Ptr is new Inner_Inst.Inner_T_Ptr; end Gen_Pack; -- gen_pack.adb package body Gen_Pack with SPARK_Mode => Off is procedure Force_Body is begin null; end Force_Body; end Gen_Pack; -- main.adb with Gen_Pack; procedure Main is package Inst is new Gen_Pack (T => Integer); begin null; end Main; ----------------- -- Compilation -- ----------------- $ gcc -c main.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-16 Hristian Kirtchev <kirtc...@adacore.com> * sem_ch12.adb (Analyze_Package_Instantiation): Treat a missing SPARK_Mode annotation as having mode "Off". (Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode annotation as having mode "Off". (Instantiate_Package_Body): Code reformatting. Treat a missing SPARK_Mode annotation as having mode "Off". (Instantiate_Subprogram_Body): Code reformatting. Treat a missing SPARK_Mode annotation as having mode "Off".
Index: sem_ch12.adb =================================================================== --- sem_ch12.adb (revision 228884) +++ sem_ch12.adb (working copy) @@ -3723,11 +3723,12 @@ goto Leave; else - -- If the context of the instance is subject to SPARK_Mode "off", - -- 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" 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 = Off then + if SPARK_Mode /= On then Ignore_Pragma_SPARK_Mode := True; end if; @@ -5098,11 +5099,12 @@ Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit); else - -- If the context of the instance is subject to SPARK_Mode "off", - -- 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" 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 = Off then + if SPARK_Mode /= On then Ignore_Pragma_SPARK_Mode := True; end if; @@ -10632,18 +10634,19 @@ Act_Spec : constant Node_Id := Specification (Act_Decl); Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec); + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + Save_Style_Check : constant Boolean := Style_Check; + + Act_Body : Node_Id; + Act_Body_Id : Entity_Id; Act_Body_Name : Node_Id; Gen_Body : Node_Id; Gen_Body_Id : Node_Id; - Act_Body : Node_Id; - Act_Body_Id : Entity_Id; + Par_Ent : Entity_Id := Empty; + Par_Vis : Boolean := False; Parent_Installed : Boolean := False; - Save_Style_Check : constant Boolean := Style_Check; - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; - Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation -- to match the visibility of the formal type @@ -10783,8 +10786,17 @@ if Present (Gen_Body_Id) then 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 SPARK_Mode /= On then + Ignore_Pragma_SPARK_Mode := True; + end if; + Current_Sem_Unit := Body_Info.Current_Sem_Unit; - Gen_Body := Unit_Declaration_Node (Gen_Body_Id); Create_Instantiation_Source @@ -10943,6 +10955,7 @@ 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 @@ -11019,6 +11032,7 @@ 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_Warnings : constant Warning_Record := Save_Warnings; @@ -11104,6 +11118,16 @@ Save_Env (Gen_Unit, Anon_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 SPARK_Mode /= On then + Ignore_Pragma_SPARK_Mode := True; + end if; + Current_Sem_Unit := Body_Info.Current_Sem_Unit; Create_Instantiation_Source (Inst_Node, @@ -11203,6 +11227,7 @@ end if; Restore_Env; + Ignore_Pragma_SPARK_Mode := Saved_IPSM; Style_Check := Saved_Style_Check; Restore_Warnings (Saved_Warnings); @@ -11268,9 +11293,10 @@ (Make_Simple_Return_Statement (Loc, Ret_Expr)))); end if; - Pack_Body := Make_Package_Body (Loc, - Defining_Unit_Name => New_Copy (Pack_Id), - Declarations => New_List (Act_Body)); + Pack_Body := + Make_Package_Body (Loc, + Defining_Unit_Name => New_Copy (Pack_Id), + Declarations => New_List (Act_Body)); Insert_After (Inst_Node, Pack_Body); Set_Corresponding_Spec (Pack_Body, Pack_Id);