[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 81130b59c294769758c97e4670764f3b205ce9d6..df2475f5e596f908204eb9c21a7e2724c0cdc0ce 100644 (file)
--- 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