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 modifies the analysis of pragma Refined_Global to treat objects and states as constituents only when their encapsulating state appears in pragma Global. ------------ -- Source -- ------------ -- pack.ads package Pack with Abstract_State => (State1, State2), Initializes => (Var, State1, State2) is Var : Integer := 0; procedure Initialize_State with Global => (Output => State1), Depends => (State1 => null); end Pack; -- pack.adb package body Pack with Refined_State => (State1 => (A, B), State2 => (Inner.Inner_Var, Inner.Inner_State)) is A, B : Integer; package Inner with Abstract_State => Inner_State, Initializes => (Inner_State, Inner_Var => Var) is Inner_Var : Integer; procedure Initialize_Inner with Global => (Output => (Inner_State, Inner_Var), Input => Var), Depends => (Inner_State => null, Inner_Var => Var); end Inner; procedure Initialize_State is separate with Refined_Global => (Output => (A, B)), Refined_Depends => ((A, B) => null); procedure Double_B is separate with Global => (In_Out => B), Depends => (B => B); package body Inner is separate; begin Initialize_State; Double_B; end Pack; -- pack-double_b.adb separate (Pack) procedure Double_B is begin B := B * 2; end Double_B; -- pack-initialize_state.adb separate (Pack) procedure Initialize_State is begin A := 0; B := 0; end Initialize_State; -- pack-inner.adb separate (Pack) package body Inner with Refined_State => (Inner_State => Inner_Body_Var) is Inner_Body_Var : Integer; procedure Initialize_Inner with Refined_Global => (Output => (Inner_Body_Var, Inner_Var), Input => Var), Refined_Depends => (Inner_Body_Var => null, Inner_Var => Var) is begin Inner_Body_Var := 0; Inner_Var := Var; end Initialize_Inner; begin Initialize_Inner; end Inner; ----------------- -- Compilation -- ----------------- $ gcc -c pack.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-27 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Refined_Global_In_Decl_Part): Add variable States. (Check_Refined_Global_Item): An object or state acts as a constituent only when the corresponding encapsulating state appears in pragma Global. (Collect_Global_Item): Add a state with non-null visible refinement to list States.
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] |