[Ada] Fix Global contract for the predefined Yield procedure

Message ID 20191212100431.GA114779@adacore.com
State New
Headers show
  • [Ada] Fix Global contract for the predefined Yield procedure
Related show

Commit Message

Pierre-Marie de Rodat Dec. 12, 2019, 10:04 a.m.
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

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  <trojanek@adacore.com>


	* 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;