This implements the rule in SPARK RM (6.1.5(4)): A global item shall
not denote a state abstraction whose refinement is visible (a state
abstraction cannot be named within its enclosing package's body other
than in its refinement).
The following is compiled with -gnatd.V
1. package Depends_Illegal
2. with Abstract_State => A
3. is
4. pragma Elaborate_Body (Depends_Illegal);
5. end Depends_Illegal;
1. package body Depends_Illegal
2. with Refined_State => (A => (X, Y))
3. is
4. X, Y : Natural := 0;
5. function F1 (Par1 : Natural) return Natural
6. with Global => A,
|
>>> global reference to "A" not allowed (SPARK RM 6.1.5(4))
>>> refinement of "A" is visible at line 2
7. Depends => (F1'Result => A,
|
>>> global reference to "A" not allowed (SPARK RM 6.1.5(4))
>>> refinement of "A" is visible at line 2
8. null => Par1)
9. is
10. begin
11. return X;
12. end F1;
13. end Depends_Illegal;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-17 Robert Dewar <de...@adacore.com>
* einfo.ads, einfo.adb (Has_Body_References): New flag.
(Body_References): New field.
* sem_prag.adb (Record_Possible_Body_Reference): New procedure
(Analyze_Input_Output): Call Record_Possible_Body_Reference
(Analyze_Global_Item): Call Record_Possible_Body_Reference
(Analyze_Refinement_Clause): Output messages if illegal global refs.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 203568)
+++ einfo.adb (working copy)
@@ -132,6 +132,7 @@
-- String_Literal_Low_Bound Node15
-- Access_Disp_Table Elist16
+ -- Body_References Elist16
-- Cloned_Subtype Node16
-- DTC_Entity Node16
-- Entry_Formal Node16
@@ -552,8 +553,8 @@
-- Has_Delayed_Rep_Aspects Flag261
-- May_Inherit_Delayed_Rep_Aspects Flag262
-- Has_Visible_Refinement Flag263
+ -- Has_Body_References Flag264
- -- (unused) Flag264
-- (unused) Flag265
-- (unused) Flag266
-- (unused) Flag267
@@ -733,6 +734,12 @@
return Flag40 (Id);
end Body_Needed_For_SAL;
+ function Body_References (Id : E) return L is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Elist16 (Id);
+ end Body_References;
+
function C_Pass_By_Copy (Id : E) return B is
begin
pragma Assert (Is_Record_Type (Id));
@@ -1294,6 +1301,12 @@
return Flag139 (Id);
end Has_Biased_Representation;
+ function Has_Body_References (Id : E) return B is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Flag264 (Id);
+ end Has_Body_References;
+
function Has_Completion (Id : E) return B is
begin
return Flag26 (Id);
@@ -3336,6 +3349,12 @@
Set_Flag40 (Id, V);
end Set_Body_Needed_For_SAL;
+ procedure Set_Body_References (Id : E; V : L) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Elist16 (Id, V);
+ end Set_Body_References;
+
procedure Set_C_Pass_By_Copy (Id : E; V : B := True) is
begin
pragma Assert (Is_Record_Type (Id) and then Is_Base_Type (Id));
@@ -3909,6 +3928,12 @@
Set_Flag139 (Id, V);
end Set_Has_Biased_Representation;
+ procedure Set_Has_Body_References (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Flag264 (Id, V);
+ end Set_Has_Body_References;
+
procedure Set_Has_Completion (Id : E; V : B := True) is
begin
Set_Flag26 (Id, V);
@@ -7984,6 +8009,7 @@
W ("Has_Anonymous_Master", Flag253 (Id));
W ("Has_Atomic_Components", Flag86 (Id));
W ("Has_Biased_Representation", Flag139 (Id));
+ W ("Has_Body_References", Flag264 (Id));
W ("Has_Completion", Flag26 (Id));
W ("Has_Completion_In_Body", Flag71 (Id));
W ("Has_Complex_Representation", Flag140 (Id));
@@ -8672,6 +8698,10 @@
procedure Write_Field16_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+
+ when E_Abstract_State =>
+ Write_Str ("Body_References");
+
when E_Record_Type |
E_Record_Type_With_Private =>
Write_Str ("Access_Disp_Table");
Index: einfo.ads
===================================================================
--- einfo.ads (revision 203568)
+++ einfo.ads (working copy)
@@ -493,6 +493,12 @@
-- units. Indicates that the source for the body must be included
-- when the unit is part of a standalone library.
+-- Body_References (Elist16)
+-- Defined in abstract state entities. Only set if Has_Body_References
+-- flag is set True, in which case it contains an element list of global
+-- references (identifiers) in the current package body to this abstract
+-- state that are illegal if the abstract state has a visible refinement.
+
-- C_Pass_By_Copy (Flag125) [implementation base type only]
-- Defined in record types. Set if a pragma Convention for the record
-- type specifies convention C_Pass_By_Copy. This convention name is
@@ -1405,6 +1411,10 @@
-- size of the type, forcing biased representation for the object, but
-- the subtype is still an unbiased type.
+-- Has_Body_References (Flag264)
+-- Defined in entities for abstract states. Set if Body_References has
+-- at least one entry.
+
-- Has_Completion (Flag26)
-- Defined in all entities that require a completion (functions,
-- procedures, private types, limited private types, incomplete types,
@@ -5117,6 +5127,8 @@
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Refined_State (Node10)
+ -- Body_References (Elist16)
+ -- Has_Body_References (Flag264)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Null_Refinement (synth)
-- Has_Null_Refinement (synth)
@@ -6230,6 +6242,7 @@
function Block_Node (Id : E) return N;
function Body_Entity (Id : E) return E;
function Body_Needed_For_SAL (Id : E) return B;
+ function Body_References (Id : E) return L;
function CR_Discriminant (Id : E) return E;
function C_Pass_By_Copy (Id : E) return B;
function Can_Never_Be_Null (Id : E) return B;
@@ -6325,6 +6338,7 @@
function Has_Anonymous_Master (Id : E) return B;
function Has_Atomic_Components (Id : E) return B;
function Has_Biased_Representation (Id : E) return B;
+ function Has_Body_References (Id : E) return B;
function Has_Completion (Id : E) return B;
function Has_Completion_In_Body (Id : E) return B;
function Has_Complex_Representation (Id : E) return B;
@@ -6848,6 +6862,7 @@
procedure Set_Block_Node (Id : E; V : N);
procedure Set_Body_Entity (Id : E; V : E);
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True);
+ procedure Set_Body_References (Id : E; V : L);
procedure Set_CR_Discriminant (Id : E; V : E);
procedure Set_C_Pass_By_Copy (Id : E; V : B := True);
procedure Set_Can_Never_Be_Null (Id : E; V : B := True);
@@ -6942,6 +6957,7 @@
procedure Set_Has_Anonymous_Master (Id : E; V : B := True);
procedure Set_Has_Atomic_Components (Id : E; V : B := True);
procedure Set_Has_Biased_Representation (Id : E; V : B := True);
+ procedure Set_Has_Body_References (Id : E; V : B := True);
procedure Set_Has_Completion (Id : E; V : B := True);
procedure Set_Has_Completion_In_Body (Id : E; V : B := True);
procedure Set_Has_Complex_Representation (Id : E; V : B := True);
@@ -7568,6 +7584,7 @@
pragma Inline (Block_Node);
pragma Inline (Body_Entity);
pragma Inline (Body_Needed_For_SAL);
+ pragma Inline (Body_References);
pragma Inline (CR_Discriminant);
pragma Inline (C_Pass_By_Copy);
pragma Inline (Can_Never_Be_Null);
@@ -7660,6 +7677,7 @@
pragma Inline (Has_Anonymous_Master);
pragma Inline (Has_Atomic_Components);
pragma Inline (Has_Biased_Representation);
+ pragma Inline (Has_Body_References);
pragma Inline (Has_Completion);
pragma Inline (Has_Completion_In_Body);
pragma Inline (Has_Complex_Representation);
@@ -8031,6 +8049,7 @@
pragma Inline (Set_Block_Node);
pragma Inline (Set_Body_Entity);
pragma Inline (Set_Body_Needed_For_SAL);
+ pragma Inline (Set_Body_References);
pragma Inline (Set_CR_Discriminant);
pragma Inline (Set_C_Pass_By_Copy);
pragma Inline (Set_Can_Never_Be_Null);
@@ -8121,6 +8140,7 @@
pragma Inline (Set_Has_Anonymous_Master);
pragma Inline (Set_Has_Atomic_Components);
pragma Inline (Set_Has_Biased_Representation);
+ pragma Inline (Set_Has_Body_References);
pragma Inline (Set_Has_Completion);
pragma Inline (Set_Has_Completion_In_Body);
pragma Inline (Set_Has_Complex_Representation);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203749)
+++ sem_prag.adb (working copy)
@@ -277,23 +277,30 @@
-- of a Test_Case pragma if present (possibly Empty). We treat these as
-- spec expressions (i.e. similar to a default expression).
+ procedure Record_Possible_Body_Reference
+ (Item : Node_Id;
+ Item_Id : Entity_Id);
+ -- Given an entity reference (Item) and the corresponding Entity (Item_Id),
+ -- determines if we have a body reference to an abstract state, which may
+ -- be illegal if the state is refined within the body.
+
procedure Rewrite_Assertion_Kind (N : Node_Id);
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
-- then it is rewritten as an identifier with the corresponding special
-- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas
-- Check, Check_Policy.
+ procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
+ -- Place semantic information on the argument of an Elaborate/Elaborate_All
+ -- pragma. Entity name for unit and its parents is taken from item in
+ -- previous with_clause that mentions the unit.
+
procedure rv;
-- This is a dummy function called by the processing for pragma Reviewable.
-- It is there for assisting front end debugging. By placing a Reviewable
-- pragma in the source program, a breakpoint on rv catches this place in
-- the source, allowing convenient stepping to the point of interest.
- procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
- -- Place semantic information on the argument of an Elaborate/Elaborate_All
- -- pragma. Entity name for unit and its parents is taken from item in
- -- previous with_clause that mentions the unit.
-
--------------
-- Add_Item --
--------------
@@ -772,6 +779,8 @@
Item_Id := Entity_Of (Item);
+ Record_Possible_Body_Reference (Item, Item_Id);
+
if Present (Item_Id) then
if Ekind_In (Item_Id, E_Abstract_State,
E_In_Parameter,
@@ -1645,6 +1654,7 @@
Item_Id := Entity_Of (Item);
if Present (Item_Id) then
+ Record_Possible_Body_Reference (Item, Item_Id);
-- A global item may denote a formal parameter of an enclosing
-- subprogram. Do this check first to provide a better error
@@ -21641,6 +21651,29 @@
("& must denote an abstract state", State, State_Id);
end if;
+ -- Enforce SPARK RM (6.1.5(4)): A global item shall not
+ -- denote a state abstraction whose refinement is visible
+ -- (a state abstraction cannot be named within its enclosing
+ -- package's body other than in its refinement).
+
+ if Has_Body_References (State_Id) then
+ declare
+ Ref : Elmt_Id;
+ Nod : Node_Id;
+ begin
+ Ref := First_Elmt (Body_References (State_Id));
+ while Present (Ref) loop
+ Nod := Node (Ref);
+ Error_Msg_N
+ ("global reference to & not allowed "
+ & "(SPARK RM 6.1.5(4))", Nod);
+ Error_Msg_Sloc := Sloc (State);
+ Error_Msg_N ("\refinement of & is visible#", Nod);
+ Next_Elmt (Ref);
+ end loop;
+ end;
+ end if;
+
-- The state name is illegal
else
@@ -23296,6 +23329,27 @@
end Process_Compilation_Unit_Pragmas;
+ ------------------------------------
+ -- Record_Possible_Body_Reference --
+ ------------------------------------
+
+ procedure Record_Possible_Body_Reference
+ (Item : Node_Id;
+ Item_Id : Entity_Id)
+ is
+ begin
+ if In_Package_Body
+ and then Ekind (Item_Id) = E_Abstract_State
+ then
+ if not Has_Body_References (Item_Id) then
+ Set_Has_Body_References (Item_Id, True);
+ Set_Body_References (Item_Id, New_Elmt_List);
+ end if;
+
+ Append_Elmt (Item, Body_References (Item_Id));
+ end if;
+ end Record_Possible_Body_Reference;
+
------------------------------
-- Relocate_Pragmas_To_Body --
------------------------------
