diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2021-01-29 12:16:17 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-05-07 05:29:04 -0400 |
| commit | a3e2584e85d91d0ab076c3f603bc0179921dbd82 (patch) | |
| tree | 8aa7e6ca2de873ce9c5856589b4d9452ac521333 /gcc | |
| parent | 3a700c5fef18b2f339e464eec5e12a3b9956edd3 (diff) | |
| download | gcc-a3e2584e85d91d0ab076c3f603bc0179921dbd82.zip gcc-a3e2584e85d91d0ab076c3f603bc0179921dbd82.tar.gz gcc-a3e2584e85d91d0ab076c3f603bc0179921dbd82.tar.bz2 | |
[Ada] Attribute Address is not an interfering context in SPARK
gcc/ada/
* sem_res.adb (Flag_Object): Ignore prefixes of attribute
Address.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/sem_res.adb | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index bd950f5..898f317 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3749,6 +3749,19 @@ package body Sem_Res is begin case Nkind (N) is + + -- Do not consider object name appearing in the prefix of + -- attribute Address as a read. + + when N_Attribute_Reference => + + -- Prefix of attribute Address denotes an object, program + -- unit, or label; none of them needs to be flagged here. + + if Attribute_Name (N) = Name_Address then + return Skip; + end if; + -- Do not consider nested function calls because they have -- already been processed during their own resolution. |