[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Wed, 12 Oct 2016 13:53:46 +0000 (15:53 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Wed, 12 Oct 2016 13:53:46 +0000 (15:53 +0200)
2016-10-12  Ed Schonberg  <schonberg@adacore.com>

* lib-writ.adb (Write_ALI): Removal of unused file entries from
dependency list must be performed before the list is sorted,
so that the dependency number of other files is properly set-up
for use in tools that relate entity information to the unit in
which they are declared.

2016-10-12  Hristian Kirtchev  <kirtchev@adacore.com>

* exp_aggr.adb (Initialize_Ctrl_Array_Component):
Create a copy of the initialization expression to avoid sharing
it between multiple components.

2016-10-12  Yannick Moy  <moy@adacore.com>

* einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
in abtract states.
(Has_Non_Null_Visible_Refinement): Return true for patial refinement.
(Partial_Refinement_Constituents): New function returns the full or
partial refinement constituents depending on scope.
* sem_ch3.adb (Analyze_Declarations): Remove partial visible
refinements when exiting the scope of a package spec or body
and those partial refinements are not in scope afterwards.
* sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
abstract states of parent units with partial refinement so that
it is visible.
* sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
abstract state if any as having partial refinement in that scope.
(Analyze_Refined_Global_In_Decl_Part): Check constituent usage
based on full or partial refinement depending on scope.

2016-10-12  Ed Schonberg  <schonberg@adacore.com>

* exp_ch4.adb (Expand_N_Type_Conversion): If the target type
has an invariant aspect, insert invariant call at the proper
place in the code rather than rewriting the expression as an
expression with actions, to prevent spurious semantic errors on
the rewritten conversion when it is the object in a renaming.

From-SVN: r241048

gcc/ada/ChangeLog
gcc/ada/einfo.adb
gcc/ada/einfo.ads
gcc/ada/exp_aggr.adb
gcc/ada/exp_ch4.adb
gcc/ada/lib-writ.adb
gcc/ada/sem_ch3.adb
gcc/ada/sem_ch7.adb
gcc/ada/sem_ch7.ads
gcc/ada/sem_prag.adb

index 436f9a557148a82de4b6cf5808ef1caf145a0c76..db7b6c82b55e80c611bef8dd020be4418c97dcd5 100644 (file)
@@ -1,3 +1,43 @@
+2016-10-12  Ed Schonberg  <schonberg@adacore.com>
+
+       * lib-writ.adb (Write_ALI): Removal of unused file entries from
+       dependency list must be performed before the list is sorted,
+       so that the dependency number of other files is properly set-up
+       for use in tools that relate entity information to the unit in
+       which they are declared.
+
+2016-10-12  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * exp_aggr.adb (Initialize_Ctrl_Array_Component):
+       Create a copy of the initialization expression to avoid sharing
+       it between multiple components.
+
+2016-10-12  Yannick Moy  <moy@adacore.com>
+
+       * einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
+       in abtract states.
+       (Has_Non_Null_Visible_Refinement): Return true for patial refinement.
+       (Partial_Refinement_Constituents): New function returns the full or
+       partial refinement constituents depending on scope.
+       * sem_ch3.adb (Analyze_Declarations): Remove partial visible
+       refinements when exiting the scope of a package spec or body
+       and those partial refinements are not in scope afterwards.
+       * sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
+       abstract states of parent units with partial refinement so that
+       it is visible.
+       * sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
+       abstract state if any as having partial refinement in that scope.
+       (Analyze_Refined_Global_In_Decl_Part): Check constituent usage
+       based on full or partial refinement depending on scope.
+
+2016-10-12  Ed Schonberg  <schonberg@adacore.com>
+
+       * exp_ch4.adb (Expand_N_Type_Conversion): If the target type
+       has an invariant aspect, insert invariant call at the proper
+       place in the code rather than rewriting the expression as an
+       expression with actions, to prevent spurious semantic errors on
+       the rewritten conversion when it is the object in a renaming.
+
 2016-10-12  Hristian Kirtchev  <kirtchev@adacore.com>
 
        * exp_ch5.adb, sem_ch3.adb, exp_ch9.adb, a-tags.adb, sem_prag.adb,
index 1748efd0b660195cac03fe874939b134328465a2..dedc8a3312c3c6643b9f577b3554b9ae5ac7bbaa 100644 (file)
@@ -610,8 +610,8 @@ package body Einfo is
    --    Is_Actual_Subtype               Flag293
    --    Has_Pragma_Unused               Flag294
    --    Is_Ignored_Transient            Flag295
+   --    Has_Partial_Visible_Refinement  Flag296
 
-   --    (unused)                        Flag296
    --    (unused)                        Flag297
    --    (unused)                        Flag298
    --    (unused)                        Flag299
@@ -1682,6 +1682,12 @@ package body Einfo is
       return Flag232 (Id);
    end Has_Own_Invariants;
 
+   function Has_Partial_Visible_Refinement (Id : E) return B is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Flag296 (Id);
+   end Has_Partial_Visible_Refinement;
+
    function Has_Per_Object_Constraint (Id : E) return B is
    begin
       return Flag154 (Id);
@@ -4698,6 +4704,12 @@ package body Einfo is
       Set_Flag232 (Id, V);
    end Set_Has_Own_Invariants;
 
+   procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Flag296 (Id, V);
+   end Set_Has_Partial_Visible_Refinement;
+
    procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
    begin
       Set_Flag154 (Id, V);
@@ -7485,13 +7497,14 @@ package body Einfo is
       pragma Assert (Ekind (Id) = E_Abstract_State);
       Constits := Refinement_Constituents (Id);
 
-      --  For a refinement to be non-null, the first constituent must be
-      --  anything other than null.
+      --  A partial refinement is always non-null. For a full refinement to be
+      --  non-null, the first constituent must be anything other than null.
 
       return
-        Has_Visible_Refinement (Id)
-          and then Present (Constits)
-          and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
+        Has_Partial_Visible_Refinement (Id)
+          or else (Has_Visible_Refinement (Id)
+                    and then Present (Constits)
+                    and then Nkind (Node (First_Elmt (Constits))) /= N_Null);
    end Has_Non_Null_Visible_Refinement;
 
    -----------------------------
@@ -8370,6 +8383,29 @@ package body Einfo is
       return Empty;
    end Partial_Invariant_Procedure;
 
+   -------------------------------------
+   -- Partial_Refinement_Constituents --
+   -------------------------------------
+
+   function Partial_Refinement_Constituents (Id : E) return L is
+      Constits : Elist_Id;
+
+   begin
+      --  "Refinement" is a concept applicable only to abstract states
+
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Constits := Refinement_Constituents (Id);
+
+      --  A refinement may be partially visible when objects declared in the
+      --  private part of a package are subject to a Part_Of indicator.
+
+      if No (Constits) then
+         Constits := Part_Of_Constituents (Id);
+      end if;
+
+      return Constits;
+   end Partial_Refinement_Constituents;
+
    ------------------------
    -- Predicate_Function --
    ------------------------
index 1085862f9b60f8fe85db34c294ad85d72388f617..405d97815affef87244a48d2ffbe95fd643c724f 100644 (file)
@@ -1812,6 +1812,14 @@ package Einfo is
 --       one invariant of its own. The flag is also set on the full view of a
 --       private extension or a private type for completeness.
 
+--    Has_Partial_Visible_Refinement (Flag296)
+--       Defined in E_Abstract_State entities. Set when a state has at least
+--       one refinement constituent subject to indicator Part_Of, and analysis
+--       is in the region between the declaration of the first constituent for
+--       this abstract state (in the private part of the package) and the end
+--       of the package spec or body with visibility over this private part
+--       (which includes the package itself and its child packages).
+
 --    Has_Per_Object_Constraint (Flag154)
 --       Defined in E_Component entities. Set if the subtype of the component
 --       has a per object constraint. Per object constraints result from the
@@ -3780,6 +3788,11 @@ package Einfo is
 --       Note: the reason this is marked as a synthesized attribute is that the
 --       way this is stored is as an element of the Subprograms_For_Type field.
 
+--    Partial_Refinement_Constituents (synthesized)
+--       Present in abstract state entities. Contains the constituents that
+--       refine the state in its private part, in other words, all the hidden
+--       states that indicate this abstract state in a Part_Of aspect/pragma.
+
 --    Partial_View_Has_Unknown_Discr (Flag280)
 --       Present in all types. Set to Indicate that the partial view of a type
 --       has unknown discriminants. A default initialization of an object of
@@ -5619,6 +5632,7 @@ package Einfo is
    --    Non_Limited_View                    (Node19)
    --    Encapsulating_State                 (Node32)
    --    From_Limited_With                   (Flag159)
+   --    Has_Partial_Visible_Refinement      (Flag296)
    --    Has_Visible_Refinement              (Flag263)
    --    Has_Non_Limited_View                (synth)
    --    Has_Non_Null_Visible_Refinement     (synth)
@@ -5626,6 +5640,7 @@ package Einfo is
    --    Is_External_State                   (synth)
    --    Is_Null_State                       (synth)
    --    Is_Synchronized_State               (synth)
+   --    Partial_Refinement_Constituents     (synth)
 
    --  E_Access_Protected_Subprogram_Type
    --    Equivalent_Type                     (Node18)
@@ -6977,6 +6992,7 @@ package Einfo is
    function Has_Object_Size_Clause              (Id : E) return B;
    function Has_Out_Or_In_Out_Parameter         (Id : E) return B;
    function Has_Own_Invariants                  (Id : E) return B;
+   function Has_Partial_Visible_Refinement      (Id : E) return B;
    function Has_Per_Object_Constraint           (Id : E) return B;
    function Has_Pragma_Controlled               (Id : E) return B;
    function Has_Pragma_Elaborate_Body           (Id : E) return B;
@@ -7412,6 +7428,7 @@ package Einfo is
    function Number_Entries                      (Id : E) return Nat;
    function Number_Formals                      (Id : E) return Pos;
    function Parameter_Mode                      (Id : E) return Formal_Kind;
+   function Partial_Refinement_Constituents     (Id : E) return L;
    function Primitive_Operations                (Id : E) return L;
    function Root_Type                           (Id : E) return E;
    function Safe_Emax_Value                     (Id : E) return U;
@@ -7652,6 +7669,7 @@ package Einfo is
    procedure Set_Has_Object_Size_Clause          (Id : E; V : B := True);
    procedure Set_Has_Out_Or_In_Out_Parameter     (Id : E; V : B := True);
    procedure Set_Has_Own_Invariants              (Id : E; V : B := True);
+   procedure Set_Has_Partial_Visible_Refinement  (Id : E; V : B := True);
    procedure Set_Has_Per_Object_Constraint       (Id : E; V : B := True);
    procedure Set_Has_Pragma_Controlled           (Id : E; V : B := True);
    procedure Set_Has_Pragma_Elaborate_Body       (Id : E; V : B := True);
@@ -8444,6 +8462,7 @@ package Einfo is
    pragma Inline (Has_Object_Size_Clause);
    pragma Inline (Has_Out_Or_In_Out_Parameter);
    pragma Inline (Has_Own_Invariants);
+   pragma Inline (Has_Partial_Visible_Refinement);
    pragma Inline (Has_Per_Object_Constraint);
    pragma Inline (Has_Pragma_Controlled);
    pragma Inline (Has_Pragma_Elaborate_Body);
@@ -8959,6 +8978,7 @@ package Einfo is
    pragma Inline (Set_Has_Object_Size_Clause);
    pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
    pragma Inline (Set_Has_Own_Invariants);
+   pragma Inline (Set_Has_Partial_Visible_Refinement);
    pragma Inline (Set_Has_Per_Object_Constraint);
    pragma Inline (Set_Has_Pragma_Controlled);
    pragma Inline (Set_Has_Pragma_Elaborate_Body);
index 33374d358828320fb160cd0b33e67666944b3989..e83b07affdd16921ba5c483216dc8162af9d9cc2 100644 (file)
@@ -1277,6 +1277,7 @@ package body Exp_Aggr is
          is
             Act_Aggr   : Node_Id;
             Act_Stmts  : List_Id;
+            Expr       : Node_Id;
             Fin_Call   : Node_Id;
             Hook_Clear : Node_Id;
 
@@ -1285,20 +1286,29 @@ package body Exp_Aggr is
             --  in-place expansion.
 
          begin
+            --  Duplicate the initialization expression in case the context is
+            --  a multi choice list or an "others" choice which plugs various
+            --  holes in the aggregate. As a result the expression is no longer
+            --  shared between the various components and is reevaluated for
+            --  each such component.
+
+            Expr := New_Copy_Tree (Init_Expr);
+            Set_Parent (Expr, Parent (Init_Expr));
+
             --  Perform a preliminary analysis and resolution to determine what
             --  the initialization expression denotes. An unanalyzed function
             --  call may appear as an identifier or an indexed component.
 
-            if Nkind_In (Init_Expr, N_Function_Call,
-                                    N_Identifier,
-                                    N_Indexed_Component)
-              and then not Analyzed (Init_Expr)
+            if Nkind_In (Expr, N_Function_Call,
+                               N_Identifier,
+                               N_Indexed_Component)
+              and then not Analyzed (Expr)
             then
-               Preanalyze_And_Resolve (Init_Expr, Comp_Typ);
+               Preanalyze_And_Resolve (Expr, Comp_Typ);
             end if;
 
             In_Place_Expansion :=
-              Nkind (Init_Expr) = N_Function_Call
+              Nkind (Expr) = N_Function_Call
                 and then not Is_Limited_Type (Comp_Typ);
 
             --  The initialization expression is a controlled function call.
@@ -1315,7 +1325,7 @@ package body Exp_Aggr is
                --  generation of a transient scope, which leads to out-of-order
                --  adjustment and finalization.
 
-               Set_No_Side_Effect_Removal (Init_Expr);
+               Set_No_Side_Effect_Removal (Expr);
 
                --  When the transient component initialization is related to a
                --  range or an "others", keep all generated statements within
@@ -1341,7 +1351,7 @@ package body Exp_Aggr is
                Process_Transient_Component
                  (Loc        => Loc,
                   Comp_Typ   => Comp_Typ,
-                  Init_Expr  => Init_Expr,
+                  Init_Expr  => Expr,
                   Fin_Call   => Fin_Call,
                   Hook_Clear => Hook_Clear,
                   Aggr       => Act_Aggr,
@@ -1356,7 +1366,7 @@ package body Exp_Aggr is
             Initialize_Array_Component
               (Arr_Comp  => Arr_Comp,
                Comp_Typ  => Comp_Typ,
-               Init_Expr => Init_Expr,
+               Init_Expr => Expr,
                Stmts     => Stmts);
 
             --  At this point the array element is fully initialized. Complete
index 7931c13ee9231b6d29d521b9e465cad004ad53c3..905467b8a6b28123e1e8f943360a29c3d1ec5a7d 100644 (file)
@@ -10577,15 +10577,16 @@ package body Exp_Ch4 is
       end if;
 
       --  Check for case of converting to a type that has an invariant
-      --  associated with it. This required an invariant check. We convert
+      --  associated with it. This requires an invariant check. We insert
+      --  a call:
 
-      --    typ (expr)
+      --        invariant_check (typ (expr))
 
-      --  into
-
-      --    do invariant_check (typ (expr)) in typ (expr);
-
-      --  using Duplicate_Subexpr to avoid multiple side effects
+      --  in the code, after removing side effects from the expression.
+      --  This is clearer than replacing the conversion into an expression
+      --  with actions, because the context may impose additional actions
+      --  (tag checks, membership tests, etc.) that conflict with this
+      --  rewriting (used previously).
 
       --  Note: the Comes_From_Source check, and then the resetting of this
       --  flag prevents what would otherwise be an infinite recursion.
@@ -10595,12 +10596,8 @@ package body Exp_Ch4 is
         and then Comes_From_Source (N)
       then
          Set_Comes_From_Source (N, False);
-         Rewrite (N,
-           Make_Expression_With_Actions (Loc,
-             Actions    => New_List (
-               Make_Invariant_Call (Duplicate_Subexpr (N))),
-             Expression => Duplicate_Subexpr_No_Checks (N)));
-         Analyze_And_Resolve (N, Target_Type);
+         Remove_Side_Effects (N);
+         Insert_Action (N, Make_Invariant_Call (Duplicate_Subexpr (N)));
          goto Done;
       end if;
 
index b78e3eb3855283e818de0bbfda2aa87e4b41e58e..0cd615fd50458780883f0917771c313ff5c51509 100644 (file)
@@ -990,8 +990,27 @@ package body Lib.Writ is
          if Cunit_Entity (Unum) = Empty
            or else not From_Limited_With (Cunit_Entity (Unum))
          then
-            Num_Sdep := Num_Sdep + 1;
-            Sdep_Table (Num_Sdep) := Unum;
+            --  Units that are not analyzed need not appear in the dependency
+            --  list. These units are either units appearing in limited_with
+            --  clauses of other units, or units loaded for inlining that end
+            --  up not inlined by a later decision of the inlining code, to
+            --  prevent circularities. We want to exclude these files from the
+            --  list of dependencies, so that the dependency number of other
+            --  is correctly set, as that number is used by cross-reference
+            --  tools to relate entity information to the unit in which they
+            --  are declared.
+
+            if Present (Cunit_Entity (Unum))
+              and then Ekind (Cunit_Entity (Unum)) = E_Void
+              and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
+              and then Serious_Errors_Detected = 0
+            then
+               null;
+
+            else
+               Num_Sdep := Num_Sdep + 1;
+               Sdep_Table (Num_Sdep) := Unum;
+            end if;
          end if;
       end loop;
 
@@ -1433,32 +1452,6 @@ package body Lib.Writ is
             Units.Table (Unum).Dependency_Num := J;
             Sind := Units.Table (Unum).Source_Index;
 
-            --  The dependency table also contains units that appear in the
-            --  context of a unit loaded through a limited_with clause. These
-            --  units are never analyzed, and thus the main unit does not
-            --  really have a dependency on them. Subunits are always compiled
-            --  in the context of the parent, and their file table entries are
-            --  not properly decorated, they are recognized syntactically.
-
-            --  This optimization is disabled when inline is active, because
-            --  inline may propose some bodies for inlining, and decide later
-            --  that they may lead to circularities, in which case they are
-            --  also left unanalyzed in the file table. There is no simple way
-            --  to distinguish between the two kinds of unanalyzed entries,
-            --  so simplest is to skip this step.
-
-            --  Actually, this optimization is always disabled, because it
-            --  breaks gnatfind.
-
-            if False -- ???
-              and then Present (Cunit_Entity (Unum))
-              and then Ekind (Cunit_Entity (Unum)) = E_Void
-              and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
-              and then not Inline_Active
-            then
-               goto Next_Unit;
-            end if;
-
             Write_Info_Initiate ('D');
             Write_Info_Char (' ');
 
@@ -1534,9 +1527,6 @@ package body Lib.Writ is
             end if;
 
             Write_Info_EOL;
-
-         <<Next_Unit>>
-            null;
          end loop;
       end;
 
index 3b9435f92f7ccb6564ba47fea7bccb924002f8f7..a97d0172100896b1ae492ed2137b355f1d0bb2ad 100644 (file)
@@ -2178,10 +2178,17 @@ package body Sem_Ch3 is
       --  case, add a proper spec if the body lacks one. The spec is inserted
       --  before Body_Decl and immediately analyzed.
 
+      procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
+      --  Spec_Id is the entity of a package that may define abstract states,
+      --  and in the case of a child unit, whose ancestors may define abstract
+      --  states. If the states have partial visible refinement, remove the
+      --  partial visibility of each constituent at the end of the package
+      --  spec and body declarations.
+
       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.
+      --  constituent at the end of the package body declaration.
 
       -----------------
       -- Adjust_Decl --
@@ -2335,6 +2342,29 @@ package body Sem_Ch3 is
          Insert_Before_And_Analyze (Body_Decl, Decl);
       end Handle_Late_Controlled_Primitive;
 
+      ----------------------------------------
+      -- Remove_Partial_Visible_Refinements --
+      ----------------------------------------
+
+      procedure Remove_Partial_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_Partial_Visible_Refinement (Node (State_Elmt), False);
+               Next_Elmt (State_Elmt);
+            end loop;
+         end if;
+
+         --  For a child unit, also hide the partial state refinement from
+         --  ancestor packages.
+
+         if Is_Child_Unit (Spec_Id) then
+            Remove_Partial_Visible_Refinements (Scope (Spec_Id));
+         end if;
+      end Remove_Partial_Visible_Refinements;
+
       --------------------------------
       -- Remove_Visible_Refinements --
       --------------------------------
@@ -2576,6 +2606,15 @@ package body Sem_Ch3 is
             --  restore the original state conditions.
 
             Remove_Visible_Refinements (Corresponding_Spec (Context));
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
+
+         elsif Nkind (Context) = N_Package_Declaration then
+
+            --  Partial state refinements are visible up to the end of the
+            --  package spec declarations. Hide the partial state refinements
+            --  from visibility to restore the original state conditions.
+
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
          end if;
 
          --  Verify that all abstract states found in any package declared in
index 4a3b2de04297a81405008c4a4957e79c801e8cb1..55ec81e1f51189aecca7590da8c6066ee0e6e35a 100644 (file)
@@ -2275,6 +2275,34 @@ package body Sem_Ch7 is
          Next_Entity (Id);
       end loop;
 
+      --  An abstract state is partially refined when it has at least one
+      --  Part_Of constituent. Since these constituents are being installed
+      --  into visibility, update the partial refinement status of any state
+      --  defined in the associated package, subject to at least one Part_Of
+      --  constituent.
+
+      if Ekind_In (P, E_Generic_Package, E_Package) then
+         declare
+            States     : constant Elist_Id := Abstract_States (P);
+            State_Elmt : Elmt_Id;
+            State_Id   : Entity_Id;
+
+         begin
+            if Present (States) then
+               State_Elmt := First_Elmt (States);
+               while Present (State_Elmt) loop
+                  State_Id := Node (State_Elmt);
+
+                  if Present (Part_Of_Constituents (State_Id)) then
+                     Set_Has_Partial_Visible_Refinement (State_Id);
+                  end if;
+
+                  Next_Elmt (State_Elmt);
+               end loop;
+            end if;
+         end;
+      end if;
+
       --  Indicate that the private part is currently visible, so it can be
       --  properly reset on exit.
 
index 2963aed984caa93ffe3b117fa10e197cc6d35501..4e645adf7fb4226f1997c072a37a1a53215026fe 100644 (file)
@@ -46,10 +46,10 @@ package Sem_Ch7 is
    --  On entrance to a package body, make declarations in package spec
    --  immediately visible.
    --
-   --  When compiling the body of a package,  both routines are called in
+   --  When compiling the body of a package, both routines are called in
    --  succession. When compiling the body of a child package, the call
    --  to Install_Private_Declaration is immediate for private children,
-   --  but is deferred until the compilation of the  private part of the
+   --  but is deferred until the compilation of the private part of the
    --  child for public child packages.
 
    function Unit_Requires_Body
index d95cab895b6c65b30371354a0c585bbbb23cfde0..9b9fe82985d891ed491ad12238dd4af7776b525b 100644 (file)
@@ -3410,6 +3410,13 @@ package body Sem_Prag is
 
          Append_Elmt (Var_Id, Constits);
          Set_Encapsulating_State (Var_Id, Encap_Id);
+
+         --  A Part_Of constituent partially refines an abstract state. This
+         --  property does not apply to protected or task units.
+
+         if Ekind (Encap_Id) = E_Abstract_State then
+            Set_Has_Partial_Visible_Refinement (Encap_Id);
+         end if;
       end if;
 
       --  Emit a clarification message when the encapsulator is undefined,
@@ -18717,7 +18724,7 @@ package body Sem_Prag is
 
             Add_Contract_Item (N, Item_Id);
 
-            --  A variable may act as consituent of a single concurrent type
+            --  A variable may act as constituent of a single concurrent type
             --  which in turn could be declared after the variable. Due to this
             --  discrepancy, the full analysis of indicator Part_Of is delayed
             --  until the end of the enclosing declarative region (see routine
@@ -24051,7 +24058,7 @@ package body Sem_Prag is
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             Posted       : Boolean := False;
@@ -24614,7 +24621,7 @@ package body Sem_Prag is
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits      : constant Elist_Id :=
-                              Refinement_Constituents (State_Id);
+                              Partial_Refinement_Constituents (State_Id);
             Constit_Elmt  : Elmt_Id;
             Constit_Id    : Entity_Id;
             Has_Missing   : Boolean := False;
@@ -24753,7 +24760,7 @@ package body Sem_Prag is
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             In_Seen      : Boolean := False;
@@ -24853,7 +24860,7 @@ package body Sem_Prag is
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits     : constant Elist_Id :=
-                             Refinement_Constituents (State_Id);
+                             Partial_Refinement_Constituents (State_Id);
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
             Posted       : Boolean := False;
@@ -24952,7 +24959,7 @@ package body Sem_Prag is
 
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constits      : constant Elist_Id :=
-                              Refinement_Constituents (State_Id);
+                              Partial_Refinement_Constituents (State_Id);
             Constit_Elmt  : Elmt_Id;
             Constit_Id    : Entity_Id;
             Proof_In_Seen : Boolean := False;
@@ -25083,7 +25090,10 @@ package body Sem_Prag is
 
             if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
              and then Present (Encapsulating_State (Item_Id))
-             and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+             and then
+               (Has_Visible_Refinement (Encapsulating_State (Item_Id))
+                  or else
+                Has_Partial_Visible_Refinement (Encapsulating_State (Item_Id)))
              and then Contains (States, Encapsulating_State (Item_Id))
             then
                if Global_Mode = Name_Input then
@@ -25438,10 +25448,10 @@ package body Sem_Prag is
       --  Non-instance case
 
       else
-         --  The corresponding Global pragma must mention at least one state
-         --  witha visible refinement at the point Refined_Global is processed.
-         --  States with null refinements need Refined_Global pragma
-         --  (SPARK RM 7.2.4(2)).
+         --  The corresponding Global pragma must mention at least one
+         --  state with a visible refinement at the point Refined_Global
+         --  is processed. States with null refinements need Refined_Global
+         --  pragma (SPARK RM 7.2.4(2)).
 
          if not Has_In_State
            and then not Has_In_Out_State