[multiple changes]

2015-10-20  Yannick Moy  <moy@adacore.com>

	* a-sytaco.ads (Ada.Synchronous_Task_Control): Package
	now withs System.Task_Identification. The visible part
	of the spec has SPARK_Mode. The private part has pragma
	SPARK_Mode (Off).
	(Set_True): Added Global and Depends aspects
	(Set_False): Added Global and Depends aspects (Current_State):
	Added Volatile_Function aspect and added external state
	Ada.Task_Identification.Tasking_State as a Global input.
	(Suspend_Until_True): Added Global and Depends aspects
	* a-sytaco.adb (Ada.Synchronous_Task_Control):
	Package body has SPARK_Mode => Off
	* a-extiin.ads (Ada.Execution_Time.Interrupts):
	Package now withs Ada.Real_Time and has SPARK_Mode.
	(Clock): Added Volatile_Function aspect and added external state
	Ada.Real_Time.Clock_Time as a Global input.
	* a-reatim.ads (Ada.Real_Time): The visible part of the spec has
	SPARK_Mode. The private part has pragma SPARK_Mode (Off). The package
	declares external state Clock_Time with properties Async_Readers and
	Async_Writers.
	(Clock): Added Volatile_Function aspect and
	added external state Clock_Time as a Global input.
	* a-reatim.adb (Ada.Real_Time): Package body has SPARK_Mode => Off
	* a-exetim-default.ads, a-exetim-mingw.ads (Ada.Execution_Time):
	The visible part of the spec has SPARK_Mode. The private part
	has pragma SPARK_Mode (Off).
	(Clock): Added Volatile_Function
	aspect and added external state Clock_Time as a Global input.
	(Clock_For_Interrupts): Added Volatile_Function aspect and added
	external state Ada.Real_Time.Clock_Time as a Global input.
	* a-exetim-mingw.adb (Ada.Execution_Time): Package body has
	SPARK_Mode => Off
	* a-interr.ads (Ada.Interrupts): Package now
	withs Ada.Task_Identification (Is_Reserved): Added
	SPARK_Mode, Volatile_Function and external state
	Ada.Task_Identification.Tasking_State as a Global input.
	(Is_Attached): Added SPARK_Mode, Volatile_Function and external
	state Ada.Task_Identification.Tasking_State as a Global input.
	(Attach_Handler): Added SPARK_Mode => Off (Exchange_Handler):
	Added SPARK_Mode => Off (Detach_Handler): Added SPARK_Mode
	and external state Ada.Task_Identification.Tasking_State as a
	Global In_Out.	(Reference): Added SPARK_Mode => Off
	* a-disedf.ads (Get_Deadline): Added SPARK_Mode, Volatile_Function
	and external state Ada.Task_Identification.Tasking_State as a
	Global input.
	* a-taside.ads (Ada.Task_Identification): The visible part of
	the spec has SPARK_Mode.  The private part has pragma SPARK_Mode
	(Off). The package declares external state Tasking_State with
	properties Async_Readers and Async_Writers.
	(Current_Task): Added
	Volatile_Function aspect and added external state Tasking_State
	as a Global input.
	(Environment_Task): Added SPARK_Mode => Off
	(Is_Terminated): Added Volatile_Function aspect and added external
	state Tasking_State as a Global input.	(Is_Callable): Added
	Volatile_Function aspect and added external state Tasking_State as
	a Global input.
	(Activation_Is_Complete): Added Volatile_Function
	aspect and added external state Tasking_State as a Global input.
	* a-taside.adb (Ada.Task_Identification): Package body has
	SPARK_Mode => Off.

2015-10-20  Ed Schonberg  <schonberg@adacore.com>

	* atree.ads, atree.adb: Enable List38 and List39 on entities.
	* einfo.ads, einfo.adb (Class_Wide_Preconds) new attribute defined
	on subprograms. Holds the list of class-wide precondition
	functions inherited from ancestors. Each such function is an
	instantiation of the generic function generated from an explicit
	aspect specification for a class-wide precondition. A type is
	an ancestor of itself, and therefore a root type has such an
	instance on its own list.
	(Class_Wide_Postconds): ditto for postconditions.

2015-10-20  Vincent Celier  <celier@adacore.com>

	* prj-attr.adb: Add packages Prove and GnatTest.

