diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-05-06 17:19:56 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-07-06 07:35:01 -0400 |
| commit | 114efadf43a21f1c56b2b79cdabc0bea91ca68d5 (patch) | |
| tree | 8a5334f7ad768ebf8eb03835df67fcd521bd0e9c /gcc | |
| parent | a34da56b26df1db73c20d36ae753173999bd46da (diff) | |
| download | gcc-114efadf43a21f1c56b2b79cdabc0bea91ca68d5.zip gcc-114efadf43a21f1c56b2b79cdabc0bea91ca68d5.tar.gz gcc-114efadf43a21f1c56b2b79cdabc0bea91ca68d5.tar.bz2 | |
[Ada] Simplify implicit loading of Tasking_State in GNATprove_Mode
gcc/ada/
* sem_attr.adb (Analyze_Attribute): Reuse SPARK_Implicit_Load.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/sem_attr.adb | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 81130b5..df2475f 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -7245,22 +7245,17 @@ package body Sem_Attr is -- See SPARK RM 9(18) for the relevant rule. if GNATprove_Mode then - declare - Unused : Entity_Id; - - begin - case Attr_Id is - when Attribute_Callable - | Attribute_Caller - | Attribute_Count - | Attribute_Terminated - => - Unused := RTE (RE_Tasking_State); + case Attr_Id is + when Attribute_Callable + | Attribute_Caller + | Attribute_Count + | Attribute_Terminated + => + SPARK_Implicit_Load (RE_Tasking_State); - when others => - null; - end case; - end; + when others => + null; + end case; end if; -- All errors raise Bad_Attribute, so that we get out before any further |