diff options
| author | Yannick Moy <moy@adacore.com> | 2022-11-24 16:27:37 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-11-28 13:02:31 +0100 |
| commit | 83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f (patch) | |
| tree | 70e71a68004e8053d451c58c5d08892b5f950749 /libgcc | |
| parent | 2b293a949c0fbe21e47c4bc99f807dc941c02bb6 (diff) | |
| download | gcc-83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f.zip gcc-83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f.tar.gz gcc-83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f.tar.bz2 | |
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.
Diffstat (limited to 'libgcc')
0 files changed, 0 insertions, 0 deletions