sem_prag.ads (Build_Classwide_Expression): new procedure to build the expression for an inherited classwide condition...

2016-06-22  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.ads (Build_Classwide_Expression): new procedure to
	build the expression for an inherited classwide condition, and
	to validate such expressions when they apply to an inherited
	operation that is not overridden.
	* sem_prag.adb (Primitives_Mapping): new data structure to
	handle the mapping between operations of a root type and the
	corresponding overriding operations of a type extension. Used
	to construct the expression for an inherited classwide condition.
	(Update_Primitives_Mapping): add to Primitives_Mapping the links
	between primitive operations of a root type and those of a given
	type extension.
	(Build_Pragma_Check_Equivalent): use Primitives_Mapping.
	* sem_ch6.adb (New_Overloaded_Entity): Remove call to
	Collect_Iherited_Class_Wide_Conditions in GNATprove_Mode. This
	needs to be done at freeze point of the type.
	* freeze.adb (Check_Inherited_Conditions): new procedure to
	verify the legality of inherited classwide conditions. In normal
	compilation mode the procedure determines whether an inherited
	operation needs a wrapper to handle an inherited condition that
	differs from the condition of the root type.  In SPARK mode
	the routine invokes Collect_Inherited_Class_Wide_Conditions to
	produce the SPARK version of these inherited conditions.
	(Freeze_Record_Type): For a type extension, call
	Check_Inherited_Conditions.

From-SVN: r237698

1 files changed, 11 insertions, 0 deletions

diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index d860708..064534f 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -244,6 +244,17 @@ package Sem_Prag is
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
    --  Perform preanalysis of pragma Test_Case
 
+   procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id);
+   --  Build the expression for an inherited classwide condition. Prag is
+   --  the pragma constructed from the corresponding aspect of the parent
+   --  subprogram, and Subp is the overridding operation.
+   --  The routine is also called to check whether an inherited operation
+   --  that is not overridden but has inherited conditions need a wrapper,
+   --  because the inherited condition includes calls to other primitives that
+   --  have been overridden. In that case the first argument is the expression
+   --  of the original classwide aspect. In SPARK_Mode, such operation which
+   --  are just inherited but have modified pre/postconditions are illegal.
+
    function Build_Pragma_Check_Equivalent
      (Prag           : Node_Id;
       Subp_Id        : Entity_Id := Empty;