2015-10-20  Steve Baird  <baird@adacore.com>

	* a-conhel.adb: Add an Annotate pragma to help suppress CodePeer's
	analysis of internals of container generic instances. This pragma
	has no other effect.
	* a-conhel.adb (Generic_Implementation) Add "pragma Annotate
	(CodePeer, Skip_Analysis);".

From-SVN: r229070

21 files changed, 316 insertions, 38 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ea3417e..e983e4c 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,90 @@
+2015-10-20  Yannick Moy  <moy@adacore.com>
+
+	* a-sytaco.ads (Ada.Synchronous_Task_Control): Package
+	now withs System.Task_Identification. The visible part
+	of the spec has SPARK_Mode. The private part has pragma
+	SPARK_Mode (Off).
+	(Set_True): Added Global and Depends aspects
+	(Set_False): Added Global and Depends aspects (Current_State):
+	Added Volatile_Function aspect and added external state
+	Ada.Task_Identification.Tasking_State as a Global input.
+	(Suspend_Until_True): Added Global and Depends aspects
+	* a-sytaco.adb (Ada.Synchronous_Task_Control):
+	Package body has SPARK_Mode => Off
+	* a-extiin.ads (Ada.Execution_Time.Interrupts):
+	Package now withs Ada.Real_Time and has SPARK_Mode.
+	(Clock): Added Volatile_Function aspect and added external state
+	Ada.Real_Time.Clock_Time as a Global input.
+	* a-reatim.ads (Ada.Real_Time): The visible part of the spec has
+	SPARK_Mode. The private part has pragma SPARK_Mode (Off). The package
+	declares external state Clock_Time with properties Async_Readers and
+	Async_Writers.
+	(Clock): Added Volatile_Function aspect and
+	added external state Clock_Time as a Global input.
+	* a-reatim.adb (Ada.Real_Time): Package body has SPARK_Mode => Off
+	* a-exetim-default.ads, a-exetim-mingw.ads (Ada.Execution_Time):
+	The visible part of the spec has SPARK_Mode. The private part
+	has pragma SPARK_Mode (Off).
+	(Clock): Added Volatile_Function
+	aspect and added external state Clock_Time as a Global input.
+	(Clock_For_Interrupts): Added Volatile_Function aspect and added
+	external state Ada.Real_Time.Clock_Time as a Global input.
+	* a-exetim-mingw.adb (Ada.Execution_Time): Package body has
+	SPARK_Mode => Off
+	* a-interr.ads (Ada.Interrupts): Package now
+	withs Ada.Task_Identification (Is_Reserved): Added
+	SPARK_Mode, Volatile_Function and external state
+	Ada.Task_Identification.Tasking_State as a Global input.
+	(Is_Attached): Added SPARK_Mode, Volatile_Function and external
+	state Ada.Task_Identification.Tasking_State as a Global input.
+	(Attach_Handler): Added SPARK_Mode => Off (Exchange_Handler):
+	Added SPARK_Mode => Off (Detach_Handler): Added SPARK_Mode
+	and external state Ada.Task_Identification.Tasking_State as a
+	Global In_Out.	(Reference): Added SPARK_Mode => Off
+	* a-disedf.ads (Get_Deadline): Added SPARK_Mode, Volatile_Function
+	and external state Ada.Task_Identification.Tasking_State as a
+	Global input.
+	* a-taside.ads (Ada.Task_Identification): The visible part of
+	the spec has SPARK_Mode.  The private part has pragma SPARK_Mode
+	(Off). The package declares external state Tasking_State with
+	properties Async_Readers and Async_Writers.
+	(Current_Task): Added
+	Volatile_Function aspect and added external state Tasking_State
+	as a Global input.
+	(Environment_Task): Added SPARK_Mode => Off
+	(Is_Terminated): Added Volatile_Function aspect and added external
+	state Tasking_State as a Global input.	(Is_Callable): Added
+	Volatile_Function aspect and added external state Tasking_State as
+	a Global input.
+	(Activation_Is_Complete): Added Volatile_Function
+	aspect and added external state Tasking_State as a Global input.
+	* a-taside.adb (Ada.Task_Identification): Package body has
+	SPARK_Mode => Off.
+
+2015-10-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* atree.ads, atree.adb: Enable List38 and List39 on entities.
+	* einfo.ads, einfo.adb (Class_Wide_Preconds) new attribute defined
+	on subprograms. Holds the list of class-wide precondition
+	functions inherited from ancestors. Each such function is an
+	instantiation of the generic function generated from an explicit
+	aspect specification for a class-wide precondition. A type is
+	an ancestor of itself, and therefore a root type has such an
+	instance on its own list.
+	(Class_Wide_Postconds): ditto for postconditions.
+
+2015-10-20  Vincent Celier  <celier@adacore.com>
+
+	* prj-attr.adb: Add packages Prove and GnatTest.
+
+2015-10-20  Steve Baird  <baird@adacore.com>
+
+	* a-conhel.adb: Add an Annotate pragma to help suppress CodePeer's
+	analysis of internals of container generic instances. This pragma
+	has no other effect.
+	* a-conhel.adb (Generic_Implementation) Add "pragma Annotate
+	(CodePeer, Skip_Analysis);".
+
 2015-10-20  Steve Baird  <baird@adacore.com>
 
 	* pprint.adb: Code clean up.
