[Ada] Hidden state detection

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 198286)
+++ sem_ch3.adb	(working copy)
@@ -3720,6 +3720,13 @@ 
       end if;
 
       Analyze_Dimension (N);
+
+      --  Verify whether the object declaration introduces an illegal hidden
+      --  state within a package subject to a null abstract state.
+
+      if Formal_Extensions and then Ekind (Id) = E_Variable then
+         Check_No_Hidden_State (Id);
+      end if;
    end Analyze_Object_Declaration;
 
    ---------------------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 198286)
+++ einfo.adb	(working copy)
@@ -666,7 +666,7 @@ 
 
    function Abstract_States (Id : E) return L is
    begin
-      pragma Assert (Ekind (Id) = E_Package);
+      pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
       return Elist25 (Id);
    end Abstract_States;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 198275)
+++ sem_prag.adb	(working copy)
@@ -8518,6 +8518,13 @@ 
                   Pop_Scope;
                end if;
 
+               --  Verify whether the state introduces an illegal hidden state
+               --  within a package subject to a null abstract state.
+
+               if Formal_Extensions then
+                  Check_No_Hidden_State (Id);
+               end if;
+
                --  Associate the state with its related package
 
                if No (Abstract_States (Pack_Id)) then
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 198284)
+++ sem_util.adb	(working copy)
@@ -2125,6 +2125,98 @@ 
       end if;
    end Check_Nested_Access;
 
+   ---------------------------
+   -- Check_No_Hidden_State --
+   ---------------------------
+
+   procedure Check_No_Hidden_State (Id : Entity_Id) is
+      function Has_Null_Abstract_State (Pkg : Entity_Id) return Boolean;
+      --  Determine whether the entity of a package denoted by Pkg has a null
+      --  abstract state.
+
+      -----------------------------
+      -- Has_Null_Abstract_State --
+      -----------------------------
+
+      function Has_Null_Abstract_State (Pkg : Entity_Id) return Boolean is
+         States : constant Elist_Id := Abstract_States (Pkg);
+
+      begin
+         --  Check the first available state of the related package. A null
+         --  abstract state always appears as the sole element of the state
+         --  list.
+
+         return
+           Present (States)
+             and then Is_Null_State (Node (First_Elmt (States)));
+      end Has_Null_Abstract_State;
+
+      --  Local variables
+
+      Context     : Entity_Id := Empty;
+      Not_Visible : Boolean   := False;
+      Scop        : Entity_Id;
+
+   --  Start of processing for Check_No_Hidden_State
+
+   begin
+      pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+
+      --  Find the proper context where the object or state appears
+
+      Scop := Scope (Id);
+      while Present (Scop) loop
+         Context := Scop;
+
+         --  Keep track of the context's visibility
+
+         Not_Visible := Not_Visible or else In_Private_Part (Context);
+
+         --  Prevent the search from going too far
+
+         if Context = Standard_Standard then
+            return;
+
+         --  Objects and states that appear immediately within a subprogram or
+         --  inside a construct nested within a subprogram do not introduce a
+         --  hidden state. They behave as local variable declarations.
+
+         elsif Is_Subprogram (Context) then
+            return;
+
+         --  When examining a package body, use the entity of the spec as it
+         --  carries the abstract state declarations.
+
+         elsif Ekind (Context) = E_Package_Body then
+            Context := Spec_Entity (Context);
+         end if;
+
+         --  Stop the traversal when a package subject to a null abstract state
+         --  has been found.
+
+         if Ekind_In (Context, E_Generic_Package, E_Package)
+           and then Has_Null_Abstract_State (Context)
+         then
+            exit;
+         end if;
+
+         Scop := Scope (Scop);
+      end loop;
+
+      --  At this point we know that there is at least one package with a null
+      --  abstract state in visibility. Emit an error message unconditionally
+      --  if the entity being processed is a state because the placement of the
+      --  related package is irrelevant. This is not the case for objects as
+      --  the intermediate context matters.
+
+      if Present (Context)
+        and then (Ekind (Id) = E_Abstract_State or else Not_Visible)
+      then
+         Error_Msg_N ("cannot introduce hidden state &", Id);
+         Error_Msg_NE ("\package & has null abstract state", Id, Context);
+      end if;
+   end Check_No_Hidden_State;
+
    ------------------------------------------
    -- Check_Potentially_Blocking_Operation --
    ------------------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 198283)
+++ sem_util.ads	(working copy)
@@ -168,14 +168,14 @@ 
    --  the compilation unit, and install it in the Elaboration_Entity field
    --  of Spec_Id, the entity for the compilation unit.
 
-      procedure Build_Explicit_Dereference
-        (Expr : Node_Id;
-         Disc : Entity_Id);
-      --  AI05-139: Names with implicit dereference. If the expression N is a
-      --  reference type and the context imposes the corresponding designated
-      --  type, convert N into N.Disc.all. Such expressions are always over-
-      --  loaded with both interpretations, and the dereference interpretation
-      --  carries the name of the reference discriminant.
+   procedure Build_Explicit_Dereference
+     (Expr : Node_Id;
+      Disc : Entity_Id);
+   --  AI05-139: Names with implicit dereference. If the expression N is a
+   --  reference type and the context imposes the corresponding designated
+   --  type, convert N into N.Disc.all. Such expressions are always over-
+   --  loaded with both interpretations, and the dereference interpretation
+   --  carries the name of the reference discriminant.
 
    function Cannot_Raise_Constraint_Error (Expr : Node_Id) return Boolean;
    --  Returns True if the expression cannot possibly raise Constraint_Error.
@@ -231,6 +231,10 @@ 
    --  is accessed inside a nested procedure, and set Has_Up_Level_Access flag
    --  accordingly. This is currently only enabled for VM_Target /= No_VM.
 
+   procedure Check_No_Hidden_State (Id : Entity_Id);
+   --  Determine whether object or state Id introduces a hidden state. If this
+   --  is the case, emit an error.
+
    procedure Check_Potentially_Blocking_Operation (N : Node_Id);
    --  N is one of the statement forms that is a potentially blocking
    --  operation. If it appears within a protected action, emit warning.