[Ada] State refinement constituent uninstall

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 203531)
+++ sem_ch3.adb	(working copy)
@@ -2067,6 +2067,11 @@ 
       --  (They have the sloc of the label as found in the source, and that
       --  is ahead of the current declarative part).
 
+      procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
+      --  Spec_Id is the entity of a package that may define abstract states.
+      --  If the states have visible refinement, remove the visibility of each
+      --  constituent at the end of the package body declarations.
+
       -----------------
       -- Adjust_Decl --
       -----------------
@@ -2080,6 +2085,24 @@ 
          end loop;
       end Adjust_Decl;
 
+      --------------------------------
+      -- Remove_Visible_Refinements --
+      --------------------------------
+
+      procedure Remove_Visible_Refinements (Spec_Id : Entity_Id) is
+         State_Elmt : Elmt_Id;
+
+      begin
+         if Present (Abstract_States (Spec_Id)) then
+            State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+            while Present (State_Elmt) loop
+               Set_Has_Visible_Refinement (Node (State_Elmt), False);
+
+               Next_Elmt (State_Elmt);
+            end loop;
+         end if;
+      end Remove_Visible_Refinements;
+
       --  Local variables
 
       Body_Id     : Entity_Id;
@@ -2089,6 +2112,9 @@ 
       Prag        : Node_Id;
       Spec_Id     : Entity_Id;
 
+      In_Package_Body : Boolean := False;
+      --  Flag set when the current declaration list belongs to a package body
+
    --  Start of processing for Analyze_Declarations
 
    begin
@@ -2220,6 +2246,8 @@ 
          --  Refined_Global because the last two may mention constituents.
 
          elsif Nkind (Context) = N_Package_Body then
+            In_Package_Body := True;
+
             Body_Id := Defining_Entity (Context);
             Spec_Id := Corresponding_Spec (Context);
             Prag    := Get_Pragma (Body_Id, Pragma_Refined_State);
@@ -2256,6 +2284,14 @@ 
 
          Next (Decl);
       end loop;
+
+      --  State refinements are visible upto the end the of the package body
+      --  declarations. Hide the refinements from visibility to restore the
+      --  original state conditions.
+
+      if In_Package_Body then
+         Remove_Visible_Refinements (Spec_Id);
+      end if;
    end Analyze_Declarations;
 
    -----------------------------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 203527)
+++ einfo.adb	(working copy)
@@ -551,7 +551,7 @@ 
 
    --    Has_Delayed_Rep_Aspects         Flag261
    --    May_Inherit_Delayed_Rep_Aspects Flag262
-   --    Has_Null_Refinement             Flag263
+   --    Has_Visible_Refinement          Flag263
 
    --    (unused)                        Flag264
    --    (unused)                        Flag265
@@ -1483,12 +1483,6 @@ 
       return Flag75 (Implementation_Base_Type (Id));
    end Has_Non_Standard_Rep;
 
-   function Has_Null_Refinement (Id : E) return B is
-   begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      return Flag263 (Id);
-   end Has_Null_Refinement;
-
    function Has_Object_Size_Clause (Id : E) return B is
    begin
       pragma Assert (Is_Type (Id));
@@ -1716,6 +1710,12 @@ 
       return Flag215 (Id);
    end Has_Up_Level_Access;
 
+   function Has_Visible_Refinement (Id : E) return B is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Flag263 (Id);
+   end Has_Visible_Refinement;
+
    function Has_Volatile_Components (Id : E) return B is
    begin
       return Flag87 (Implementation_Base_Type (Id));
@@ -4110,12 +4110,6 @@ 
       Set_Flag75 (Id, V);
    end Set_Has_Non_Standard_Rep;
 
-   procedure Set_Has_Null_Refinement (Id : E; V : B := True) is
-   begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      Set_Flag263 (Id, V);
-   end Set_Has_Null_Refinement;
-
    procedure Set_Has_Object_Size_Clause (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Type (Id));
