Explicit External aspect was an equivalant to an implicit default. It was only
needed as a workaround for a frontend bug. (If it meant to serve as
documentation, there should be explicit Effective_Reads and Effective_Writes
set to False too.)
No test, because these changes are semantically neutral.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-21 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* libgnarl/a-reatim.ads (Clock_Time): Remove External aspect.
* libgnarl/a-taside.ads (Tasking_State): Likewise.
* libgnat/a-calend.ads (Clock_Time): Likewise.--- gcc/ada/libgnarl/a-reatim.ads
+++ gcc/ada/libgnarl/a-reatim.ads
@@ -38,9 +38,7 @@ pragma Elaborate_All (System.Task_Primitives.Operations);
package Ada.Real_Time with
SPARK_Mode,
- Abstract_State => (Clock_Time with Synchronous,
- External => (Async_Readers,
- Async_Writers)),
+ Abstract_State => (Clock_Time with Synchronous),
Initializes => Clock_Time
is
--- gcc/ada/libgnarl/a-taside.ads
+++ gcc/ada/libgnarl/a-taside.ads
@@ -38,9 +38,7 @@ with System.Tasking;
package Ada.Task_Identification with
SPARK_Mode,
- Abstract_State => (Tasking_State with Synchronous,
- External => (Async_Readers,
- Async_Writers)),
+ Abstract_State => (Tasking_State with Synchronous),
Initializes => Tasking_State
is
pragma Preelaborate;
--- gcc/ada/libgnat/a-calend.ads
+++ gcc/ada/libgnat/a-calend.ads
@@ -35,9 +35,7 @@
package Ada.Calendar with
SPARK_Mode,
- Abstract_State => (Clock_Time with Synchronous,
- External => (Async_Readers,
- Async_Writers)),
+ Abstract_State => (Clock_Time with Synchronous),
Initializes => Clock_Time
is
