[multiple changes]

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove
	mode, collect inherited class-wide conditions to generate the
	corresponding pragmas.
	* sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts
	* contracts.adb (Collect_Inherited_Class_Wide_Conditions): New
	procedure for overriding subprograms, used to generate the pragmas
	corresponding to an inherited class- wide pre- or postcondition.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): moved here
	from contracts.adb (Replace_Condition_Entities): Subsidiary
	Build_Pragma_Check_Equivalent, to implement the proper semantics
	of inherited class-wide conditions, as given in AI12-0113.
	(Process_Class_Wide_Condition): Removed.
	(Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas
	in contract of subprogram, to collect inherited class-wide
	conditions.
	(Build_Pragma_Check_Equivalent): Moved to sem_prag.adb

2016-04-18  Yannick Moy  <moy@adacore.com>

	* a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off.
	* a-calend.ads (Ada.Calendar): Mark package spec as
	SPARK_Mode and add synchronous external abstract state Clock_Time.

From-SVN: r235113

1 files changed, 17 insertions, 0 deletions

diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 3bc2f65..063e7df 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -244,6 +244,16 @@ package Sem_Prag is
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
    --  Perform preanalysis of pragma Test_Case
 
+   function Build_Pragma_Check_Equivalent
+     (Prag     : Node_Id;
+      Subp_Id  : Entity_Id := Empty;
+      Inher_Id : Entity_Id := Empty) return Node_Id;
+   --  Transform a [refined] pre- or postcondition denoted by Prag into an
+   --  equivalent pragma Check. When the pre- or postcondition is inherited,
+   --  the routine replaces the references of all formals of Inher_Id and
+   --  primitive operations of its controlling type by references to the
+   --  corresponding entities of Subp_Id and the descendant type.
+
    procedure Check_Applicable_Policy (N : Node_Id);
    --  N is either an N_Aspect or an N_Pragma node. There are two cases. If
    --  the name of the aspect or pragma is not one of those recognized as
@@ -301,6 +311,13 @@ package Sem_Prag is
    --  state, variable or package instantiation denoted by Item_Id requires the
    --  use of indicator/option Part_Of. If this is the case, emit an error.
 
+   procedure Collect_Inherited_Class_Wide_Conditions
+     (Subp : Entity_Id;
+      Bod  : Node_Id);
+   --  When analyzing an overriding subprogram, check whether the overridden
+   --  operations have class-wide pre/postconditions, and generate the
+   --  corresponding pragmas.
+
    procedure Collect_Subprogram_Inputs_Outputs
      (Subp_Id      : Entity_Id;
       Synthesize   : Boolean := False;