diff --git a/gcc/ada/a-conhel.adb b/gcc/ada/a-conhel.adb
index f433250..de66a50 100644
--- a/gcc/ada/a-conhel.adb
+++ b/gcc/ada/a-conhel.adb
@@ -29,6 +29,8 @@ package body Ada.Containers.Helpers is
 
    package body Generic_Implementation is
 
+      pragma Annotate (CodePeer, Skip_Analysis);
+
       use type SAC.Atomic_Unsigned;
 
       ------------
diff --git a/gcc/ada/a-disedf.ads b/gcc/ada/a-disedf.ads
index f1a5f3c..4b28a6d 100644
--- a/gcc/ada/a-disedf.ads
+++ b/gcc/ada/a-disedf.ads
@@ -45,6 +45,10 @@ package Ada.Dispatching.EDF is
    function Get_Deadline
       (T : Ada.Task_Identification.Task_Id :=
              Ada.Task_Identification.Current_Task)
-       return Deadline;
+       return Deadline
+   with
+     SPARK_Mode,
+     Volatile_Function,
+     Global => Ada.Task_Identification.Tasking_State;
 
 end Ada.Dispatching.EDF;
diff --git a/gcc/ada/a-exetim-default.ads b/gcc/ada/a-exetim-default.ads
index 56429af..c1ccda5 100644
--- a/gcc/ada/a-exetim-default.ads
+++ b/gcc/ada/a-exetim-default.ads
@@ -36,7 +36,9 @@
 with Ada.Task_Identification;
 with Ada.Real_Time;
 
-package Ada.Execution_Time is
+package Ada.Execution_Time with
+  SPARK_Mode
+is
 
    type CPU_Time is private;
 
@@ -48,7 +50,10 @@ package Ada.Execution_Time is
    function Clock
      (T : Ada.Task_Identification.Task_Id :=
         Ada.Task_Identification.Current_Task)
