From 8d45ce773959d3e89c18790d9f5b48d526dcdd07 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Tue, 17 Jul 2018 08:03:54 +0000 Subject: [PATCH] [Ada] Spurious error on unused Part_Of constituent 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" 2018-07-17 Hristian Kirtchev 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. From-SVN: r262768 --- gcc/ada/ChangeLog | 12 ++++++++++++ gcc/ada/sem_prag.adb | 19 ++++++++++++++++++- gcc/ada/sem_util.adb | 16 +++++++++++++--- gcc/ada/sem_util.ads | 23 ++++++++++++----------- 4 files changed, 55 insertions(+), 15 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ad067f6..b322861 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2018-07-17 Hristian Kirtchev + + * 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. + 2018-07-17 Ed Schonberg * sem_util.adb (Gather_Components): A discriminant of an ancestor may diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 6bd5462..37b7d23 100644 --- a/gcc/ada/sem_prag.adb +++ b/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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 2b96ce8..0977392 100644 --- a/gcc/ada/sem_util.adb +++ b/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; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 34d618e..21a74ae 100644 --- a/gcc/ada/sem_util.ads +++ b/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; -- 2.7.4