From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 81A393858C62; Mon, 28 Nov 2022 12:03:53 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 81A393858C62 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1669637033; bh=rEC9H+P8g3EiqI58pN2J5gHs+R3afFJfDWnWHsF4IwQ=; h=From:To:Subject:Date:From; b=hldW0cNBoI0iSEof5Arb3KGw4G1IG5ssN5fMuY8E04xv1XsqyAfmPBB7u/vrC0VqI 8uMy4ZYtmsrdc30AdQajKvl3njxLCATtD+dVbsF/vBmbKoCPzJGatuEYcOmZ+XuBl3 u6wbOP6fGxIaVK6aNmaBVLVIjLaPgMcDn4Eb4SOQ= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 2b293a949c0fbe21e47c4bc99f807dc941c02bb6 X-Git-Newrev: 83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f Message-Id: <20221128120353.81A393858C62@sourceware.org> Date: Mon, 28 Nov 2022 12:03:53 +0000 (GMT) List-Id: https://gcc.gnu.org/g:83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f commit r13-4358-g83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f Author: Yannick Moy 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 "