-      return CPU_Time;
+      return CPU_Time
+   with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
    function "+"
      (Left  : CPU_Time;
@@ -84,9 +89,12 @@ package Ada.Execution_Time is
    Interrupt_Clocks_Supported          : constant Boolean := False;
    Separate_Interrupt_Clocks_Supported : constant Boolean := False;
 
-   function Clock_For_Interrupts return CPU_Time;
+   function Clock_For_Interrupts return CPU_Time with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
 private
+   pragma SPARK_Mode (Off);
 
    type CPU_Time is new Ada.Real_Time.Time;
 
diff --git a/gcc/ada/a-exetim-mingw.adb b/gcc/ada/a-exetim-mingw.adb
index b6919f2..44f4ac3 100644
--- a/gcc/ada/a-exetim-mingw.adb
+++ b/gcc/ada/a-exetim-mingw.adb
@@ -39,7 +39,9 @@ with System.Task_Primitives.Operations; use System.Task_Primitives.Operations;
 with System.Tasking;                    use System.Tasking;
 with System.Win32;                      use System.Win32;
 
-package body Ada.Execution_Time is
+package body Ada.Execution_Time with
+  SPARK_Mode => Off
+is
 
    ---------
    -- "+" --
diff --git a/gcc/ada/a-exetim-mingw.ads b/gcc/ada/a-exetim-mingw.ads
index bc458f6..8dcd320 100644
--- a/gcc/ada/a-exetim-mingw.ads
+++ b/gcc/ada/a-exetim-mingw.ads
@@ -38,7 +38,9 @@
 with Ada.Task_Identification;
 with Ada.Real_Time;
 
-package Ada.Execution_Time is
+package Ada.Execution_Time with
+  SPARK_Mode
+is
 
    type CPU_Time is private;
 
@@ -50,7 +52,10 @@ package Ada.Execution_Time is
    function Clock
      (T : Ada.Task_Identification.Task_Id :=
         Ada.Task_Identification.Current_Task)
-      return CPU_Time;
+      return CPU_Time
+   with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
    function "+"
      (Left  : CPU_Time;
@@ -86,9 +91,12 @@ package Ada.Execution_Time is
    Interrupt_Clocks_Supported          : constant Boolean := False;
    Separate_Interrupt_Clocks_Supported : constant Boolean := False;
 
-   function Clock_For_Interrupts return CPU_Time;
+   function Clock_For_Interrupts return CPU_Time with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
 private
+   pragma SPARK_Mode (Off);
 
    type CPU_Time is new Ada.Real_Time.Time;
 
diff --git a/gcc/ada/a-exetim.ads b/gcc/ada/a-exetim.ads
index 2b07250..54a9b41 100644
--- a/gcc/ada/a-exetim.ads
+++ b/gcc/ada/a-exetim.ads
@@ -24,7 +24,9 @@
 with Ada.Task_Identification;
 with Ada.Real_Time;
 
-package Ada.Execution_Time is
+package Ada.Execution_Time with
+  SPARK_Mode
+is
    pragma Preelaborate;
 
    pragma Unimplemented_Unit;
@@ -39,7 +41,10 @@ package Ada.Execution_Time is
    function Clock
      (T : Ada.Task_Identification.Task_Id :=
         Ada.Task_Identification.Current_Task)
-      return CPU_Time;
+      return CPU_Time
+   with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
    function "+"
      (Left  : CPU_Time;
@@ -75,9 +80,12 @@ package Ada.Execution_Time is
    Interrupt_Clocks_Supported          : constant Boolean := False;
    Separate_Interrupt_Clocks_Supported : constant Boolean := False;
 
-   function Clock_For_Interrupts return CPU_Time;
+   function Clock_For_Interrupts return CPU_Time with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
 private
+   pragma SPARK_Mode (Off);
 
    type CPU_Time is new Ada.Real_Time.Time;
 
diff --git a/gcc/ada/a-extiin.ads b/gcc/ada/a-extiin.ads
index 0105a4c..8e8563d 100644
--- a/gcc/ada/a-extiin.ads
+++ b/gcc/ada/a-extiin.ads
@@ -14,12 +14,18 @@
 ------------------------------------------------------------------------------
 
 with Ada.Interrupts;
+with Ada.Real_Time;
 
-package Ada.Execution_Time.Interrupts is
+package Ada.Execution_Time.Interrupts with
+  SPARK_Mode
+is
 
    pragma Unimplemented_Unit;
 
-   function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time;
+   function Clock (Interrupt : Ada.Interrupts.Interrupt_ID) return CPU_Time
+   with
+     Volatile_Function,
+     Global => Ada.Real_Time.Clock_Time;
 
    function Supported (Interrupt : Ada.Interrupts.Interrupt_ID) return Boolean;
 
diff --git a/gcc/ada/a-interr.ads b/gcc/ada/a-interr.ads
index fede3bd..09a5868 100644
--- a/gcc/ada/a-interr.ads
+++ b/gcc/ada/a-interr.ads
@@ -34,6 +34,7 @@
 ------------------------------------------------------------------------------
 
 with System.Interrupts;
+with Ada.Task_Identification;
 
 package Ada.Interrupts is
 
@@ -41,25 +42,40 @@ package Ada.Interrupts is
 
    type Parameterless_Handler is access protected procedure;
 
-   function Is_Reserved (Interrupt : Interrupt_ID) return Boolean;
+   function Is_Reserved (Interrupt : Interrupt_ID) return Boolean with
+     SPARK_Mode,
+     Volatile_Function,
+     Global => Ada.Task_Identification.Tasking_State;
 
-   function Is_Attached (Interrupt : Interrupt_ID) return Boolean;
+   function Is_Attached (Interrupt : Interrupt_ID) return Boolean with
+     SPARK_Mode,
+     Volatile_Function,
+     Global => Ada.Task_Identification.Tasking_State;
 
    function Current_Handler
-     (Interrupt : Interrupt_ID) return Parameterless_Handler;
+     (Interrupt : Interrupt_ID) return Parameterless_Handler
+   with
+     SPARK_Mode => Off;
 
    procedure Attach_Handler
      (New_Handler : Parameterless_Handler;
-      Interrupt   : Interrupt_ID);
+      Interrupt   : Interrupt_ID)
+   with
+     SPARK_Mode => Off;
 
    procedure Exchange_Handler
      (Old_Handler : out Parameterless_Handler;
       New_Handler : Parameterless_Handler;
-      Interrupt   : Interrupt_ID);
+      Interrupt   : Interrupt_ID)
+   with
+     SPARK_Mode => Off;
 
-   procedure Detach_Handler (Interrupt : Interrupt_ID);
+   procedure Detach_Handler (Interrupt : Interrupt_ID) with
+     SPARK_Mode,
+     Global => (In_Out => Ada.Task_Identification.Tasking_State);
 
-   function Reference (Interrupt : Interrupt_ID) return System.Address;
+   function Reference (Interrupt : Interrupt_ID) return System.Address with
+     SPARK_Mode => Off;
 
 private
    pragma Inline (Is_Reserved);
diff --git a/gcc/ada/a-reatim.adb b/gcc/ada/a-reatim.adb
index 1b4d4d8..4bac97b 100644
--- a/gcc/ada/a-reatim.adb
+++ b/gcc/ada/a-reatim.adb
@@ -32,7 +32,9 @@
 
 with System.Tasking;
 
-package body Ada.Real_Time is
+package body Ada.Real_Time with
+  SPARK_Mode => Off
+is
 
    ---------
    -- "*" --
diff --git a/gcc/ada/a-reatim.ads b/gcc/ada/a-reatim.ads
index 7abbeb8..ff73167 100644
--- a/gcc/ada/a-reatim.ads
+++ b/gcc/ada/a-reatim.ads
@@ -36,7 +36,11 @@
 with System.Task_Primitives.Operations;
 pragma Elaborate_All (System.Task_Primitives.Operations);
 
-package Ada.Real_Time is
+package Ada.Real_Time with
+  SPARK_Mode,
+  Abstract_State => (Clock_Time with External => (Async_Readers,
+                                                  Async_Writers))
+is
 
    pragma Compile_Time_Error
      (Duration'Size /= 64,
@@ -54,7 +58,9 @@ package Ada.Real_Time is
    Time_Span_Unit  : constant Time_Span;
 
    Tick : constant Time_Span;
-   function Clock return Time;
+   function Clock return Time with
+     Volatile_Function,
+     Global => Clock_Time;
 
    function "+"  (Left : Time;      Right : Time_Span) return Time;
    function "+"  (Left : Time_Span; Right : Time)      return Time;
@@ -107,6 +113,8 @@ package Ada.Real_Time is
    function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time;
 
 private
+   pragma SPARK_Mode (Off);
+
    --  Time and Time_Span are represented in 64-bit Duration value in
    --  nanoseconds. For example, 1 second and 1 nanosecond is represented
    --  as the stored integer 1_000_000_001. This is for the 64-bit Duration
diff --git a/gcc/ada/a-sytaco.adb b/gcc/ada/a-sytaco.adb
index 62bced2..ab7c9ad 100644
--- a/gcc/ada/a-sytaco.adb
+++ b/gcc/ada/a-sytaco.adb
@@ -34,7 +34,9 @@ with Ada.Exceptions;
 with System.Tasking;
 with System.Task_Primitives.Operations;
 
-package body Ada.Synchronous_Task_Control is
+package body Ada.Synchronous_Task_Control with
+  SPARK_Mode => Off
+is
 
    ----------------
    -- Initialize --
diff --git a/gcc/ada/a-sytaco.ads b/gcc/ada/a-sytaco.ads
index a6bd84e..bf1ab87 100644
--- a/gcc/ada/a-sytaco.ads
+++ b/gcc/ada/a-sytaco.ads
@@ -36,22 +36,37 @@
 with System.Task_Primitives;
 
 with Ada.Finalization;
+with Ada.Task_Identification;
 
-package Ada.Synchronous_Task_Control is
+package Ada.Synchronous_Task_Control with
+  SPARK_Mode
+is
    pragma Preelaborate;
    --  In accordance with Ada 2005 AI-362
 
    type Suspension_Object is limited private;
 
-   procedure Set_True (S : in out Suspension_Object);
+   procedure Set_True (S : in out Suspension_Object) with
+     Global  => null,
+     Depends => (S    => null,
+                 null => S);
 
-   procedure Set_False (S : in out Suspension_Object);
+   procedure Set_False (S : in out Suspension_Object) with
+     Global  => null,
+     Depends => (S    => null,
+                 null => S);
 
-   function Current_State (S : Suspension_Object) return Boolean;
+   function Current_State (S : Suspension_Object) return Boolean with
+     Volatile_Function,
+     Global => Ada.Task_Identification.Tasking_State;
 
-   procedure Suspend_Until_True (S : in out Suspension_Object);
+   procedure Suspend_Until_True (S : in out Suspension_Object) with
+     Global  => null,
+     Depends => (S    => null,
+                 null => S);
 
 private
+   pragma SPARK_Mode (Off);
 
    procedure Initialize (S : in out Suspension_Object);
    --  Initialization for Suspension_Object
diff --git a/gcc/ada/a-taside.adb b/gcc/ada/a-taside.adb
index ac4473e..b916c76 100644
--- a/gcc/ada/a-taside.adb
+++ b/gcc/ada/a-taside.adb
@@ -45,7 +45,9 @@ with System.Tasking.Utilities;
 
 pragma Warnings (On);
 
-package body Ada.Task_Identification is
+package body Ada.Task_Identification with
+  SPARK_Mode => Off
+is
 
    use System.Parameters;
 
diff --git a/gcc/ada/a-taside.ads b/gcc/ada/a-taside.ads
index d736b03..3a3df7c 100644
--- a/gcc/ada/a-taside.ads
+++ b/gcc/ada/a-taside.ads
@@ -36,7 +36,11 @@
 with System;
 with System.Tasking;
 
-package Ada.Task_Identification is
+package Ada.Task_Identification with
+  SPARK_Mode,
+  Abstract_State => (Tasking_State with External => (Async_Readers,
+                                                     Async_Writers))
+is
    pragma Preelaborate;
    --  In accordance with Ada 2005 AI-362
 
@@ -50,25 +54,35 @@ package Ada.Task_Identification is
 
    function Image (T : Task_Id) return String;
 
-   function Current_Task return Task_Id;
+   function Current_Task return Task_Id with
+     Volatile_Function,
+     Global => Tasking_State;
    pragma Inline (Current_Task);
 
-   function Environment_Task return Task_Id;
+   function Environment_Task return Task_Id with
+     SPARK_Mode => Off;
    pragma Inline (Environment_Task);
 
    procedure Abort_Task (T : Task_Id);
    pragma Inline (Abort_Task);
    --  Note: parameter is mode IN, not IN OUT, per AI-00101
 
-   function Is_Terminated (T : Task_Id) return Boolean;
+   function Is_Terminated (T : Task_Id) return Boolean with
+     Volatile_Function,
+     Global => Tasking_State;
    pragma Inline (Is_Terminated);
 
-   function Is_Callable (T : Task_Id) return Boolean;
+   function Is_Callable (T : Task_Id) return Boolean with
+     Volatile_Function,
+     Global => Tasking_State;
    pragma Inline (Is_Callable);
 
-   function Activation_Is_Complete (T : Task_Id) return Boolean;
+   function Activation_Is_Complete (T : Task_Id) return Boolean with
+     Volatile_Function,
+     Global => Tasking_State;
 
 private
+   pragma SPARK_Mode (Off);
 
    type Task_Id is new System.Tasking.Task_Id;
 
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 870d7ff..973bdde 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -828,6 +828,7 @@ package body Atree is
          end case;
 
          Set_Chars (New_Ent, Chars (E));
+         --  Set_Comes_From_Source (New_Ent, Comes_From_Source (E));
          return New_Ent;
       end Copy_Entity;
 
@@ -2905,6 +2906,16 @@ package body Atree is
          return List_Id (Nodes.Table (N + 4).Field7);
       end List25;
 
+      function List38 (N : Node_Id) return List_Id is
+      begin
+         return List_Id (Nodes.Table (N + 6).Field8);
+      end List38;
+
+      function List39 (N : Node_Id) return List_Id is
+      begin
+         return List_Id (Nodes.Table (N + 6).Field9);
+      end List39;
+
       function Elist1 (N : Node_Id) return Elist_Id is
          pragma Assert (N <= Nodes.Last);
          Value : constant Union_Id := Nodes.Table (N).Field1;
@@ -5758,6 +5769,18 @@ package body Atree is
          Nodes.Table (N + 4).Field7 := Union_Id (Val);
       end Set_List25;
 
+      procedure Set_List38 (N : Node_Id; Val : List_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 6).Field8 := Union_Id (Val);
+      end Set_List38;
+
+      procedure Set_List39 (N : Node_Id; Val : List_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 6).Field9 := Union_Id (Val);
+      end Set_List39;
+
       procedure Set_Elist1 (N : Node_Id; Val : Elist_Id) is
       begin
          Nodes.Table (N).Field1 := Union_Id (Val);
diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads
index 155cde3..0b4d245 100644
--- a/gcc/ada/atree.ads
+++ b/gcc/ada/atree.ads
@@ -1355,6 +1355,12 @@ package Atree is
       function List25 (N : Node_Id) return List_Id;
       pragma Inline (List25);
 
+      function List38 (N : Node_Id) return List_Id;
+      pragma Inline (List38);
+
+      function List39 (N : Node_Id) return List_Id;
+      pragma Inline (List39);
+
       function Elist1 (N : Node_Id) return Elist_Id;
       pragma Inline (Elist1);
 
@@ -2706,6 +2712,12 @@ package Atree is
       procedure Set_List25 (N : Node_Id; Val : List_Id);
       pragma Inline (Set_List25);
 
+      procedure Set_List38 (N : Node_Id; Val : List_Id);
+      pragma Inline (Set_List38);
+
+      procedure Set_List39 (N : Node_Id; Val : List_Id);
+      pragma Inline (Set_List39);
+
       procedure Set_Elist1 (N : Node_Id; Val : Elist_Id);
       pragma Inline (Set_Elist1);
 
diff --git a/gcc/ada/atree.h b/gcc/ada/atree.h
index e296b8a..adb636a 100644
--- a/gcc/ada/atree.h
+++ b/gcc/ada/atree.h
@@ -505,6 +505,8 @@ extern Node_Id Current_Error_Node;
 #define List10(N)     Field10 (N)
 #define List14(N)     Field14 (N)
 #define List25(N)     Field25 (N)
+#define List38(N)     Field38 (N)
+#define List39(N)     Field39 (N)
 
 #define Elist1(N)     Field1  (N)
 #define Elist2(N)     Field2  (N)
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index c6a9998..dff2a2b 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -267,8 +267,10 @@ package body Einfo is
 
    --    Anonymous_Master                Node36
 
-   --    (unused)                        Node38
-   --    (unused)                        Node39
+   --    (Class_Wide_Preconds)           List38
+
+   --    (Class_Wide_Postconds)          List39
+
    --    (unused)                        Node40
    --    (unused)                        Node41
 
@@ -842,6 +844,18 @@ package body Einfo is
       return Flag31 (Id);
    end Checks_May_Be_Suppressed;
 
+   function Class_Wide_Postconds (Id : E) return S is
+   begin
+      pragma Assert (Is_Subprogram (Id));
+      return List39 (Id);
+   end Class_Wide_Postconds;
+
+   function Class_Wide_Preconds (Id : E) return S is
+   begin
+      pragma Assert (Is_Subprogram (Id));
+      return List38 (Id);
+   end Class_Wide_Preconds;
+
    function Class_Wide_Type (Id : E) return E is
    begin
       pragma Assert (Is_Type (Id));
@@ -3732,6 +3746,18 @@ package body Einfo is
       Set_Flag31 (Id, V);
    end Set_Checks_May_Be_Suppressed;
 
+   procedure Set_Class_Wide_Preconds (Id : E; V : S) is
+   begin
+      pragma Assert (Is_Subprogram (Id));
+      Set_List38 (Id, V);
+   end Set_Class_Wide_Preconds;
+
+   procedure Set_Class_Wide_Postconds (Id : E; V : S) is
+   begin
+      pragma Assert (Is_Subprogram (Id));
+      Set_List39 (Id, V);
+   end Set_Class_Wide_Postconds;
+
    procedure Set_Class_Wide_Type (Id : E; V : E) is
    begin
       pragma Assert (Is_Type (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 58d3ba8..bea9dac 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -607,6 +607,17 @@ package Einfo is
 --       tables must be consulted to determine if there actually is an active
 --       Suppress or Unsuppress pragma that applies to the entity.
 
+--    Class_Wide_Preconds (List38)
+--       Defined on subprograms. Holds the list of class-wide precondition
+--       functions inherited from ancestors. Each such function is an
+--       instantiation of the generic function generated from an explicit
+--       aspect specification for a class-wide precondition. A type is an
+--       ancestor of itself, and therefore a root type has such an instance
+--       on its own list.
+
+--    Class_Wide_Postconds (List39)
+--       Ditto for class-wide postconditions.
+
 --    Class_Wide_Type (Node9)
 --       Defined in all type entities. For a tagged type or subtype, returns
 --       the corresponding implicitly declared class-wide type. For a
@@ -5844,6 +5855,8 @@ package Einfo is
    --    Contract                            (Node34)
    --    Import_Pragma                       (Node35)   (non-generic case only)
    --    Anonymous_Master                    (Node36)   (non-generic case only)
+   --    Class_Wide_Preconds                 (List38)
+   --    Class_Wide_Postconds                (List39)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Contains_Ignored_Ghost_Code         (Flag279)
    --    Default_Expressions_Processed       (Flag108)
@@ -6151,6 +6164,8 @@ package Einfo is
    --    Contract                            (Node34)
    --    Import_Pragma                       (Node35)   (non-generic case only)
    --    Anonymous_Master                    (Node36)   (non-generic case only)
+   --    Class_Wide_Preconds                 (List38)
+   --    Class_Wide_Postconds                (List39)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Contains_Ignored_Ghost_Code         (Flag279)
    --    Delay_Cleanups                      (Flag114)
@@ -6675,6 +6690,8 @@ package Einfo is
    function Can_Never_Be_Null                   (Id : E) return B;
    function Can_Use_Internal_Rep                (Id : E) return B;
    function Checks_May_Be_Suppressed            (Id : E) return B;
+   function Class_Wide_Postconds                (Id : E) return S;
+   function Class_Wide_Preconds                 (Id : E) return S;
    function Class_Wide_Type                     (Id : E) return E;
    function Cloned_Subtype                      (Id : E) return E;
    function Component_Alignment                 (Id : E) return C;
@@ -7334,6 +7351,8 @@ package Einfo is
    procedure Set_Can_Never_Be_Null               (Id : E; V : B := True);
    procedure Set_Can_Use_Internal_Rep            (Id : E; V : B := True);
    procedure Set_Checks_May_Be_Suppressed        (Id : E; V : B := True);
+   procedure Set_Class_Wide_Postconds            (Id : E; V : S);
+   procedure Set_Class_Wide_Preconds             (Id : E; V : S);
    procedure Set_Class_Wide_Type                 (Id : E; V : E);
    procedure Set_Cloned_Subtype                  (Id : E; V : E);
    procedure Set_Component_Alignment             (Id : E; V : C);
@@ -8111,6 +8130,8 @@ package Einfo is
    pragma Inline (Can_Never_Be_Null);
    pragma Inline (Can_Use_Internal_Rep);
    pragma Inline (Checks_May_Be_Suppressed);
+   pragma Inline (Class_Wide_Preconds);
+   pragma Inline (Class_Wide_Postconds);
    pragma Inline (Class_Wide_Type);
    pragma Inline (Cloned_Subtype);
    pragma Inline (Component_Bit_Offset);
@@ -8615,6 +8636,8 @@ package Einfo is
    pragma Inline (Set_Can_Never_Be_Null);
    pragma Inline (Set_Can_Use_Internal_Rep);
    pragma Inline (Set_Checks_May_Be_Suppressed);
+   pragma Inline (Set_Class_Wide_Postconds);
+   pragma Inline (Set_Class_Wide_Preconds);
    pragma Inline (Set_Class_Wide_Type);
    pragma Inline (Set_Cloned_Subtype);
    pragma Inline (Set_Component_Bit_Offset);
diff --git a/gcc/ada/prj-attr.adb b/gcc/ada/prj-attr.adb
index 66de7c7..791fe21 100644
--- a/gcc/ada/prj-attr.adb
+++ b/gcc/ada/prj-attr.adb
@@ -389,6 +389,14 @@ package body Prj.Attr is
    "LVswitches#" &
    "LVexcluded_source_files#" &
 
+   --  package Prove
+
+   "Pprove#" &
+
+   --  package GnatTest
+
+   "Pgnattest#" &
+
    "#";
 
    Initialized : Boolean := False;