===================================================================
@@ -539,6 +539,8 @@
-- Local variables
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
@@ -738,6 +740,14 @@
Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
+
+ -- A package body may be instantiated or inlined at a later pass.
+ -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when
+ -- it applied to the package spec.
+
+ if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
end if;
Set_Categorization_From_Pragmas (N);
@@ -931,6 +941,8 @@
end if;
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
Restore_Ghost_Mode (Mode);
end Analyze_Package_Body_Helper;
@@ -969,6 +981,15 @@
Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Id);
Set_SPARK_Aux_Pragma_Inherited (Id);
+
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+ -- case the body of this package is instantiated or inlined later and
+ -- out of context. The body uses this attribute to restore the value
+ -- of the global flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Id);
+ end if;
end if;
-- Analyze aspect specifications immediately, since we need to recognize
===================================================================
@@ -620,7 +620,7 @@
-- Body_Needed_For_Inlining Flag299
-- Has_Private_Extension Flag300
- -- (unused) Flag301
+ -- Ignore_SPARK_Mode_Pragmas Flag301
-- (unused) Flag302
-- (unused) Flag303
-- (unused) Flag304
@@ -1981,6 +1981,29 @@
return Node4 (Id);
end Homonym;
+ function Ignore_SPARK_Mode_Pragmas (Id : E) return B is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ return Flag301 (Id);
+ end Ignore_SPARK_Mode_Pragmas;
+
function Import_Pragma (Id : E) return E is
begin
pragma Assert (Is_Subprogram (Id));
@@ -5073,6 +5096,29 @@
Set_Elist24 (Id, V);
end Set_Incomplete_Actuals;
+ procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ Set_Flag301 (Id, V);
+ end Set_Ignore_SPARK_Mode_Pragmas;
+
procedure Set_Import_Pragma (Id : E; V : E) is
begin
pragma Assert (Is_Subprogram (Id));
@@ -9402,6 +9448,7 @@
W ("Has_Visible_Refinement", Flag263 (Id));
W ("Has_Volatile_Components", Flag87 (Id));
W ("Has_Xref_Entry", Flag182 (Id));
+ W ("Ignore_SPARK_Mode_Pragmas", Flag301 (Id));
W ("In_Package_Body", Flag48 (Id));
W ("In_Private_Part", Flag45 (Id));
W ("In_Use", Flag8 (Id));
===================================================================
@@ -2164,6 +2164,13 @@
-- scopes. Homonyms in the same scope are overloaded. Used for name
-- resolution and for the generation of debugging information.
+-- Ignore_SPARK_Mode_Pragmas (Flag301)
+-- Present in concurrent type, entry, operator, [generic] package,
+-- package body, [generic] subprogram, and subprogram body entities.
+-- Set when the entity appears in an instance subject to SPARK_Mode
+-- "off" and indicates that all SPARK_Mode pragmas found within must
+-- be ignored.
+
-- Implementation_Base_Type (synthesized)
-- Applies to all entities. For types, similar to Base_Type, but never
-- returns a private type when applied to a non-private type. Instead in
@@ -5922,14 +5929,15 @@
-- Extra_Formals (Node28)
-- Contract (Node34)
-- SPARK_Pragma (Node40) (protected kind)
- -- Needs_No_Actuals (Flag22)
- -- Uses_Sec_Stack (Flag95)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
+ -- Has_Expanded_Contract (Flag240)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
+ -- Is_Entry_Wrapper (Flag297)
+ -- Needs_No_Actuals (Flag22)
-- Sec_Stack_Needed_For_Return (Flag167)
- -- Has_Expanded_Contract (Flag240)
-- SPARK_Pragma_Inherited (Flag265) (protected kind)
- -- Is_Entry_Wrapper (Flag297)
+ -- Uses_Sec_Stack (Flag95)
-- Address_Clause (synth)
-- Entry_Index_Type (synth)
-- First_Formal (synth)
@@ -6056,6 +6064,7 @@
-- Has_Nested_Subprogram (Flag282)
-- Has_Out_Or_In_Out_Parameter (Flag110)
-- Has_Recursive_Call (Flag143)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Called (Flag102) (non-generic case only)
-- Is_Constructor (Flag76)
@@ -6209,6 +6218,7 @@
-- SPARK_Pragma (Node40)
-- Default_Expressions_Processed (Flag108)
-- Has_Nested_Subprogram (Flag282)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Primitive (Flag218)
@@ -6272,6 +6282,7 @@
-- Has_Forward_Instantiation (Flag175)
-- Has_Master_Entity (Flag21)
-- Has_RACW (Flag214) (non-generic case only)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- In_Package_Body (Flag48)
-- In_Use (Flag8)
-- Is_Instantiated (Flag126)
@@ -6299,6 +6310,7 @@
-- SPARK_Aux_Pragma (Node41)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
@@ -6367,6 +6379,7 @@
-- Has_Master_Entity (Flag21)
-- Has_Nested_Block_With_Handler (Flag101)
-- Has_Nested_Subprogram (Flag282)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Asynchronous (Flag81)
-- Is_Called (Flag102) (non-generic case only)
@@ -6406,6 +6419,7 @@
-- E_Protected_Body
-- SPARK_Pragma (Node40)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
@@ -6427,6 +6441,7 @@
-- Entry_Max_Queue_Lengths_Array (Node35)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
@@ -6557,6 +6572,7 @@
-- E_Task_Body
-- Contract (Node34)
-- SPARK_Pragma (Node40)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
@@ -6580,6 +6596,7 @@
-- Delay_Cleanups (Flag114)
-- Has_Master_Entity (Flag21)
-- Has_Storage_Size_Clause (Flag23) (base type only)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
@@ -7103,6 +7120,7 @@
function Has_Xref_Entry (Id : E) return B;
function Hiding_Loop_Variable (Id : E) return E;
function Homonym (Id : E) return E;
+ function Ignore_SPARK_Mode_Pragmas (Id : E) return B;
function Import_Pragma (Id : E) return E;
function Incomplete_Actuals (Id : E) return L;
function In_Package_Body (Id : E) return B;
@@ -7788,6 +7806,7 @@
procedure Set_Has_Xref_Entry (Id : E; V : B := True);
procedure Set_Hiding_Loop_Variable (Id : E; V : E);
procedure Set_Homonym (Id : E; V : E);
+ procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True);
procedure Set_Import_Pragma (Id : E; V : E);
procedure Set_Incomplete_Actuals (Id : E; V : L);
procedure Set_In_Package_Body (Id : E; V : B := True);
@@ -8587,6 +8606,7 @@
pragma Inline (Has_Xref_Entry);
pragma Inline (Hiding_Loop_Variable);
pragma Inline (Homonym);
+ pragma Inline (Ignore_SPARK_Mode_Pragmas);
pragma Inline (Import_Pragma);
pragma Inline (Incomplete_Actuals);
pragma Inline (In_Package_Body);
@@ -9109,6 +9129,7 @@
pragma Inline (Set_Has_Xref_Entry);
pragma Inline (Set_Hiding_Loop_Variable);
pragma Inline (Set_Homonym);
+ pragma Inline (Set_Ignore_SPARK_Mode_Pragmas);
pragma Inline (Set_Import_Pragma);
pragma Inline (Set_Incomplete_Actuals);
pragma Inline (Set_In_Package_Body);
===================================================================
@@ -21689,7 +21689,7 @@
-- enclosing context has SPARK_Mode set to "off", the pragma has
-- no semantic effect.
- if Ignore_Pragma_SPARK_Mode then
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
return;
===================================================================
@@ -2605,8 +2605,8 @@
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Associations : Boolean := True;
New_N : Node_Id;
@@ -2782,7 +2782,12 @@
-- all SPARK_Mode pragmas within the generic_package_name.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the formal spec in case the body is instantiated at a later
+ -- pass. This preserves the original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Formal);
end if;
Analyze (Specification (N));
@@ -2843,7 +2848,7 @@
Analyze_Aspect_Specifications (N, Pack_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
end Analyze_Formal_Package_Declaration;
---------------------------------
@@ -3622,8 +3627,8 @@
Inline_Now : Boolean := False;
Has_Inline_Always : Boolean := False;
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
@@ -3865,7 +3870,13 @@
-- the instance.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the instance spec in case the body is instantiated at a
+ -- later pass. This preserves the original context in effect for
+ -- the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
end if;
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
@@ -4433,11 +4444,6 @@
Set_Defining_Identifier (N, Act_Decl_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
-
-- Check that if N is an instantiation of System.Dim_Float_IO or
-- System.Dim_Integer_IO, the formal type has a dimension system.
@@ -4460,6 +4466,11 @@
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@@ -4474,10 +4485,10 @@
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
if Mode_Set then
Restore_Ghost_Mode (Mode);
@@ -5119,8 +5130,8 @@
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
@@ -5201,15 +5212,6 @@
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
- -- 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;
-
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
@@ -5348,6 +5350,22 @@
Set_Has_Pragma_Inline_Always
(Anon_Id, Has_Pragma_Inline_Always (Gen_Unit));
+ -- 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_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark both the instance spec and the anonymous package in case
+ -- the body is instantiated at a later pass. This preserves the
+ -- original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
+ Set_Ignore_SPARK_Mode_Pragmas (Anon_Id);
+ end if;
+
if not Is_Intrinsic_Subprogram (Gen_Unit) then
Check_Elab_Instantiation (N);
end if;
@@ -5421,10 +5439,6 @@
Env_Installed := False;
Generic_Renamings.Set_Last (0);
Generic_Renamings_HTable.Reset;
-
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
end if;
<<Leave>>
@@ -5432,6 +5446,10 @@
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@@ -5446,9 +5464,9 @@
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
if Mode_Set then
Restore_Ghost_Mode (Mode);
@@ -10847,7 +10865,8 @@
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
Loc : constant Source_Ptr := Sloc (Inst_Node);
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ Save_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
Save_Style_Check : constant Boolean := Style_Check;
procedure Check_Initialized_Types;
@@ -11009,13 +11028,16 @@
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 the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, 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;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@@ -11186,8 +11208,6 @@
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
-- complaint is suppressed if we have detected other errors (since a
@@ -11209,7 +11229,7 @@
-- was already detected, since this can cause blowups.
else
- return;
+ goto Leave;
end if;
-- Case of package that does not need a body
@@ -11244,6 +11264,9 @@
Expander_Mode_Restore;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ Style_Check := Save_Style_Check;
+
Restore_Ghost_Mode (Mode);
end Instantiate_Package_Body;
@@ -11269,8 +11292,9 @@
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_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
Act_Body : Node_Id;
@@ -11363,13 +11387,16 @@
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 the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, 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;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
@@ -11473,8 +11500,6 @@
end if;
Restore_Env;
- Ignore_Pragma_SPARK_Mode := Saved_IPSM;
- Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
-- Body not found. Error was emitted already. If there were no previous
@@ -11549,6 +11574,9 @@
Expander_Mode_Restore;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Style_Check := Saved_Style_Check;
+
Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
@@ -11562,12 +11590,12 @@
Analyzed_Formal : Node_Id;
Actual_Decls : List_Id) return List_Id
is
- Gen_T : constant Entity_Id := Defining_Identifier (Formal);
A_Gen_T : constant Entity_Id :=
Defining_Identifier (Analyzed_Formal);
- Ancestor : Entity_Id := Empty;
Def : constant Node_Id := Formal_Type_Definition (Formal);
+ Gen_T : constant Entity_Id := Defining_Identifier (Formal);
Act_T : Entity_Id;
+ Ancestor : Entity_Id := Empty;
Decl_Node : Node_Id;
Decl_Nodes : List_Id;
Loc : Source_Ptr;
===================================================================
@@ -3622,11 +3622,21 @@
-----------------------
function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
- Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
+ Id : constant Entity_Id := Defining_Entity (N);
+ Prag : constant Node_Id := SPARK_Pragma (Id);
begin
- return
- Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+ -- Default the mode to "off" when the context is an instance and all
+ -- SPARK_Mode pragmas found within are to be ignored.
+
+ if Ignore_SPARK_Mode_Pragmas (Id) then
+ return True;
+
+ else
+ return
+ Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+ end if;
end SPARK_Mode_Is_Off;
-- Start of processing for Check_State_Refinements
===================================================================
@@ -3298,8 +3298,9 @@
-- Local variables
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
-- Start of processing for Analyze_Subprogram_Body_Helper
@@ -3371,7 +3372,7 @@
else
Enter_Name (Body_Id);
- return;
+ goto Leave;
end if;
-- Non-generic case, find the subprogram declaration, if one was seen,
@@ -3381,7 +3382,7 @@
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- return;
+ goto Leave;
else
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
@@ -3868,6 +3869,29 @@
Set_SPARK_Pragma_Inherited (Body_Id);
end if;
+ -- A subprogram body may be instantiated or inlined at a later pass.
+ -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when it
+ -- applied to the initial declaration of the body.
+
+ if Present (Spec_Id) then
+ if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
+
+ else
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+ -- case the body is instantiated or inlined later and out of context.
+ -- The body uses this attribute to restore the value of the global
+ -- flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Body_Id);
+
+ elsif Ignore_SPARK_Mode_Pragmas (Body_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
+ end if;
+
-- If this is the proper body of a stub, we must verify that the stub
-- conforms to the body, and to the previous spec if one was present.
-- We know already that the body conforms to that spec. This test is
@@ -4056,6 +4080,7 @@
Protected_Body_Subprogram (Spec_Id);
Prot_Ext_Formal : Entity_Id := Extra_Formals (Spec_Id);
Impl_Ext_Formal : Entity_Id := Extra_Formals (Impl_Subp);
+
begin
while Present (Prot_Ext_Formal) loop
pragma Assert (Present (Impl_Ext_Formal));
@@ -4406,6 +4431,8 @@
end if;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
@@ -4470,6 +4497,15 @@
Set_SPARK_Pragma_Inherited (Designator);
end if;
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+ -- the body of this subprogram is instantiated or inlined later and out
+ -- of context. The body uses this attribute to restore the value of the
+ -- global flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Designator);
+ end if;
+
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
===================================================================
@@ -814,18 +814,18 @@
-- default value appropriate to the system (in Osint.Initialize), and then
-- reset if a command line switch is used to change the setting.
- Ignore_Pragma_SPARK_Mode : Boolean := False;
- -- GNAT
- -- Set True to ignore the semantics and effects of pragma SPARK_Mode when
- -- the pragma appears inside an instance whose enclosing context is subject
- -- to SPARK_Mode "off".
-
Ignore_Rep_Clauses : Boolean := False;
-- GNAT
-- Set True to ignore all representation clauses. Useful when compiling
-- code from foreign compilers for checking or ASIS purposes. Can be
-- set True by use of -gnatI.
+ Ignore_SPARK_Mode_Pragmas_In_Instance : Boolean := False;
+ -- GNAT
+ -- Set True to ignore the semantics and effects of pragma SPARK_Mode when
+ -- the pragma appears inside an instance whose enclosing context is subject
+ -- to SPARK_Mode "off". This property applies to nested instances.
+
Ignore_Style_Checks_Pragmas : Boolean := False;
-- GNAT
-- Set True to ignore all Style_Checks pragmas. Can be set True by use