diff options
Diffstat (limited to 'gcc/ada/sem_attr.adb')
| -rw-r--r-- | gcc/ada/sem_attr.adb | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 1b6d3ef30b6..f2556a7f2a4 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -565,6 +565,14 @@ package body Sem_Attr is -- Start of processing for Analyze_Access_Attribute begin + -- Access attribute is not allowed in SPARK or ALFA + + if Formal_Verification_Mode and then Comes_From_Source (N) then + Error_Attr_P ("|~~% attribute is not allowed"); + end if; + + -- Proceed with analysis + Check_E0; if Nkind (P) = N_Character_Literal then |