This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
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:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |