From 114efadf43a21f1c56b2b79cdabc0bea91ca68d5 Mon Sep 17 00:00:00 2001
From: Piotr Trojanek <trojanek@adacore.com>
Date: Wed, 6 May 2020 17:19:56 +0200
Subject: [PATCH] [Ada] Simplify implicit loading of Tasking_State in
 GNATprove_Mode

gcc/ada/

	* sem_attr.adb (Analyze_Attribute): Reuse SPARK_Implicit_Load.
---
 gcc/ada/sem_attr.adb | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

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
-- 
2.30.2