This patch updates the analysis of indicator Part_Of (or the lack thereof), to
ignore generic formal parameters for purposes of determining the visible state
space because they are not visible outside the generic and related instances.
------------
-- Source --
------------
-- gen_pack.ads
generic
In_Formal : in Integer := 0;
In_Out_Formal : in out Integer;
package Gen_Pack is
Exported_In_Formal : Integer renames In_Formal;
Exported_In_Out_Formal : Integer renames In_Out_Formal;
end Gen_Pack;
-- pack.ads
with Gen_Pack;
package Pack
with Abstract_State => State
is
procedure Force_Body;
Val : Integer;
private
package OK_1 is
new Gen_Pack (In_Out_Formal => Val)
with Part_Of => State; -- OK
package OK_2 is
new Gen_Pack (In_Formal => 1, In_Out_Formal => Val)
with Part_Of => State; -- OK
package Error_1 is -- Error
new Gen_Pack (In_Out_Formal => Val);
package Error_2 is -- Error
new Gen_Pack (In_Formal => 2, In_Out_Formal => Val);
end Pack;
-- pack.adb
package body Pack
with Refined_State => -- Error
(State => (OK_1.Exported_In_Formal,
OK_1.Exported_In_Out_Formal))
is
procedure Force_Body is null;
end Pack;
-- gen_pack.ads
generic
In_Formal : in Integer := 0;
In_Out_Formal : in out Integer;
package Gen_Pack is
Exported_In_Formal : Integer renames In_Formal;
Exported_In_Out_Formal : Integer renames In_Out_Formal;
end Gen_Pack;
-- pack.ads
with Gen_Pack;
package Pack
with Abstract_State => State
is
procedure Force_Body;
Val : Integer;
private
package OK_1 is
new Gen_Pack (In_Out_Formal => Val)
with Part_Of => State; -- OK
package OK_2 is
new Gen_Pack (In_Formal => 1, In_Out_Formal => Val)
with Part_Of => State; -- OK
package Error_1 is -- Error
new Gen_Pack (In_Out_Formal => Val);
package Error_2 is -- Error
new Gen_Pack (In_Formal => 2, In_Out_Formal => Val);
end Pack;
-- pack.adb
package body Pack
with Refined_State => -- Error
(State => (OK_1.Exported_In_Formal,
OK_1.Exported_In_Out_Formal))
is
procedure Force_Body is null;
end Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c pack.adb
pack.adb:3:11: state "State" has unused Part_Of constituents
pack.adb:3:11: constant "Exported_In_Formal" defined at gen_pack.ads:6,
instance at pack.ads:15
pack.adb:3:11: variable "Exported_In_Out_Formal" defined at gen_pack.ads:7,
instance at pack.ads:15
pack.ads:19:12: indicator Part_Of is required in this context (SPARK RM
7.2.6(2))
pack.ads:19:12: "Error_1" is declared in the private part of package "Pack"
pack.ads:21:12: indicator Part_Of is required in this context (SPARK RM
7.2.6(2))
pack.ads:21:12: "Error_2" is declared in the private part of package "Pack"
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-07-17 Hristian Kirtchev <kirtc...@adacore.com>
gcc/ada/
* sem_prag.adb (Has_Visible_State): Do not consider generic formals
because they are not part of the visible state space. Add constants to
the list of acceptable visible states.
(Propagate_Part_Of): Do not consider generic formals when propagating
the Part_Of indicator.
* sem_util.adb (Entity_Of): Do not follow renaming chains which go
through a generic formal because they are not visible for SPARK
purposes.
* sem_util.ads (Entity_Of): Update the comment on usage.--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -19982,6 +19982,13 @@ package body Sem_Prag is
if not Comes_From_Source (Item_Id) then
null;
+ -- Do not consider generic formals or their corresponding
+ -- actuals because they are not part of a visible state.
+ -- Note that both entities are marked as hidden.
+
+ elsif Is_Hidden (Item_Id) then
+ null;
+
-- The Part_Of indicator turns an abstract state or an
-- object into a constituent of the encapsulating state.
@@ -28775,9 +28782,19 @@ package body Sem_Prag is
if not Comes_From_Source (Item_Id) then
null;
+ -- Do not consider generic formals or their corresponding actuals
+ -- because they are not part of a visible state. Note that both
+ -- entities are marked as hidden.
+
+ elsif Is_Hidden (Item_Id) then
+ null;
+
-- A visible state has been found
- elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+ elsif Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
+ then
return True;
-- Recursively peek into nested packages and instantiations
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -7442,7 +7442,17 @@ package body Sem_Util is
-- Ren : ... renames Obj;
if Is_Entity_Name (Ren) then
- Id := Entity (Ren);
+
+ -- Do not follow a renaming that goes through a generic formal,
+ -- because these entities are hidden and must not be referenced
+ -- from outside the generic.
+
+ if Is_Hidden (Entity (Ren)) then
+ exit;
+
+ else
+ Id := Entity (Ren);
+ end if;
-- The reference renames a function result. Check the original
-- node in case expansion relocates the function call.
@@ -8819,7 +8829,7 @@ package body Sem_Util is
-- Stored_Constraint as well.
-- An inherited discriminant may have been constrained in a
- -- later ancestor (no the immediate parent) so we must examine
+ -- later ancestor (not the immediate parent) so we must examine
-- the stored constraint of all of them to locate the inherited
-- value.
@@ -8858,7 +8868,7 @@ package body Sem_Util is
end loop;
end if;
- -- Discriminant may be inherited from ancestor.
+ -- Discriminant may be inherited from ancestor
T := Etype (T);
end loop;
end;
--- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -126,8 +126,8 @@ package Sem_Util is
Loc : Source_Ptr := No_Location;
Rep : Boolean := True;
Warn : Boolean := False);
- -- N is a subexpression which will raise constraint error when evaluated
- -- at runtime. Msg is a message that explains the reason for raising the
+ -- N is a subexpression that will raise Constraint_Error when evaluated
+ -- at run time. Msg is a message that explains the reason for raising the
-- exception. The last character is ? if the message is always a warning,
-- even in Ada 95, and is not a ? if the message represents an illegality
-- (because of violation of static expression rules) in Ada 95 (but not
@@ -614,19 +614,19 @@ package Sem_Util is
-- Emit an error if iterated component association N is actually an illegal
-- quantified expression lacking a quantifier.
- function Dynamic_Accessibility_Level (Expr : Node_Id) return Node_Id;
- -- Expr should be an expression of an access type. Builds an integer
- -- literal except in cases involving anonymous access types where
- -- accessibility levels are tracked at runtime (access parameters and Ada
- -- 2012 stand-alone objects).
-
function Discriminated_Size (Comp : Entity_Id) return Boolean;
-- If a component size is not static then a warning will be emitted
-- in Ravenscar or other restricted contexts. When a component is non-
-- static because of a discriminant constraint we can specialize the
-- warning by mentioning discriminants explicitly. This was created for
-- private components of protected objects, but is generally useful when
- -- retriction (No_Implicit_Heap_Allocation) is active.
+ -- restriction No_Implicit_Heap_Allocation is active.
+
+ function Dynamic_Accessibility_Level (Expr : Node_Id) return Node_Id;
+ -- Expr should be an expression of an access type. Builds an integer
+ -- literal except in cases involving anonymous access types, where
+ -- accessibility levels are tracked at run time (access parameters and
+ -- Ada 2012 stand-alone objects).
function Effective_Extra_Accessibility (Id : Entity_Id) return Entity_Id;
-- Same as Einfo.Extra_Accessibility except thtat object renames
@@ -705,7 +705,8 @@ package Sem_Util is
function Entity_Of (N : Node_Id) return Entity_Id;
-- Obtain the entity of arbitrary node N. If N is a renaming, return the
-- entity of the earliest renamed source abstract state or whole object.
- -- If no suitable entity is available, return Empty.
+ -- If no suitable entity is available, return Empty. This routine carries
+ -- out actions that are tied to SPARK semantics.
procedure Explain_Limited_Type (T : Entity_Id; N : Node_Id);
-- This procedure is called after issuing a message complaining about an
@@ -2025,7 +2026,7 @@ package Sem_Util is
function Is_Transfer (N : Node_Id) return Boolean;
-- Returns True if the node N is a statement which is known to cause an
- -- unconditional transfer of control at runtime, i.e. the following
+ -- unconditional transfer of control at run time, i.e. the following
-- statement definitely will not be executed.
function Is_True (U : Uint) return Boolean;
