sem_prag.ads (Build_Classwide_Expression): new procedure to build the expression…

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

gcc/ada/ChangeLog

+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.
+
 2016-06-22  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_ch3.adb, sem_type.adb, sem.adb, freeze.adb, sem_util.adb,

gcc/ada/freeze.adb

@@ -127,6 +127,11 @@ package body Freeze is
    --  Attribute references to outer types are freeze points for those types;
    --  this routine generates the required freeze nodes for them.
 
+   procedure Check_Inherited_Conditions (R : Entity_Id);
+   --  For a tagged derived type, create wrappers for inherited operations
+   --  that have a classwide condition, so it can be properly rewritten if
+   --  it involves calls to other overriding primitives.
+
    procedure Check_Strict_Alignment (E : Entity_Id);
    --  E is a base type. If E is tagged or has a component that is aliased
    --  or tagged or contains something this is aliased or tagged, set
@@ -1381,6 +1386,59 @@ package body Freeze is
       end if;
    end Check_Expression_Function;
 
+   --------------------------------
+   -- Check_Inherited_Conditions --
+   --------------------------------
+
+   procedure Check_Inherited_Conditions (R : Entity_Id) is
+      Prim_Ops : constant Elist_Id := Primitive_Operations (R);
+      Op_Node  : Elmt_Id;
+      Prim     : Entity_Id;
+      Par_Prim : Entity_Id;
+      A_Pre    : Node_Id;
+      A_Post   : Node_Id;
+
+   begin
+      Op_Node := First_Elmt (Prim_Ops);
+      while Present (Op_Node) loop
+         Prim := Node (Op_Node);
+
+         --  In SPARK mode this is where we can collect the inherited
+         --  conditions, because we do not create the Check pragmas that
+         --  normally convey the the modified classwide conditions on
+         --  overriding operations.
+
+         if SPARK_Mode = On
+            and then Comes_From_Source (Prim)
+            and then Present (Overridden_Operation (Prim))
+         then
+            Collect_Inherited_Class_Wide_Conditions (Prim);
+         end if;
+
+         --  In normal mode, we examine inherited operations to check
+         --  whether they require a wrapper to handle inherited conditions
+         --  that call other primitives.
+         --  Wrapper construction TBD.
+
+         if not Comes_From_Source (Prim)
+           and then Present (Alias (Prim))
+         then
+            Par_Prim := Alias (Prim);
+            A_Pre  := Find_Aspect (Par_Prim, Aspect_Pre);
+            if Present (A_Pre) and then Class_Present (A_Pre) then
+               Build_Classwide_Expression (Expression (A_Pre), Prim);
+            end if;
+
+            A_Post := Find_Aspect (Par_Prim, Aspect_Post);
+            if Present (A_Post) and then Class_Present (A_Post) then
+               Build_Classwide_Expression (Expression (A_Post), Prim);
+            end if;
+         end if;
+
+         Next_Elmt (Op_Node);
+      end loop;
+   end Check_Inherited_Conditions;
+
    ----------------------------
    -- Check_Strict_Alignment --
    ----------------------------
@@ -1657,6 +1715,9 @@ package body Freeze is
 
                Freeze_All (First_Entity (E), After);
 
+               --  Analyze_Pending_Bodies (Visible_Declarations (E));
+               --  Analyze_Pending_Bodies (Private_Declarations (E));
+
                End_Package_Scope (E);
 
                if Is_Generic_Instance (E)
@@ -4573,6 +4634,13 @@ package body Freeze is
                end loop;
             end;
          end if;
+
+         --  For a derived tagged type, check whether inherited primitives
+         --  might require a wrapper to handle classwide conditions.
+
+         if Is_Tagged_Type (Rec) and then Is_Derived_Type (Rec) then
+            Check_Inherited_Conditions (Rec);
+         end if;
       end Freeze_Record_Type;
 
       -------------------------------

gcc/ada/sem_ch6.adb

@@ -10535,13 +10535,6 @@ package body Sem_Ch6 is
                         Set_Convention (S, Convention (E));
                         Check_Dispatching_Operation (S, E);
 
-                        --  In GNATprove_Mode, create the pragmas corresponding
-                        --  to inherited class-wide conditions.
-
-                        if GNATprove_Mode then
-                           Collect_Inherited_Class_Wide_Conditions (S);
-                        end if;
-
                      else
                         Check_Dispatching_Operation (S, Empty);
                      end if;

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;