From 83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 24 Nov 2022 16:27:37 +0100 Subject: 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. --- gcc/ada/sem_ch3.adb | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'gcc/ada/sem_ch3.adb') diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index ce5a00b..61386e2 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); -- cgit v1.1