* [Ada] Incorrect error on valid global refinement
@ 2014-02-19 10:51 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2014-02-19 10:51 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 1454 bytes --]
This patch updates the analysis of aspect/pragma Refined_Global to interpret
states and variables with an encapsulating state as constituents only when the
related state has visible refinement.
------------
-- Source --
------------
-- parent.ads
package Parent
with Abstract_State => State
is
procedure Dummy;
private
Var : Integer := 0 with Part_Of => State;
end Parent;
-- parent.adb
with Parent.Priv_Child;
package body Parent
with Refined_State => (State => (Var, Parent.Priv_Child.Priv_State))
is
procedure Dummy is begin null; end Dummy;
end Parent;
-- parent-priv_child.ads
private package Parent.Priv_Child
with Abstract_State => (Priv_State with Part_Of => State)
is
procedure OK (Param : Integer)
with Global => (In_Out => (Var, Priv_State));
end Parent.Priv_Child;
-- parent-priv_child.adb
package body Parent.Priv_Child
with Refined_State => (Priv_State => Priv_Var)
is
Priv_Var : Integer := 0;
procedure OK (Param : Integer)
with Refined_Global => (In_Out => (Var, Priv_Var))
is begin null; end OK;
end Parent.Priv_Child;
-----------------
-- Compilation --
-----------------
$ gcc -c parent-priv_child.adb
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-19 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Check_Refined_Global_Item):
A state or variable acts as a constituent only it is part of an
encapsulating state and the state has visible refinement.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 945 bytes --]
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207884)
+++ sem_prag.adb (working copy)
@@ -22610,10 +22610,13 @@
-- Start of processing for Check_Refined_Global_Item
begin
- -- The state or variable acts as a constituent of a state, collect
- -- it for the state completeness checks performed later on.
+ -- When the state or variable acts as a constituent of another
+ -- state with a visible refinement, collect it for the state
+ -- completeness checks performed later on.
- if Present (Encapsulating_State (Item_Id)) then
+ if Present (Encapsulating_State (Item_Id))
+ and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+ then
if Global_Mode = Name_Input then
Add_Item (Item_Id, In_Constits);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2014-02-19 10:51 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-02-19 10:51 [Ada] Incorrect error on valid global refinement Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).