diff options
| author | Yannick Moy <moy@adacore.com> | 2024-02-02 18:20:06 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-05-14 10:19:50 +0200 |
| commit | df48963b9553a51023c0d115bdf6205309e04bfe (patch) | |
| tree | 5e8ed8d6ba931aedfab087b456a47bdfed6dbdc3 /gcc/ada/sem_ch6.adb | |
| parent | 20dfaae2d1ba4749db13792105a32c5d8ef422e3 (diff) | |
| download | gcc-df48963b9553a51023c0d115bdf6205309e04bfe.zip gcc-df48963b9553a51023c0d115bdf6205309e04bfe.tar.gz gcc-df48963b9553a51023c0d115bdf6205309e04bfe.tar.bz2 | |
ada: Update of SPARK RM legality rules on ghost code
Update checking of ghost code after a small change in SPARK RM
rules 6.9(15) and 6.9(20), so that the Ghost assertion policy
that matters when checking the validity of a reference to a ghost entity
in an assertion expression is the Ghost assertion policy at the point
of declaration of the entity.
Also fix references to SPARK RM rules in comments, which were off by two
in many cases after the insertion of rules 13 and 14 regarding generic
instantiations.
gcc/ada/
* contracts.adb: Fix references to SPARK RM rules.
* freeze.adb: Same.
* ghost.adb: Fix references to SPARK RM rules.
(Check_Ghost_Context): Update checking of references to
ghost entities in assertion expressions.
* sem_ch6.adb: Fix references to SPARK RM rules.
* sem_prag.adb: Same.
Diffstat (limited to 'gcc/ada/sem_ch6.adb')
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 17f62d3..c0bfe87 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -11693,7 +11693,7 @@ package body Sem_Ch6 is Check_Private_Overriding (B_Typ); -- The Ghost policy in effect at the point of declaration -- or a tagged type and a primitive operation must match - -- (SPARK RM 6.9(16)). + -- (SPARK RM 6.9(18)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -11737,7 +11737,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration -- of a tagged type and a primitive operation must match - -- (SPARK RM 6.9(16)). + -- (SPARK RM 6.9(18)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -11770,7 +11770,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration of a -- tagged type and a primitive operation must match - -- (SPARK RM 6.9(16)). + -- (SPARK RM 6.9(18)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -12226,7 +12226,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration of a -- parent subprogram and an overriding subprogram must match - -- (SPARK RM 6.9(17)). + -- (SPARK RM 6.9(19)). Check_Ghost_Overriding (S, Overridden_Subp); end if; @@ -12389,7 +12389,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration -- of a parent subprogram and an overriding subprogram - -- must match (SPARK RM 6.9(17)). + -- must match (SPARK RM 6.9(19)). Check_Ghost_Overriding (E, S); end if; @@ -12598,7 +12598,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration -- of a parent subprogram and an overriding subprogram - -- must match (SPARK RM 6.9(17)). + -- must match (SPARK RM 6.9(19)). Check_Ghost_Overriding (S, E); @@ -12751,7 +12751,7 @@ package body Sem_Ch6 is -- The Ghost policy in effect at the point of declaration of a parent -- subprogram and an overriding subprogram must match - -- (SPARK RM 6.9(17)). + -- (SPARK RM 6.9(19)). Check_Ghost_Overriding (S, Overridden_Subp); |