[multiple changes]
2016-10-12 Yannick Moy <moy@adacore.com> * einfo.adb, einfo.ads (Partial_Refinement_Constituents): Take into account constituents that are themselves abstract states with full or partial refinement visible. * sem_prag.adb (Find_Encapsulating_State): Move function to library-level, to share between subprograms. (Analyze_Refined_Global_In_Decl_Part): Use Find_Encapsulating_State to get relevant encapsulating state. 2016-10-12 Arnaud Charlet <charlet@adacore.com> * gnat1drv.adb: Fix minor typo. From-SVN: r241052
This commit is contained in:
parent
c8dc49fb03
commit
05f1a54316
|
@ -1,3 +1,17 @@
|
|||
2016-10-12 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* einfo.adb, einfo.ads (Partial_Refinement_Constituents): Take
|
||||
into account constituents that are themselves abstract states
|
||||
with full or partial refinement visible.
|
||||
* sem_prag.adb (Find_Encapsulating_State): Move function
|
||||
to library-level, to share between subprograms.
|
||||
(Analyze_Refined_Global_In_Decl_Part): Use
|
||||
Find_Encapsulating_State to get relevant encapsulating state.
|
||||
|
||||
2016-10-12 Arnaud Charlet <charlet@adacore.com>
|
||||
|
||||
* gnat1drv.adb: Fix minor typo.
|
||||
|
||||
2016-10-12 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Adapt checking
|
||||
|
|
|
@ -8407,19 +8407,79 @@ package body Einfo is
|
|||
-------------------------------------
|
||||
|
||||
function Partial_Refinement_Constituents (Id : E) return L is
|
||||
Constits : Elist_Id;
|
||||
Constits : Elist_Id := No_Elist;
|
||||
|
||||
procedure Add_Usable_Constituents (Item : E);
|
||||
-- Add global item Item and/or its constituents to list Constits when
|
||||
-- they can be used in a global refinement within the current scope. The
|
||||
-- criteria are:
|
||||
-- 1) If Item is an abstract state with full refinement visible, add
|
||||
-- its constituents.
|
||||
-- 2) If Item is an abstract state with only partial refinement
|
||||
-- visible, add both Item and its constituents.
|
||||
-- 3) If Item is an abstract state without a visible refinement, add
|
||||
-- it.
|
||||
-- 4) If Id is not an abstract state, add it.
|
||||
|
||||
procedure Add_Usable_Constituents (List : Elist_Id);
|
||||
-- Apply Add_Usable_Constituents to every constituent in List
|
||||
|
||||
-----------------------------
|
||||
-- Add_Usable_Constituents --
|
||||
-----------------------------
|
||||
|
||||
procedure Add_Usable_Constituents (Item : E) is
|
||||
begin
|
||||
if Ekind (Item) = E_Abstract_State then
|
||||
if Has_Visible_Refinement (Item) then
|
||||
Add_Usable_Constituents (Refinement_Constituents (Item));
|
||||
|
||||
elsif Has_Partial_Visible_Refinement (Item) then
|
||||
Append_New_Elmt (Item, Constits);
|
||||
Add_Usable_Constituents (Part_Of_Constituents (Item));
|
||||
|
||||
else
|
||||
Append_New_Elmt (Item, Constits);
|
||||
end if;
|
||||
|
||||
else
|
||||
Append_New_Elmt (Item, Constits);
|
||||
end if;
|
||||
end Add_Usable_Constituents;
|
||||
|
||||
procedure Add_Usable_Constituents (List : Elist_Id) is
|
||||
Constit_Elmt : Elmt_Id;
|
||||
begin
|
||||
if Present (List) then
|
||||
Constit_Elmt := First_Elmt (List);
|
||||
while Present (Constit_Elmt) loop
|
||||
Add_Usable_Constituents (Node (Constit_Elmt));
|
||||
Next_Elmt (Constit_Elmt);
|
||||
end loop;
|
||||
end if;
|
||||
end Add_Usable_Constituents;
|
||||
|
||||
-- Start of processing for Partial_Refinement_Constituents
|
||||
|
||||
begin
|
||||
-- "Refinement" is a concept applicable only to abstract states
|
||||
|
||||
pragma Assert (Ekind (Id) = E_Abstract_State);
|
||||
Constits := Refinement_Constituents (Id);
|
||||
|
||||
if Has_Visible_Refinement (Id) then
|
||||
Constits := Refinement_Constituents (Id);
|
||||
|
||||
-- A refinement may be partially visible when objects declared in the
|
||||
-- private part of a package are subject to a Part_Of indicator.
|
||||
|
||||
if No (Constits) then
|
||||
Constits := Part_Of_Constituents (Id);
|
||||
elsif Has_Partial_Visible_Refinement (Id) then
|
||||
Add_Usable_Constituents (Part_Of_Constituents (Id));
|
||||
|
||||
-- Function should only be called when full or partial refinement is
|
||||
-- visible.
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
return Constits;
|
||||
|
|
|
@ -3793,9 +3793,11 @@ package Einfo is
|
|||
-- way this is stored is as an element of the Subprograms_For_Type field.
|
||||
|
||||
-- Partial_Refinement_Constituents (synthesized)
|
||||
-- Present in abstract state entities. Contains the constituents that
|
||||
-- refine the state in its private part, in other words, all the hidden
|
||||
-- states that indicate this abstract state in a Part_Of aspect/pragma.
|
||||
-- Defined in abstract state entities. Returns the constituents that
|
||||
-- refine the state in the current scope, which are allowed in a global
|
||||
-- refinement in this scope. These consist in those constituents that are
|
||||
-- abstract states with no or only partial refinement visible, and those
|
||||
-- that are not themselves abstract states.
|
||||
|
||||
-- Partial_View_Has_Unknown_Discr (Flag280)
|
||||
-- Present in all types. Set to Indicate that the partial view of a type
|
||||
|
|
|
@ -343,7 +343,7 @@ procedure Gnat1drv is
|
|||
-- of compiler warnings, but these are being turned off by default,
|
||||
-- and CodePeer generates better messages (referencing original
|
||||
-- variables) this way.
|
||||
-- Do this only is -gnatws is set (the default with -gnatcC), so that
|
||||
-- Do this only if -gnatws is set (the default with -gnatcC), so that
|
||||
-- if warnings are enabled, we'll get better messages from GNAT.
|
||||
|
||||
if Warning_Mode = Suppress then
|
||||
|
|
|
@ -258,6 +258,13 @@ package body Sem_Prag is
|
|||
-- Subsidiary to all Find_Related_xxx routines. Emit an error on pragma
|
||||
-- Prag that duplicates previous pragma Prev.
|
||||
|
||||
function Find_Encapsulating_State
|
||||
(States : Elist_Id;
|
||||
Constit_Id : Entity_Id) return Entity_Id;
|
||||
-- Given the entity of a constituent Constit_Id, find the corresponding
|
||||
-- encapsulating state which appears in States. The routine returns Empty
|
||||
-- is no such state is found.
|
||||
|
||||
function Find_Related_Context
|
||||
(Prag : Node_Id;
|
||||
Do_Checks : Boolean := False) return Node_Id;
|
||||
|
@ -24545,6 +24552,12 @@ package body Sem_Prag is
|
|||
-- These list contain the entities of all Input, In_Out, Output and
|
||||
-- Proof_In items defined in the corresponding Global pragma.
|
||||
|
||||
Repeat_Items : Elist_Id := No_Elist;
|
||||
-- A list of all global items without full visible refinement found
|
||||
-- in pragma Global. These states should be repeated in the global
|
||||
-- refinement (SPARK RM 7.2.4(3c)) unless they have a partial visible
|
||||
-- refinement, in which case they may be repeated (SPARK RM 7.2.4(3d)).
|
||||
|
||||
Spec_Id : Entity_Id;
|
||||
-- The entity of the subprogram subject to pragma Refined_Global
|
||||
|
||||
|
@ -24552,12 +24565,6 @@ package body Sem_Prag is
|
|||
-- A list of all states with full or partial visible refinement found in
|
||||
-- pragma Global.
|
||||
|
||||
Repeat_Items : Elist_Id := No_Elist;
|
||||
-- A list of all global items without full visible refinement found
|
||||
-- in pragma Global. These states should be repeated in the global
|
||||
-- refinement (SPARK RM 7.2.4(3c)) unless they have a partial visible
|
||||
-- refinement, in which case they may be repeated (SPARK RM 7.2.4(3d)).
|
||||
|
||||
procedure Check_In_Out_States;
|
||||
-- Determine whether the corresponding Global pragma mentions In_Out
|
||||
-- states with visible refinement and if so, ensure that one of the
|
||||
|
@ -24616,8 +24623,8 @@ package body Sem_Prag is
|
|||
-- In_Out_Constits and Out_Constits of valid constituents.
|
||||
|
||||
procedure Present_Then_Remove (List : Elist_Id; Item : Entity_Id);
|
||||
-- Same as function Present_Then_Remove, but do not report presence of
|
||||
-- Item in List.
|
||||
-- Same as function Present_Then_Remove, but do not report the presence
|
||||
-- of Item in List.
|
||||
|
||||
procedure Report_Extra_Constituents;
|
||||
-- Emit an error for each constituent found in lists In_Constits,
|
||||
|
@ -24715,12 +24722,12 @@ package body Sem_Prag is
|
|||
N, State_Id);
|
||||
end if;
|
||||
|
||||
-- The state lacks a completion. When full refinement is
|
||||
-- visible, always emit an error (SPARK RM 7.2.4(3a)). When only
|
||||
-- partial refinement is visible, emit an error if the abstract
|
||||
-- state itself is not utilized (SPARK RM 7.2.4(3d)). In the
|
||||
-- case where both are utilized, an error will be issued in
|
||||
-- Check_State_And_Constituent_Use.
|
||||
-- The state lacks a completion. When full refinement is visible,
|
||||
-- always emit an error (SPARK RM 7.2.4(3a)). When only partial
|
||||
-- refinement is visible, emit an error if the abstract state
|
||||
-- itself is not utilized (SPARK RM 7.2.4(3d)). In the case where
|
||||
-- both are utilized, Check_State_And_Constituent_Use. will issue
|
||||
-- the error.
|
||||
|
||||
elsif not Input_Seen
|
||||
and then not In_Out_Seen
|
||||
|
@ -24836,17 +24843,16 @@ package body Sem_Prag is
|
|||
end loop;
|
||||
end if;
|
||||
|
||||
-- Not one of the constituents appeared as Input. When full
|
||||
-- refinement is visible, always emit an error (SPARK RM
|
||||
-- 7.2.4(3a)). When only partial refinement is visible, emit an
|
||||
-- Not one of the constituents appeared as Input. Always emit an
|
||||
-- error when the full refinement is visible (SPARK RM 7.2.4(3a)).
|
||||
-- When only partial refinement is visible, emit an
|
||||
-- error if the abstract state itself is not utilized (SPARK RM
|
||||
-- 7.2.4(3d)). In the case where both are utilized, an error will
|
||||
-- be issued in Check_State_And_Constituent_Use.
|
||||
|
||||
if not In_Seen
|
||||
and then (Has_Visible_Refinement (State_Id)
|
||||
or else
|
||||
Contains (Repeat_Items, State_Id))
|
||||
or else Contains (Repeat_Items, State_Id))
|
||||
then
|
||||
SPARK_Msg_NE
|
||||
("global refinement of state & must include at least one "
|
||||
|
@ -24910,10 +24916,10 @@ package body Sem_Prag is
|
|||
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
|
||||
Constits : constant Elist_Id :=
|
||||
Partial_Refinement_Constituents (State_Id);
|
||||
Constit_Elmt : Elmt_Id;
|
||||
Constit_Id : Entity_Id;
|
||||
Only_Partial : constant Boolean :=
|
||||
not Has_Visible_Refinement (State_Id);
|
||||
Constit_Elmt : Elmt_Id;
|
||||
Constit_Id : Entity_Id;
|
||||
Posted : Boolean := False;
|
||||
|
||||
begin
|
||||
|
@ -24922,9 +24928,9 @@ package body Sem_Prag is
|
|||
while Present (Constit_Elmt) loop
|
||||
Constit_Id := Node (Constit_Elmt);
|
||||
|
||||
-- Issue an error when a constituent of State_Id is
|
||||
-- utilized, and State_Id has only partial visible
|
||||
-- refinement (SPARK RM 7.2.4(3d)).
|
||||
-- Issue an error when a constituent of State_Id is utilized
|
||||
-- and State_Id has only partial visible refinement
|
||||
-- (SPARK RM 7.2.4(3d)).
|
||||
|
||||
if Only_Partial then
|
||||
if Present_Then_Remove (Out_Constits, Constit_Id)
|
||||
|
@ -24936,8 +24942,8 @@ package body Sem_Prag is
|
|||
then
|
||||
Error_Msg_Name_1 := Chars (State_Id);
|
||||
SPARK_Msg_NE
|
||||
("constituent & of state % cannot be used in "
|
||||
& "global refinement", N, Constit_Id);
|
||||
("constituent & of state % cannot be used in global "
|
||||
& "refinement", N, Constit_Id);
|
||||
Error_Msg_Name_1 := Chars (State_Id);
|
||||
SPARK_Msg_N ("\use state % instead", N);
|
||||
end if;
|
||||
|
@ -25000,9 +25006,9 @@ package body Sem_Prag is
|
|||
Item_Id := Node (Item_Elmt);
|
||||
|
||||
-- When full refinement is visible, ensure that all of the
|
||||
-- constituents are utilized and they have mode Output.
|
||||
-- When only partial refinement is visible, ensure that
|
||||
-- no constituent is utilized.
|
||||
-- constituents are utilized and they have mode Output. When
|
||||
-- only partial refinement is visible, ensure that no
|
||||
-- constituent is utilized.
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State
|
||||
and then Has_Non_Null_Visible_Refinement (Item_Id)
|
||||
|
@ -25066,17 +25072,16 @@ package body Sem_Prag is
|
|||
end loop;
|
||||
end if;
|
||||
|
||||
-- Not one of the constituents appeared as Proof_In. When
|
||||
-- full refinement is visible, always emit an error (SPARK RM
|
||||
-- 7.2.4(3a)). When only partial refinement is visible, emit an
|
||||
-- error if the abstract state itself is not utilized (SPARK RM
|
||||
-- 7.2.4(3d)). In the case where both are utilized, an error will
|
||||
-- be issued in Check_State_And_Constituent_Use.
|
||||
-- Not one of the constituents appeared as Proof_In. Always emit
|
||||
-- an error when full refinement is visible (SPARK RM 7.2.4(3a)).
|
||||
-- When only partial refinement is visible, emit an error if the
|
||||
-- abstract state itself is not utilized (SPARK RM 7.2.4(3d)). In
|
||||
-- the case where both are utilized, an error will be issued by
|
||||
-- Check_State_And_Constituent_Use.
|
||||
|
||||
if not Proof_In_Seen
|
||||
and then (Has_Visible_Refinement (State_Id)
|
||||
or else
|
||||
Contains (Repeat_Items, State_Id))
|
||||
or else Contains (Repeat_Items, State_Id))
|
||||
then
|
||||
SPARK_Msg_NE
|
||||
("global refinement of state & must include at least one "
|
||||
|
@ -25165,15 +25170,19 @@ package body Sem_Prag is
|
|||
SPARK_Msg_N ("\expected mode %, found mode %", Item);
|
||||
end Inconsistent_Mode_Error;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Enc_State : Entity_Id := Empty;
|
||||
-- Encapsulating state for constituent, Empty otherwise
|
||||
|
||||
-- Start of processing for Check_Refined_Global_Item
|
||||
|
||||
begin
|
||||
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
|
||||
if Ekind_In (Item_Id, E_Abstract_State,
|
||||
E_Constant,
|
||||
E_Variable)
|
||||
then
|
||||
Enc_State := Encapsulating_State (Item_Id);
|
||||
Enc_State := Find_Encapsulating_State (States, Item_Id);
|
||||
end if;
|
||||
|
||||
-- When the state or object acts as a constituent of another
|
||||
|
@ -25184,8 +25193,7 @@ package body Sem_Prag is
|
|||
|
||||
if Present (Enc_State)
|
||||
and then (Has_Visible_Refinement (Enc_State)
|
||||
or else
|
||||
Has_Partial_Visible_Refinement (Enc_State))
|
||||
or else Has_Partial_Visible_Refinement (Enc_State))
|
||||
and then Contains (States, Enc_State)
|
||||
then
|
||||
-- If the state has only partial visible refinement, remove it
|
||||
|
@ -25360,8 +25368,8 @@ package body Sem_Prag is
|
|||
end if;
|
||||
|
||||
-- Record global items without full visible refinement found in
|
||||
-- pragma Global, which should (SPARK RM 7.2.4(3c)) or may (SPARK
|
||||
-- RM 7.2.4(3d)) be repeated in the global refinement.
|
||||
-- pragma Global which should be repeated in the global refinement
|
||||
-- (SPARK RM 7.2.4(3c), SPARK RM 7.2.4(3d)).
|
||||
|
||||
if Ekind (Item_Id) /= E_Abstract_State
|
||||
or else not Has_Visible_Refinement (Item_Id)
|
||||
|
@ -25523,6 +25531,7 @@ package body Sem_Prag is
|
|||
procedure Report_Missing_Items is
|
||||
Item_Elmt : Elmt_Id;
|
||||
Item_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Do not perform this check in an instance because it was already
|
||||
-- performed successfully in the generic template.
|
||||
|
@ -25650,10 +25659,11 @@ package body Sem_Prag is
|
|||
-- refinement, prior to calling checking procedures which remove items
|
||||
-- from the list of constituents.
|
||||
|
||||
No_Constit := No (In_Constits)
|
||||
and then No (In_Out_Constits)
|
||||
and then No (Out_Constits)
|
||||
and then No (Proof_In_Constits);
|
||||
No_Constit :=
|
||||
No (In_Constits)
|
||||
and then No (In_Out_Constits)
|
||||
and then No (Out_Constits)
|
||||
and then No (Proof_In_Constits);
|
||||
|
||||
-- For Input states with visible refinement, at least one constituent
|
||||
-- must be used as an Input in the global refinement.
|
||||
|
@ -27267,46 +27277,10 @@ package body Sem_Prag is
|
|||
Constits : Elist_Id;
|
||||
Context : Node_Id)
|
||||
is
|
||||
function Find_Encapsulating_State
|
||||
(Constit_Id : Entity_Id) return Entity_Id;
|
||||
-- Given the entity of a constituent, try to find a corresponding
|
||||
-- encapsulating state that appears in the same context. The routine
|
||||
-- returns Empty is no such state is found.
|
||||
|
||||
------------------------------
|
||||
-- Find_Encapsulating_State --
|
||||
------------------------------
|
||||
|
||||
function Find_Encapsulating_State
|
||||
(Constit_Id : Entity_Id) return Entity_Id
|
||||
is
|
||||
State_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Since a constituent may be part of a larger constituent set, climb
|
||||
-- the encapsulating state chain looking for a state that appears in
|
||||
-- the same context.
|
||||
|
||||
State_Id := Encapsulating_State (Constit_Id);
|
||||
while Present (State_Id) loop
|
||||
if Contains (States, State_Id) then
|
||||
return State_Id;
|
||||
end if;
|
||||
|
||||
State_Id := Encapsulating_State (State_Id);
|
||||
end loop;
|
||||
|
||||
return Empty;
|
||||
end Find_Encapsulating_State;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Constit_Elmt : Elmt_Id;
|
||||
Constit_Id : Entity_Id;
|
||||
State_Id : Entity_Id;
|
||||
|
||||
-- Start of processing for Check_State_And_Constituent_Use
|
||||
|
||||
begin
|
||||
-- Nothing to do if there are no states or constituents
|
||||
|
||||
|
@ -27325,7 +27299,7 @@ package body Sem_Prag is
|
|||
-- state that appears in the same context and if this is the case,
|
||||
-- emit an error (SPARK RM 7.2.6(7)).
|
||||
|
||||
State_Id := Find_Encapsulating_State (Constit_Id);
|
||||
State_Id := Find_Encapsulating_State (States, Constit_Id);
|
||||
|
||||
if Present (State_Id) then
|
||||
Error_Msg_Name_1 := Chars (Constit_Id);
|
||||
|
@ -27801,6 +27775,33 @@ package body Sem_Prag is
|
|||
return Num_Primitives (E mod 511);
|
||||
end Entity_Hash;
|
||||
|
||||
------------------------------
|
||||
-- Find_Encapsulating_State --
|
||||
------------------------------
|
||||
|
||||
function Find_Encapsulating_State
|
||||
(States : Elist_Id;
|
||||
Constit_Id : Entity_Id) return Entity_Id
|
||||
is
|
||||
State_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Since a constituent may be part of a larger constituent set, climb
|
||||
-- the encapsulating state chain looking for a state that appears in
|
||||
-- States.
|
||||
|
||||
State_Id := Encapsulating_State (Constit_Id);
|
||||
while Present (State_Id) loop
|
||||
if Contains (States, State_Id) then
|
||||
return State_Id;
|
||||
end if;
|
||||
|
||||
State_Id := Encapsulating_State (State_Id);
|
||||
end loop;
|
||||
|
||||
return Empty;
|
||||
end Find_Encapsulating_State;
|
||||
|
||||
--------------------------
|
||||
-- Find_Related_Context --
|
||||
--------------------------
|
||||
|
|
Loading…
Reference in New Issue