[gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement

[gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement

[Marc Poulhi?s]

https://gcc.gnu.org/g:83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f

commit r13-4358-g83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Nov 24 16:27:37 2022 +0100

    ada: Implement change to SPARK RM rule on state refinement
    
    SPARK RM 7.1.4(4) does not mandate anymore that a package with abstract
    states has a completing body, unless the package state is mentioned in
    Part_Of specifications. Implement that change.
    
    gcc/ada/
    
            * sem_prag.adb (Check_Part_Of_Abstract_State): Add verification
            related to use of Part_Of, so that constituents in private childs
            that refer to state in a sibling or parent unit force that unit to
            have a body.
            * sem_util.adb (Check_State_Refinements): Drop the requirement to
            have always a package body for state refinement, when the package
            state is mentioned in no Part_Of specification.
            * sem_ch3.adb (Analyze_Declarations): Refresh SPARK refs in comment.
            * sem_ch7.adb (Analyze_Package_Declaration): Likewise.

Diff:
---
 gcc/ada/sem_ch3.adb  |  3 ++-
 gcc/ada/sem_ch7.adb  | 10 +++++-----
 gcc/ada/sem_prag.adb | 16 ++++++++++++++++
 gcc/ada/sem_util.adb | 14 ++++++++++----
 4 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index ce5a00b7fc8..61386e27feb 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2942,7 +2942,8 @@ package body Sem_Ch3 is
          --  Verify that all abstract states found in any package declared in
          --  the input declarative list have proper refinements. The check is
          --  performed only when the context denotes a block, entry, package,
-         --  protected, subprogram, or task body (SPARK RM 7.2.2(3)).
+         --  protected, subprogram, or task body (SPARK RM 7.1.4(4) and SPARK
+         --  RM 7.2.2(3)).
 
          Check_State_Refinements (Context);
 
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 0fb9fe10ff6..284706981d6 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -1243,11 +1243,11 @@ package body Sem_Ch7 is
          Check_Completion;
 
          --  If the package spec does not require an explicit body, then all
-         --  abstract states declared in nested packages cannot possibly get
-         --  a proper refinement (SPARK RM 7.2.2(3)). This check is performed
-         --  only when the compilation unit is the main unit to allow for
-         --  modular SPARK analysis where packages do not necessarily have
-         --  bodies.
+         --  abstract states declared in nested packages cannot possibly get a
+         --  proper refinement (SPARK RM 7.1.4(4) and SPARK RM 7.2.2(3)). This
+         --  check is performed only when the compilation unit is the main
+         --  unit to allow for modular SPARK analysis where packages do not
+         --  necessarily have bodies.
 
          if Is_Comp_Unit then
             Check_State_Refinements
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0a91518cff9..27bd879903e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -63,6 +63,7 @@ with Sem;            use Sem;
 with Sem_Aux;        use Sem_Aux;
 with Sem_Ch3;        use Sem_Ch3;
 with Sem_Ch6;        use Sem_Ch6;
+with Sem_Ch7;        use Sem_Ch7;
 with Sem_Ch8;        use Sem_Ch8;
 with Sem_Ch12;       use Sem_Ch12;
 with Sem_Ch13;       use Sem_Ch13;
@@ -3567,6 +3568,21 @@ package body Sem_Prag is
             return;
          end if;
 
+         --  In the case of state in a (descendant of a private) child which
+         --  is Part_Of the state of another package, the package defining the
+         --  encapsulating abstract state should have a body, to ensure that it
+         --  has a state refinement (SPARK RM 7.1.4(4)).
+
+         if Enclosing_Comp_Unit_Node (Encap_Id) /=
+            Enclosing_Comp_Unit_Node (Item_Id)
+           and then not Unit_Requires_Body (Scope (Encap_Id))
+         then
+            SPARK_Msg_N
+              ("indicator Part_Of must denote abstract state of package "
+               & "with a body (SPARK RM 7.1.4(4))", Indic);
+            return;
+         end if;
+
          --  At this point it is known that the Part_Of indicator is legal
 
          Legal := True;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index f331b4b78ba..a13d9ebef5b 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5450,12 +5450,18 @@ package body Sem_Util is
                while Present (State_Elmt) loop
                   State_Id := Node (State_Elmt);
 
-                  --  Emit an error when a non-null state lacks any form of
-                  --  refinement.
+                  --  Emit an error when a non-null state lacks refinement,
+                  --  but has Part_Of constituents or there is a package
+                  --  body (SPARK RM 7.1.4(4)). Constituents in private
+                  --  child packages, which are not known at this stage,
+                  --  independently require the existence of a package body.
 
                   if not Is_Null_State (State_Id)
-                    and then not Has_Null_Refinement (State_Id)
-                    and then not Has_Non_Null_Refinement (State_Id)
+                    and then No (Refinement_Constituents (State_Id))
+                    and then
+                      (Present (Part_Of_Constituents (State_Id))
+                         or else
+                       Present (Body_Id))
                   then
                      Error_Msg_N ("state & requires refinement", State_Id);
                      Error_Msg_N ("\package body should have Refined_State "