public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement
@ 2022-11-28 12:03 Marc Poulhi?s
0 siblings, 0 replies; only message in thread
From: Marc Poulhi?s @ 2022-11-28 12:03 UTC (permalink / raw)
To: gcc-cvs
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 "
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-11-28 12:03 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-11-28 12:03 [gcc r13-4358] ada: Implement change to SPARK RM rule on state refinement Marc Poulhi?s
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).