In GNATprove flow analysis is not aware of implicitly evaluated
routines, e.g. subtype predicates and user-defined equality for record
types. Therefore SPARK 2014 mandates both routines to not reference any
globals. Likewise, we don't want them to have any effects related to
tasking, i.e. we don't want them to be potentially blocking or call
protected routines (which might violate checks for the ceiling-priority
protocol).
The cleanest way to enforce this is to require all potentially blocking
operation to reference Ada.Task_Identification.Tasking_State, just like
the delay statements do.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-12-12 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* libgnarl/a-dispat.ads (Yield): Update Global contract.--- gcc/ada/libgnarl/a-dispat.ads
+++ gcc/ada/libgnarl/a-dispat.ads
@@ -13,11 +13,13 @@
-- --
------------------------------------------------------------------------------
+with Ada.Task_Identification;
+
package Ada.Dispatching is
pragma Preelaborate (Dispatching);
procedure Yield with
- Global => null;
+ Global => (In_Out => Ada.Task_Identification.Tasking_State);
Dispatching_Policy_Error : exception;
end Ada.Dispatching;
