[COMMITTED] ada: Implement change to SPARK RM rule on state refinement
Commit Message
From: Yannick Moy <moy@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(-)
@@ -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);
@@ -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
@@ -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;
@@ -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 "