public inbox for gcc-cvs@sourceware.org help / color / mirror / Atom feed
From: Marc Poulhi?s <dkm@gcc.gnu.org> To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement Date: Mon, 28 Nov 2022 12:03:53 +0000 (GMT) [thread overview] Message-ID: <20221128120353.81A393858C62@sourceware.org> (raw) 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 "
reply other threads:[~2022-11-28 12:03 UTC|newest] Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20221128120353.81A393858C62@sourceware.org \ --to=dkm@gcc.gnu.org \ --cc=gcc-cvs@gcc.gnu.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).