This patch ensures that all delayed SPARK aspects are analyzed with the proper
SPARK mode of their related construct.
------------
-- Source --
------------
-- modes.ads
package Modes
with SPARK_Mode => On,
Abstract_State => State
is
Var : Integer := 1;
procedure Disabled_1 (Formal : Integer)
with SPARK_Mode => Off,
Global => (Input => (Formal, State, Var)), -- suppressed
Depends => (null => (Formal, Var)); -- suppressed
procedure Enabled_1 (Formal : Integer)
with SPARK_Mode => On,
Global => (Input => (Formal, State, Var)), -- error
Depends => (null => (Formal, Var)); -- error
end Modes;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c modes.ads
modes.ads:14:33: global item cannot reference parameter of subprogram
modes.ads:14:41: state "State" must appear in at least one input dependence
list
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-17 Hristian Kirtchev <kirtc...@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Contract,
Analyze_Subprogram_Contract): Add new local variable Mode. Save
and restore the SPARK mode of the related construct in a
stack-like fashion.
* sem_ch7.adb (Analyze_Package_Body_Contract,
Analyze_Package_Contract): Add new local variable Mode. Save and
restore the SPARK mode of the related construct in a stack-like fashion.
* sem_util.adb Remove with and use clause for Opt.
(Restore_SPARK_Mode): New routine.
(Save_SPARK_Mode_And_Set): New routine.
* sem_util.ads Add with and use clause for Opt.
(Restore_SPARK_Mode): New routine.
(Save_SPARK_Mode_And_Set): New routine.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 212640)
+++ sem_ch7.adb (working copy)
@@ -180,9 +180,12 @@
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
begin
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
-- The analysis of pragma Refined_State detects whether the spec has
@@ -200,6 +203,8 @@
then
Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Package_Body_Contract;
---------------------------------
@@ -839,9 +844,12 @@
------------------------------
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
begin
+ Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+
-- Analyze the initialization related pragmas. Initializes must come
-- before Initial_Condition due to item dependencies.
@@ -867,6 +875,8 @@
Check_Missing_Part_Of (Pack_Id);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Package_Contract;
---------------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 212656)
+++ sem_util.adb (working copy)
@@ -41,7 +41,6 @@
with Nlists; use Nlists;
with Nmake; use Nmake;
with Output; use Output;
-with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Rtsfind; use Rtsfind;
@@ -15321,6 +15320,15 @@
Reset_Analyzed (N);
end Reset_Analyzed_Flags;
+ ------------------------
+ -- Restore_SPARK_Mode --
+ ------------------------
+
+ procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type) is
+ begin
+ SPARK_Mode := Mode;
+ end Restore_SPARK_Mode;
+
--------------------------------
-- Returns_Unconstrained_Type --
--------------------------------
@@ -15624,6 +15632,28 @@
end if;
end Same_Value;
+ -----------------------------
+ -- Save_SPARK_Mode_And_Set --
+ -----------------------------
+
+ procedure Save_SPARK_Mode_And_Set
+ (Context : Entity_Id;
+ Mode : out SPARK_Mode_Type)
+ is
+ Prag : constant Node_Id := SPARK_Pragma (Context);
+
+ begin
+ -- Save the current mode in effect
+
+ Mode := SPARK_Mode;
+
+ -- Set the mode of the context as the current SPARK mode
+
+ if Present (Prag) then
+ SPARK_Mode := Get_SPARK_Mode_From_Pragma (Prag);
+ end if;
+ end Save_SPARK_Mode_And_Set;
+
------------------------
-- Scope_Is_Transient --
------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 212640)
+++ sem_util.ads (working copy)
@@ -28,6 +28,7 @@
with Einfo; use Einfo;
with Exp_Tss; use Exp_Tss;
with Namet; use Namet;
+with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
with Uintp; use Uintp;
@@ -1689,6 +1690,10 @@
procedure Reset_Analyzed_Flags (N : Node_Id);
-- Reset the Analyzed flags in all nodes of the tree whose root is N
+ procedure Restore_SPARK_Mode (Mode : SPARK_Mode_Type);
+ -- Set the current SPARK_Mode to whatever Mode denotes. This routime must
+ -- be used in tandem with Save_SPARK_Mode_And_Set.
+
function Returns_Unconstrained_Type (Subp : Entity_Id) return Boolean;
-- Return true if Subp is a function that returns an unconstrained type
@@ -1740,6 +1745,13 @@
-- A result of False does not necessarily mean they have different values,
-- just that it is not possible to determine they have the same value.
+ procedure Save_SPARK_Mode_And_Set
+ (Context : Entity_Id;
+ Mode : out SPARK_Mode_Type);
+ -- Save the current SPARK_Mode in effect in Mode. Establish the SPARK_Mode
+ -- (if any) of a package or a subprogram denoted by Context. This routine
+ -- must be used in tandem with Restore_SPARK_Mode.
+
function Scope_Within_Or_Same (Scope1, Scope2 : Entity_Id) return Boolean;
-- Determines if the entity Scope1 is the same as Scope2, or if it is
-- inside it, where both entities represent scopes. Note that scopes
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 212640)
+++ sem_ch6.adb (working copy)
@@ -2033,12 +2033,15 @@
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
+ Mode : SPARK_Mode_Type;
Prag : Node_Id;
Ref_Depends : Node_Id := Empty;
Ref_Global : Node_Id := Empty;
Spec_Id : Entity_Id;
begin
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
-- When a subprogram body declaration is illegal, its defining entity is
-- left unanalyzed. There is nothing left to do in this case because the
-- body lacks a contract, or even a proper Ekind.
@@ -2112,6 +2115,8 @@
Body_Decl, Spec_Id);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Subprogram_Body_Contract;
------------------------------------
@@ -3680,6 +3685,7 @@
Case_Prag : Node_Id := Empty;
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
Nam : Name_Id;
Post_Prag : Node_Id := Empty;
Prag : Node_Id;
@@ -3687,6 +3693,8 @@
Seen_In_Post : Boolean := False;
begin
+ Save_SPARK_Mode_And_Set (Subp, Mode);
+
if Present (Items) then
-- Analyze pre- and postconditions
@@ -3808,6 +3816,8 @@
("function postcondition does not mention result?T?", Post_Prag);
end if;
end if;
+
+ Restore_SPARK_Mode (Mode);
end Analyze_Subprogram_Contract;
------------------------------------
