From: Piotr Trojanek <trojanek@adacore.com>
Date: Wed, 6 May 2020 15:19:56 +0000 (+0200)
Subject: [Ada] Simplify implicit loading of Tasking_State in GNATprove_Mode
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=114efadf43a21f1c56b2b79cdabc0bea91ca68d5;p=gcc.git

[Ada] Simplify implicit loading of Tasking_State in GNATprove_Mode

gcc/ada/

	* sem_attr.adb (Analyze_Attribute): Reuse SPARK_Implicit_Load.
---

diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 81130b59c29..df2475f5e59 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