This patch augments the generic instantiation machinery to preserve a key
property of a package or subprogram spec for the corresponding body which
may be instantiated or inlined later. Whenever a generic is instantiated in an
environment where the SPARK_Mode is Off, any SPARK_Mode pragma found within the
spec and body must be ignored. Due to late instantiation or inlining of bodies,
this property was previously lost which in turn led to spurious errors about
missing SPARK_Mode annotations in specs.
------------
-- Source --
------------
-- gen.ads
generic
package Gen is
task type Tsk;
end Gen;
-- gen.adb
with Ada.Real_Time; use Ada.Real_Time;
package body Gen is
task body Tsk is
Now : constant Time := Time_Of (0, Time_Span_First);
Later : Time;
begin
Later := Now + Milliseconds (1);
end Tsk;
end Gen;
-- pack.ads
with Gen;
package Pack is
package Inst is new Gen;
end Pack;
-----------------
-- Compilation --
-----------------
$ gcc -c -gnatn pack.ads
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-04-25 Hristian Kirtchev <kirtc...@adacore.com>
* einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
(Ignore_SPARK_Mode_Pragmas): New routine.
(Set_Ignore_SPARK_Mode_Pragmas): New routine.
(Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
* einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
related entities.
(Ignore_SPARK_Mode_Pragmas): New routine
along with pragma Inline.
(Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
* opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
Ignore_SPARK_Mode_Pragmas_In_Instance.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
Save and restore the value of global flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
the corresponding spec or the body must ignore all SPARK_Mode
pragmas found within.
(Analyze_Subprogram_Declaration): Mark
the spec when it needs to ignore all SPARK_Mode pragmas found
within to allow the body to infer this property in case it is
instantiated or inlined later.
* sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding spec also ignored all SPARK_Mode pragmas
found within.
(Analyze_Package_Declaration): Mark the spec when
it needs to ignore all SPARK_Mode pragmas found within to allow
the body to infer this property in case it is instantiated or
inlined later.
* sem_ch12.adb (Analyze_Formal_Package_Declaration):
Save and restore the value of flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
formal spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Package_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
the instance spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Subprogram_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
instance spec and anonymous package when they need to ignore
all SPARK_Mode pragmas found within to allow the body to infer
this property in case it is instantiated or inlined later.
(Instantiate_Package_Body): Save and restore the value of global
flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
corresponding instance spec also ignored all SPARK_Mode pragmas
found within.
(Instantiate_Subprogram_Body): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding instance spec also ignored all SPARK_Mode
pragmas found within.
* sem_prag.adb (Analyze_Pragma): Update the reference to
Ignore_Pragma_SPARK_Mode.
* sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
all SPARK_Mode pragmas defined within yields mode "off".
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 247177)
+++ sem_ch7.adb (working copy)
@@ -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
Index: einfo.adb
===================================================================
--- einfo.adb (revision 247177)
+++ einfo.adb (working copy)
@@ -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));
Index: einfo.ads
===================================================================
--- einfo.ads (revision 247177)
+++ einfo.ads (working copy)
@@ -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);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 247179)
+++ sem_prag.adb (working copy)
@@ -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;
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 247177)
+++ sem_ch12.adb (working copy)
@@ -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;
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 247181)
+++ sem_util.adb (working copy)
@@ -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
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 247177)
+++ sem_ch6.adb (working copy)
@@ -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));
Index: opt.ads
===================================================================
--- opt.ads (revision 247177)
+++ opt.ads (working copy)
@@ -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
