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]

[Ada] Spurious error on legal use of abstract state constituent


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]