diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2023-02-08 00:54:06 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-25 09:44:14 +0200 |
| commit | 7b67bfab289d7f50beed51ca72717be5a8154f3b (patch) | |
| tree | 161df46da1c463430cad96fa6b9a05e6e47edc16 /gcc/ada/sem_attr.adb | |
| parent | 53bd7622de70a4ca4a25cac953da3be2a24bc3c8 (diff) | |
| download | gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.zip gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.tar.gz gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.tar.bz2 | |
ada: Restrict use of formal parameters within exceptional cases
Restrict references to formal parameters within the new SPARK aspect
Exceptional_Cases and allow occurrences of 'Old in this aspect.
gcc/ada/
* sem_attr.adb
(Analyze_Attribute_Old_Result): Allow uses of 'Old and 'Result within
the new aspect.
* sem_res.adb
(Within_Exceptional_Cases_Consequence): New utility routine.
(Resolve_Entity_Name): Restrict use of formal parameters within the
new aspect.
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 bc4e3cf..0cfc2da2 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1423,6 +1423,14 @@ package body Sem_Attr is elsif Prag_Nam = Name_Contract_Cases then Check_Placement_In_Contract_Cases (Prag); + -- Attributes 'Old and 'Result are allowed to appear in + -- consequence of aspect or pragma Exceptional_Cases. We already + -- examined the exception_choice part of contract syntax, so we + -- can accept all remaining occurrences within the pragma. + + elsif Prag_Nam = Name_Exceptional_Cases then + null; + -- Attribute 'Result is allowed to appear in aspect or pragma -- [Refined_]Depends (SPARK RM 6.1.5(11)). |