@@ -4343,6 +4337,12 @@ 
       Set_Flag72 (Id, V);
    end Set_Has_Unknown_Discriminants;
 
+   procedure Set_Has_Visible_Refinement (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Flag263 (Id, V);
+   end Set_Has_Visible_Refinement;
+
    procedure Set_Has_Volatile_Components (Id : E; V : B := True) is
    begin
       pragma Assert (not Is_Type (Id) or else Is_Base_Type (Id));
@@ -6472,6 +6472,29 @@ 
    end Has_Interrupt_Handler;
 
    -----------------------------
+   -- Has_Non_Null_Refinement --
+   -----------------------------
+
+   function Has_Non_Null_Refinement (Id : E) return B is
+   begin
+      --  "Refinement" is a concept applicable only to abstract states
+
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+
+      if Has_Visible_Refinement (Id) then
+         pragma Assert (Present (Refinement_Constituents (Id)));
+
+         --  For a refinement to be non-null, the first constituent must be
+         --  anything other than null.
+
+         return
+           Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
+      end if;
+
+      return False;
+   end Has_Non_Null_Refinement;
+
+   -----------------------------
    -- Has_Null_Abstract_State --
    -----------------------------
 
@@ -6484,6 +6507,29 @@ 
           and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
    end Has_Null_Abstract_State;
 
+   -------------------------
+   -- Has_Null_Refinement --
+   -------------------------
+
+   function Has_Null_Refinement (Id : E) return B is
+   begin
+      --  "Refinement" is a concept applicable only to abstract states
+
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+
+      if Has_Visible_Refinement (Id) then
+         pragma Assert (Present (Refinement_Constituents (Id)));
+
+         --  For a refinement to be null, the state's sole constituent must be
+         --  a null.
+
+         return
+           Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
+      end if;
+
+      return False;
+   end Has_Null_Refinement;
+
    --------------------
    -- Has_Unmodified --
    --------------------
@@ -7969,7 +8015,6 @@ 
       W ("Has_Missing_Return",              Flag142 (Id));
       W ("Has_Nested_Block_With_Handler",   Flag101 (Id));
       W ("Has_Non_Standard_Rep",            Flag75  (Id));
-      W ("Has_Null_Refinement",             Flag263 (Id));
       W ("Has_Object_Size_Clause",          Flag172 (Id));
       W ("Has_Per_Object_Constraint",       Flag154 (Id));
       W ("Has_Postconditions",              Flag240 (Id));
@@ -8011,6 +8056,7 @@ 
       W ("Has_Unchecked_Union",             Flag123 (Id));
       W ("Has_Unknown_Discriminants",       Flag72  (Id));
       W ("Has_Up_Level_Access",             Flag215 (Id));
+      W ("Has_Visible_Refinement",          Flag263 (Id));
       W ("Has_Volatile_Components",         Flag87  (Id));
       W ("Has_Xref_Entry",                  Flag182 (Id));
       W ("In_Package_Body",                 Flag48  (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 203527)
+++ einfo.ads	(working copy)
@@ -1636,6 +1636,10 @@ 
 --       optimizations to ensure that they are consistent with exceptions.
 --       See documentation in Gigi for further details.
 
+--    Has_Non_Null_Refinement (synth)
+--       Defined in E_Abstract_State entities. True if the state has at least
+--       one variable or state constituent in aspect/pragma Refined_State.
+
 --    Has_Non_Standard_Rep (Flag75) [implementation base type only]
 --       Defined in all type entities. Set when some representation clause
 --       or pragma causes the representation of the item to be significantly
@@ -1650,8 +1654,8 @@ 
 --       Defined in package entities. True if the package is subject to a null
 --       Abstract_State aspect/pragma.
 
---    Has_Null_Refinement (Flag263)
---       Defined in E_Abstract_State entities. Set if the state has a null
+--    Has_Null_Refinement (synth)
+--       Defined in E_Abstract_State entities. True if the state has a null
 --       refinement in aspect/pragma Refined_State.
 
 --    Has_Object_Size_Clause (Flag172)
@@ -1913,6 +1917,11 @@ 
 --       VM_Target /= No_VM, for efficiency, since only the .NET back-end
 --       makes use of it to generate proper code for up-level references.
 
+--    Has_Visible_Refinement (Flag263)
+--       Defined in E_Abstract_State entities. Set when a state has at least
+--       one refinement constituent and analysis is in the region between
+--       pragma Refined_State and the end of the package body declarations.
+
 --    Has_Volatile_Components (Flag87) [implementation base type only]
 --       Defined in all types and objects. Set only for an array type or array
 --       object if a valid pragma Volatile_Components or a valid pragma
@@ -5108,7 +5117,9 @@ 
    --  E_Abstract_State
    --    Refinement_Constituents             (Elist8)
    --    Refined_State                       (Node10)
-   --    Has_Null_Refinement                 (Flag263)
+   --    Has_Visible_Refinement              (Flag263)
+   --    Has_Non_Null_Refinement             (synth)
+   --    Has_Null_Refinement                 (synth)
    --    Is_External_State                   (synth)
    --    Is_Input_Only_State                 (synth)
    --    Is_Null_State                       (synth)
@@ -6349,7 +6360,6 @@ 
    function Has_Missing_Return                  (Id : E) return B;
    function Has_Nested_Block_With_Handler       (Id : E) return B;
    function Has_Non_Standard_Rep                (Id : E) return B;
-   function Has_Null_Refinement                 (Id : E) return B;
    function Has_Object_Size_Clause              (Id : E) return B;
    function Has_Per_Object_Constraint           (Id : E) return B;
    function Has_Postconditions                  (Id : E) return B;
@@ -6391,6 +6401,7 @@ 
    function Has_Unchecked_Union                 (Id : E) return B;
    function Has_Unknown_Discriminants           (Id : E) return B;
    function Has_Up_Level_Access                 (Id : E) return B;
+   function Has_Visible_Refinement              (Id : E) return B;
    function Has_Volatile_Components             (Id : E) return B;
    function Has_Xref_Entry                      (Id : E) return B;
    function Hiding_Loop_Variable                (Id : E) return E;
@@ -6696,7 +6707,9 @@ 
    function Has_Attach_Handler                  (Id : E) return B;
    function Has_Entries                         (Id : E) return B;
    function Has_Foreign_Convention              (Id : E) return B;
+   function Has_Non_Null_Refinement             (Id : E) return B;
    function Has_Null_Abstract_State             (Id : E) return B;
+   function Has_Null_Refinement                 (Id : E) return B;
    function Implementation_Base_Type            (Id : E) return E;
    function Is_Base_Type                        (Id : E) return B;
    function Is_Boolean_Type                     (Id : E) return B;
@@ -6963,7 +6976,6 @@ 
    procedure Set_Has_Missing_Return              (Id : E; V : B := True);
    procedure Set_Has_Nested_Block_With_Handler   (Id : E; V : B := True);
    procedure Set_Has_Non_Standard_Rep            (Id : E; V : B := True);
-   procedure Set_Has_Null_Refinement             (Id : E; V : B := True);
    procedure Set_Has_Object_Size_Clause          (Id : E; V : B := True);
    procedure Set_Has_Per_Object_Constraint       (Id : E; V : B := True);
    procedure Set_Has_Postconditions              (Id : E; V : B := True);
@@ -7005,6 +7017,7 @@ 
    procedure Set_Has_Unchecked_Union             (Id : E; V : B := True);
    procedure Set_Has_Unknown_Discriminants       (Id : E; V : B := True);
    procedure Set_Has_Up_Level_Access             (Id : E; V : B := True);
+   procedure Set_Has_Visible_Refinement          (Id : E; V : B := True);
    procedure Set_Has_Volatile_Components         (Id : E; V : B := True);
    procedure Set_Has_Xref_Entry                  (Id : E; V : B := True);
    procedure Set_Hiding_Loop_Variable            (Id : E; V : E);
@@ -7679,7 +7692,6 @@ 
    pragma Inline (Has_Missing_Return);
    pragma Inline (Has_Nested_Block_With_Handler);
    pragma Inline (Has_Non_Standard_Rep);
-   pragma Inline (Has_Null_Refinement);
    pragma Inline (Has_Object_Size_Clause);
    pragma Inline (Has_Per_Object_Constraint);
    pragma Inline (Has_Postconditions);
@@ -7721,6 +7733,7 @@ 
    pragma Inline (Has_Unchecked_Union);
    pragma Inline (Has_Unknown_Discriminants);
    pragma Inline (Has_Up_Level_Access);
+   pragma Inline (Has_Visible_Refinement);
    pragma Inline (Has_Volatile_Components);
    pragma Inline (Has_Xref_Entry);
    pragma Inline (Hiding_Loop_Variable);
@@ -8140,7 +8153,6 @@ 
    pragma Inline (Set_Has_Missing_Return);
    pragma Inline (Set_Has_Nested_Block_With_Handler);
    pragma Inline (Set_Has_Non_Standard_Rep);
-   pragma Inline (Set_Has_Null_Refinement);
    pragma Inline (Set_Has_Object_Size_Clause);
    pragma Inline (Set_Has_Per_Object_Constraint);
    pragma Inline (Set_Has_Postconditions);
@@ -8182,6 +8194,7 @@ 
    pragma Inline (Set_Has_Unchecked_Union);
    pragma Inline (Set_Has_Unknown_Discriminants);
    pragma Inline (Set_Has_Up_Level_Access);
+   pragma Inline (Set_Has_Visible_Refinement);
    pragma Inline (Set_Has_Volatile_Components);
    pragma Inline (Set_Has_Xref_Entry);
    pragma Inline (Set_Hiding_Loop_Variable);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 203545)
+++ sem_prag.adb	(working copy)
@@ -798,9 +798,7 @@ 
                         --  appear in pragma [Refined_]Global as its place must
                         --  be taken by some of its constituents.
 
-                        elsif not Is_Empty_Elmt_List
-                                    (Refinement_Constituents (Item_Id))
-                        then
+                        elsif Has_Visible_Refinement (Item_Id) then
                            Error_Msg_NE
                              ("cannot mention state & in global refinement, "
                               & "use its constituents instead", Item, Item_Id);
@@ -1625,9 +1623,7 @@ 
                   --  in pragma [Refined_]Global as its place must be taken by
                   --  some of its constituents.
 
-                  elsif not Is_Empty_Elmt_List
-                              (Refinement_Constituents (Item_Id))
-                  then
+                  elsif Has_Visible_Refinement (Item_Id) then
                      Error_Msg_NE
                        ("cannot mention state & in global refinement, use its "
                         & "constituents instead", Item, Item_Id);
@@ -19677,9 +19673,7 @@ 
                         --    Depends         => (<output> =>  State)
                         --    Refined_Depends => (<output> => (C1, C2))
 
-                        elsif not Is_Empty_Elmt_List
-                                    (Refinement_Constituents (Dep_Id))
-                        then
+                        elsif Has_Non_Null_Refinement (Dep_Id) then
                            Has_Refined_State := True;
 
                            if Is_Entity_Name (Ref_Input) then
@@ -20033,9 +20027,7 @@ 
                   --    Refined_Depends => (C1 => <input>,
                   --                        C2 => <input>)
 
-                  elsif not Is_Empty_Elmt_List
-                              (Refinement_Constituents (Dep_Id))
-                  then
+                  elsif Has_Non_Null_Refinement (Dep_Id) then
                      Has_Refined_State := True;
 
                      --  Store the entities of all output constituents of an
@@ -20452,8 +20444,7 @@ 
                --  Ensure that one of the three coverage variants is satisfied
 
                if Ekind (Item_Id) = E_Abstract_State
-                 and then not Is_Empty_Elmt_List
-                                (Refinement_Constituents (Item_Id))
+                 and then Has_Non_Null_Refinement (Item_Id)
                then
                   Check_Constituent_Usage (Item_Id);
                end if;
@@ -20536,8 +20527,7 @@ 
                --  is of mode Input.
 
                if Ekind (Item_Id) = E_Abstract_State
-                 and then not Is_Empty_Elmt_List
-                                (Refinement_Constituents (Item_Id))
+                 and then Has_Non_Null_Refinement (Item_Id)
                then
                   Check_Constituent_Usage (Item_Id);
                end if;
@@ -20607,8 +20597,7 @@ 
                --  have mode Output.
 
                if Ekind (Item_Id) = E_Abstract_State
-                 and then not Is_Empty_Elmt_List
-                                (Refinement_Constituents (Item_Id))
+                 and then Has_Non_Null_Refinement (Item_Id)
                then
                   Check_Constituent_Usage (Item_Id);
                end if;
@@ -20730,8 +20719,7 @@ 
                --  occurrences in Global and Refined_Global match.
 
                if No (Refined_State (Item_Id))
-                 and then Is_Empty_Elmt_List
-                            (Refinement_Constituents (Item_Id))
+                 and then not Has_Visible_Refinement (Item_Id)
                then
                   Check_Matching_Modes (Item_Id);
                end if;
@@ -21088,13 +21076,20 @@ 
                      Add_Item (Constit_Id, Constituents_Seen);
                      Remove_Elmt (Hidden_States, State_Elmt);
 
-                     --  Establish a relation between the refined state and its
-                     --  constituent.
+                     --  Collect the constituent in the list of refinement
+                     --  items. Establish a relation between the refined state
+                     --  and its constituent.
 
                      Append_Elmt
                        (Constit_Id, Refinement_Constituents (State_Id));
                      Set_Refined_State (Constit_Id, State_Id);
 
+                     --  The state has at least one legal constituent, mark the
+                     --  start of the refinement region. The region ends when
+                     --  the body declarations end (see Analyze_Declarations).
+
+                     Set_Has_Visible_Refinement (State_Id);
+
                      return;
                   end if;
 
@@ -21129,11 +21124,18 @@ 
                   Error_Msg_N
                     ("cannot mix null and non-null constituents", Constit);
 
-               --  Mark the related state as having a null refinement
-
                else
                   Null_Seen := True;
-                  Set_Has_Null_Refinement (State_Id);
+
+                  --  Collect the constituent in the list of refinement items
+
+                  Append_Elmt (Constit, Refinement_Constituents (State_Id));
+
+                  --  The state has at least one legal constituent, mark the
+                  --  start of the refinement region. The region ends when the
+                  --  body declarations end (see Analyze_Declarations).
+
+                  Set_Has_Visible_Refinement (State_Id);
                end if;
 
             --  Non-null constituents
@@ -21717,12 +21719,15 @@ 
             if Ekind (Item_Id) = E_Abstract_State then
                if Has_Null_Refinement (Item_Id) then
                   Has_Null_State := True;
-               elsif Mode = Name_Input then
-                  Has_In_State := True;
-               elsif Mode = Name_In_Out then
-                  Has_In_Out_State := True;
-               elsif Mode = Name_Output then
-                  Has_Out_State := True;
+
+               elsif Has_Non_Null_Refinement (Item_Id) then
+                  if Mode = Name_Input then
+                     Has_In_State := True;
+                  elsif Mode = Name_In_Out then
+                     Has_In_Out_State := True;
+                  elsif Mode = Name_Output then
+                     Has_Out_State := True;
+                  end if;
                end if;
             end if;
 
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 203532)
+++ sem_util.adb	(working copy)
@@ -3418,8 +3418,7 @@ 
 
             return
               Ekind (Item_Id) = E_Abstract_State
-                and then not Is_Empty_Elmt_List
-                               (Refinement_Constituents (Item_Id));
+                and then Has_Visible_Refinement (Item_Id);
          end if;
       end Is_Refined_State;