From: Yannick Moy <m...@adacore.com> 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. Tested on x86_64-pc-linux-gnu, committed on master. --- 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 " -- 2.34.1