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.



git-svn-id: https://gcc.gnu.org/svn/gcc/trunk@237698 138bc75d-0d04-0410-961f-82ee72b054a4

5 files changed, 434 insertions, 284 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 80d03e043b2..0a252c6ba28 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,30 @@
+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,
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 037ba2f61da..271dc90abf2 100644
--- a/gcc/ada/freeze.adb
+++ b/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;
 
       -------------------------------
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 81bffcb9b99..5865b874f38 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/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;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d17dee2aefa..7f9d74ee676 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -44,6 +44,7 @@ with Exp_Dist;  use Exp_Dist;
 with Exp_Util;  use Exp_Util;
 with Freeze;    use Freeze;
 with Ghost;     use Ghost;
+with Gnatvsn;   use Gnatvsn;
 with Lib;       use Lib;
 with Lib.Writ;  use Lib.Writ;
 with Lib.Xref;  use Lib.Xref;
@@ -88,6 +89,8 @@ with Urealp;    use Urealp;
 with Validsw;   use Validsw;
 with Warnsw;    use Warnsw;
 
+with GNAT.HTable; use GNAT.HTable;
+
 package body Sem_Prag is
 
    ----------------------------------------------
@@ -163,6 +166,40 @@ package body Sem_Prag is
      Table_Increment      => 100,
      Table_Name           => "Name_Externals");
 
+     --------------------------------------------------------
+     -- Handling of inherited classwide pre/postconditions --
+     --------------------------------------------------------
+
+     --  Following AI12-0113, the expression for a classwide condition is
+     --  transformed for a subprogram that inherits it, by replacing calls
+     --  to primitive operations of the original controlling type into the
+     --  corresponding overriding operations of the derived type. The following
+     --  hash table manages this mapping, and is expanded on demand whenever
+     --  such inherited expression needs to be constructed.
+
+     --  The mapping is also used to check whether an inherited operation has
+     --  a condition that depends on overridden operations. For such an
+     --  operation we must create a wrapper that is then treated as a normal
+     --  overriding. In SPARK mode such operations are illegal.
+
+     --  For a given root type there may be several type extensions with their
+     --  own overriding operations, so at various times a given operation of
+     --  the root will be mapped into different overridings. The root type is
+     --  also mapped into the current type extension to indicate that its
+     --  operations are mapped into the overriding operations of that current
+     --  type extension.
+
+      subtype Num_Primitives is Integer range 0 .. 510;
+      function Entity_Hash (E : Entity_Id) return Num_Primitives;
+
+      package Primitives_Mapping is new Gnat.HTable.Simple_Htable
+        (Header_Num => Num_Primitives,
+         Key        => Entity_Id,
+         Element    => Entity_Id,
+         No_element => Empty,
+         Hash       => Entity_Hash,
+         Equal      => "=");
+
    -------------------------------------
    -- Local Subprograms and Variables --
    -------------------------------------
@@ -193,6 +230,11 @@ package body Sem_Prag is
    --  Query whether a particular item appears in a mixed list of nodes and
    --  entities. It is assumed that all nodes in the list have entities.
 
+   --  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.
+
    procedure Check_Postcondition_Use_In_Inlined_Subprogram
      (Prag    : Node_Id;
       Spec_Id : Entity_Id);
@@ -289,6 +331,14 @@ package body Sem_Prag is
    pragma Volatile (Dummy);
    --  Dummy volatile integer used in bodies of ip/rv to prevent optimization
 
+   procedure Update_Primitives_Mapping
+     (Inher_Id : Entity_Id;
+      Subp_Id  : Entity_Id);
+
+   --  map primitive operations of the parent type to the corresponding
+   --  operations of the descendant. note that the descendant type may
+   --  not be frozen yet, so we cannot use the dispatch table directly.
+
    procedure ip;
    pragma No_Inline (ip);
    --  A dummy procedure called when pragma Inspection_Point is analyzed. This
@@ -17580,28 +17630,39 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
             Check_Arg_Count (0);
 
-            No_Run_Time_Mode           := True;
-            Configurable_Run_Time_Mode := True;
+            --  Remove backward compatibility if Build_Type is FSF or GPL
+            --  and generate a warning.
 
-            --  Set Duration to 32 bits if word size is 32
+            declare
+               Ignore : constant Boolean := Build_Type in FSF .. GPL;
+            begin
+               if Ignore then
+                  Error_Pragma ("pragma% is ignored, has no effect??");
+               else
+                  No_Run_Time_Mode           := True;
+                  Configurable_Run_Time_Mode := True;
 
-            if Ttypes.System_Word_Size = 32 then
-               Duration_32_Bits_On_Target := True;
-            end if;
+                  --  Set Duration to 32 bits if word size is 32
 
-            --  Set appropriate restrictions
+                  if Ttypes.System_Word_Size = 32 then
+                     Duration_32_Bits_On_Target := True;
+                  end if;
 
-            Set_Restriction (No_Finalization, N);
-            Set_Restriction (No_Exception_Handlers, N);
-            Set_Restriction (Max_Tasks, N, 0);
-            Set_Restriction (No_Tasking, N);
+                  --  Set appropriate restrictions
 
-            -----------------------
-            -- No_Tagged_Streams --
-            -----------------------
+                  Set_Restriction (No_Finalization, N);
+                  Set_Restriction (No_Exception_Handlers, N);
+                  Set_Restriction (Max_Tasks, N, 0);
+                  Set_Restriction (No_Tasking, N);
+               end if;
+            end;
 
-            --  pragma No_Tagged_Streams;
-            --  pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME);
+         -----------------------
+         -- No_Tagged_Streams --
+         -----------------------
+
+         --  pragma No_Tagged_Streams;
+         --  pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME);
 
          when Pragma_No_Tagged_Streams => No_Tagged_Strms : declare
             E    : Entity_Id;
@@ -22295,22 +22356,7 @@ package body Sem_Prag is
 
          when Pragma_Universal_Data =>
             GNAT_Pragma;
-
-            --  If this is a configuration pragma, then set the universal
-            --  addressing option, otherwise confirm that the pragma satisfies
-            --  the requirements of library unit pragma placement and leave it
-            --  to the GNAAMP back end to detect the pragma (avoids transitive
-            --  setting of the option due to withed units).
-
-            if Is_Configuration_Pragma then
-               Universal_Addressing_On_AAMP := True;
-            else
-               Check_Valid_Library_Unit_Pragma;
-            end if;
-
-            if not AAMP_On_Target then
-               Error_Pragma ("??pragma% ignored (applies only to AAMP)");
-            end if;
+            Error_Pragma ("??pragma% ignored (applies only to AAMP)");
 
          ----------------
          -- Unmodified --
@@ -26291,20 +26337,6 @@ package body Sem_Prag is
       Inher_Id       : Entity_Id := Empty;
       Keep_Pragma_Id : Boolean := False) return Node_Id
    is
-      Map : Elist_Id;
-      --  List containing the following mappings
-      --    * Formal parameters of inherited subprogram Inher_Id and subprogram
-      --    Subp_Id.
-      --
-      --    * The dispatching type of Inher_Id and the dispatching type of
-      --    Subp_Id.
-      --
-      --    * Primitives of the dispatching type of Inher_Id and primitives of
-      --    the dispatching type of Subp_Id.
-
-      function Replace_Entity (N : Node_Id) return Traverse_Result;
-      --  Replace reference to formal of inherited operation or to primitive
-      --  operation of root type, with corresponding entity for derived type.
 
       function Suppress_Reference (N : Node_Id) return Traverse_Result;
       --  Detect whether node N references a formal parameter subject to
@@ -26312,83 +26344,6 @@ package body Sem_Prag is
       --  to False to suppress the generation of a reference when analyzing
       --  N later on.
 
-      --------------------
-      -- Replace_Entity --
-      --------------------
-
-      function Replace_Entity (N : Node_Id) return Traverse_Result is
-         Elmt  : Elmt_Id;
-         New_E : Entity_Id;
-
-      begin
-         if Nkind (N) = N_Identifier
-           and then Present (Entity (N))
-           and then
-             (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
-           and then
-             (Nkind (Parent (N)) /= N_Attribute_Reference
-               or else Attribute_Name (Parent (N)) /= Name_Class)
-         then
-            --  The replacement does not apply to dispatching calls within the
-            --  condition, but only to calls whose static tag is that of the
-            --  parent type.
-
-            if Is_Subprogram (Entity (N))
-              and then Nkind (Parent (N)) = N_Function_Call
-              and then Present (Controlling_Argument (Parent (N)))
-            then
-               return OK;
-            end if;
-
-            --  Loop to find out if entity has a renaming
-
-            New_E := Empty;
-            Elmt  := First_Elmt (Map);
-            while Present (Elmt) loop
-               if Node (Elmt) = Entity (N) then
-                  New_E := Node (Next_Elmt (Elmt));
-                  exit;
-               end if;
-
-               Next_Elmt (Elmt);
-            end loop;
-
-            if Present (New_E) then
-               Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
-            end if;
-
-            --  Check that there are no calls left to abstract operations if
-            --  the current subprogram is not abstract.
-
-            if Nkind (Parent (N)) = N_Function_Call
-              and then N = Name (Parent (N))
-              and then not Is_Abstract_Subprogram (Subp_Id)
-              and then Is_Abstract_Subprogram (Entity (N))
-            then
-               Error_Msg_Sloc := Sloc (Current_Scope);
-               Error_Msg_NE
-                 ("cannot call abstract subprogram in inherited condition "
-                   & "for&#", N, Current_Scope);
-            end if;
-
-            --  Update type of function call node, which should be the same as
-            --  the function's return type.
-
-            if Is_Subprogram (Entity (N))
-              and then Nkind (Parent (N)) = N_Function_Call
-            then
-               Set_Etype (Parent (N), Etype (Entity (N)));
-            end if;
-
-         --  The whole expression will be reanalyzed
-
-         elsif Nkind (N) in N_Has_Etype then
-            Set_Analyzed (N, False);
-         end if;
-
-         return OK;
-      end Replace_Entity;
-
       ------------------------
       -- Suppress_Reference --
       ------------------------
@@ -26414,9 +26369,6 @@ package body Sem_Prag is
          return OK;
       end Suppress_Reference;
 
-      procedure Replace_Condition_Entities is
-        new Traverse_Proc (Replace_Entity);
-
       procedure Suppress_References is
         new Traverse_Proc (Suppress_Reference);
 
@@ -26433,8 +26385,6 @@ package body Sem_Prag is
    --  Start of processing for Build_Pragma_Check_Equivalent
 
    begin
-      Map := No_Elist;
-
       --  When the pre- or postcondition is inherited, map the formals of the
       --  inherited subprogram to those of the current subprogram. In addition,
       --  map primitive operations of the parent type into the corresponding
@@ -26443,161 +26393,17 @@ package body Sem_Prag is
       if Present (Inher_Id) then
          pragma Assert (Present (Subp_Id));
 
-         Map := New_Elmt_List;
+         Update_Primitives_Mapping (Inher_Id, Subp_Id);
 
-         --  Create a mapping  <inherited formal> => <subprogram formal>
+         --  Add mapping from old formals to new formals.
 
          Inher_Formal := First_Formal (Inher_Id);
          Subp_Formal  := First_Formal (Subp_Id);
          while Present (Inher_Formal) and then Present (Subp_Formal) loop
-            Append_Elmt (Inher_Formal, Map);
-            Append_Elmt (Subp_Formal,  Map);
-
+            Primitives_Mapping.Set (Inher_Formal, Subp_Formal);
             Next_Formal (Inher_Formal);
             Next_Formal (Subp_Formal);
          end loop;
-
-         --  Map primitive operations of the parent type to the corresponding
-         --  operations of the descendant. Note that the descendant type may
-         --  not be frozen yet, so we cannot use the dispatch table directly.
-
-         --  Note : the construction of the map involves a full traversal of
-         --  the list of primitive operations, as well as a scan of the
-         --  declarations in the scope of the operation. Given that class-wide
-         --  conditions are typically short expressions, it might be much more
-         --  efficient to collect the identifiers in the expression first, and
-         --  then determine the ones that have to be mapped. Optimization ???
-
-         Primitive_Mapping : declare
-            function Overridden_Ancestor (S : Entity_Id) return Entity_Id;
-            --  Given the controlling type of the overridden operation and a
-            --  primitive of the current type, find the corresponding operation
-            --  of the parent type.
-
-            -------------------------
-            -- Overridden_Ancestor --
-            -------------------------
-
-            function Overridden_Ancestor (S : Entity_Id) return Entity_Id is
-               Par : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
-               Anc : Entity_Id;
-
-            begin
-               Anc := S;
-
-               --  Locate the ancestor subprogram with the proper controlling
-               --  type.
-
-               while Present (Overridden_Operation (Anc)) loop
-                  Anc := Overridden_Operation (Anc);
-                  exit when Find_Dispatching_Type (Anc) = Par;
-               end loop;
-
-               return Anc;
-            end Overridden_Ancestor;
-
-            --  Local variables
-
-            Old_Typ  : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
-            Typ      : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
-            Decl     : Node_Id;
-            Old_Elmt : Elmt_Id;
-            Old_Prim : Entity_Id;
-            Prim     : Entity_Id;
-
-         --  Start of processing for Primitive_Mapping
-
-         begin
-            Decl := First (List_Containing (Unit_Declaration_Node (Subp_Id)));
-
-            --  Look for primitive operations of the current type that have
-            --  overridden an operation of the type related to the original
-            --  class-wide precondition. There may be several intermediate
-            --  overridings between them.
-
-            while Present (Decl) loop
-               if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
-                                  N_Subprogram_Declaration)
-               then
-                  Prim := Defining_Entity (Decl);
-
-                  if Is_Subprogram (Prim)
-                    and then Present (Overridden_Operation (Prim))
-                    and then Find_Dispatching_Type (Prim) = Typ
-                  then
-                     Old_Prim := Overridden_Ancestor (Prim);
-
-                     Append_Elmt (Old_Prim, Map);
-                     Append_Elmt (Prim,     Map);
-                  end if;
-               end if;
-
-               Next (Decl);
-            end loop;
-
-            --  Now examine inherited operations. These do not override, but
-            --  have an alias, which is the entity used in a call. In turn
-            --  that alias may be inherited or comes from source, in which
-            --  case it may override an earlier operation. We only need to
-            --  examine inherited functions, that may appear within the
-            --  inherited expression.
-
-            Prim := First_Entity (Scope (Subp_Id));
-            while Present (Prim) loop
-               if not Comes_From_Source (Prim)
-                 and then Ekind (Prim) = E_Function
-                 and then Present (Alias (Prim))
-               then
-                  Old_Prim := Alias (Prim);
-
-                  if Comes_From_Source (Old_Prim) then
-                     Old_Prim := Overridden_Ancestor (Old_Prim);
-
-                  else
-                     while Present (Alias (Old_Prim))
-                       and then Scope (Old_Prim) /= Scope (Inher_Id)
-                     loop
-                        Old_Prim := Alias (Old_Prim);
-
-                        if Comes_From_Source (Old_Prim) then
-                           Old_Prim := Overridden_Ancestor (Old_Prim);
-                           exit;
-                        end if;
-                     end loop;
-                  end if;
-
-                  Append_Elmt (Old_Prim, Map);
-                  Append_Elmt (Prim,     Map);
-               end if;
-
-               Next_Entity (Prim);
-            end loop;
-
-            --  If the parent operation is an interface operation, the
-            --  overriding indicator is not present. Instead, we get from
-            --  the interface operation the primitive of the current type
-            --  that implements it.
-
-            if Is_Interface (Old_Typ) then
-               Old_Elmt := First_Elmt (Collect_Primitive_Operations (Old_Typ));
-               while Present (Old_Elmt) loop
-                  Old_Prim := Node (Old_Elmt);
-                  Prim := Find_Primitive_Covering_Interface (Typ, Old_Prim);
-
-                  if Present (Prim) then
-                     Append_Elmt (Old_Prim, Map);
-                     Append_Elmt (Prim,     Map);
-                  end if;
-
-                  Next_Elmt (Old_Elmt);
-               end loop;
-            end if;
-
-            if Map /= No_Elist then
-               Append_Elmt (Old_Typ, Map);
-               Append_Elmt (Typ,     Map);
-            end if;
-         end Primitive_Mapping;
       end if;
 
       --  Copy the original pragma while performing substitutions (if
@@ -26605,8 +26411,8 @@ package body Sem_Prag is
 
       Check_Prag := New_Copy_Tree (Source => Prag);
 
-      if Map /= No_Elist then
-         Replace_Condition_Entities (Check_Prag);
+      if Present (Inher_Id) then
+         Build_Classwide_Expression (Check_Prag, Subp_Id);
       end if;
 
       --  Mark the pragma as being internally generated and reset the Analyzed
@@ -27029,6 +26835,100 @@ package body Sem_Prag is
       end if;
    end Check_Missing_Part_Of;
 
+   --------------------------------
+   -- Build_Classwide_Expression --
+   --------------------------------
+
+   procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id) is
+      function Replace_Entity (N : Node_Id) return Traverse_Result;
+      --  Replace reference to formal of inherited operation or to primitive
+      --  operation of root type, with corresponding entity for derived type,
+      --  when constructing the classwide condition of an overridding
+      --  subprogram.
+
+      --------------------
+      -- Replace_Entity --
+      --------------------
+
+      function Replace_Entity (N : Node_Id) return Traverse_Result is
+         New_E : Entity_Id;
+
+      begin
+         if Nkind (N) = N_Identifier
+           and then Present (Entity (N))
+           and then
+             (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
+           and then
+             (Nkind (Parent (N)) /= N_Attribute_Reference
+               or else Attribute_Name (Parent (N)) /= Name_Class)
+         then
+            --  The replacement does not apply to dispatching calls within the
+            --  condition, but only to calls whose static tag is that of the
+            --  parent type.
+
+            if Is_Subprogram (Entity (N))
+              and then Nkind (Parent (N)) = N_Function_Call
+              and then Present (Controlling_Argument (Parent (N)))
+            then
+               return OK;
+            end if;
+
+            --  Determine whether entity has a renaming
+
+            New_E := Primitives_Mapping.Get (Entity (N));
+
+            if Present (New_E) then
+               Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
+            end if;
+
+            --  Check that there are no calls left to abstract operations if
+            --  the current subprogram is not abstract.
+
+            if Nkind (Parent (N)) = N_Function_Call
+              and then N = Name (Parent (N))
+            then
+               if not Is_Abstract_Subprogram (Subp)
+                 and then Is_Abstract_Subprogram (Entity (N))
+               then
+                  Error_Msg_Sloc := Sloc (Current_Scope);
+                  Error_Msg_NE
+                    ("cannot call abstract subprogram in inherited condition "
+                      & "for&#", N, Current_Scope);
+
+               elsif Present (Alias (Subp))
+                 and then Warn_On_Suspicious_Contract
+                 and then SPARK_Mode = On
+               then
+                  Error_Msg_NE ("?inherited condition is modified, "
+                  & "build a wrapper for&", Parent (Subp), Subp);
+               end if;
+            end if;
+
+            --  Update type of function call node, which should be the same as
+            --  the function's return type.
+
+            if Is_Subprogram (Entity (N))
+              and then Nkind (Parent (N)) = N_Function_Call
+            then
+               Set_Etype (Parent (N), Etype (Entity (N)));
+            end if;
+
+         --  The whole expression will be reanalyzed
+
+         elsif Nkind (N) in N_Has_Etype then
+            Set_Analyzed (N, False);
+         end if;
+
+         return OK;
+      end Replace_Entity;
+
+      procedure Replace_Condition_Entities is
+        new Traverse_Proc (Replace_Entity);
+
+   begin
+      Replace_Condition_Entities (Prag);
+   end Build_Classwide_Expression;
+
    ---------------------------------------------------
    -- Check_Postcondition_Use_In_Inlined_Subprogram --
    ---------------------------------------------------
@@ -27948,6 +27848,15 @@ package body Sem_Prag is
       return Result;
    end Get_Base_Subprogram;
 
+   -----------------
+   -- Entity_Hash --
+   -----------------
+
+   function Entity_Hash (E : Entity_Id) return Num_Primitives is
+   begin
+      return Num_Primitives (E mod 511);
+   end Entity_Hash;
+
    -----------------------
    -- Get_SPARK_Mode_Type --
    -----------------------
@@ -29195,6 +29104,148 @@ package body Sem_Prag is
       Generate_Reference (Entity (With_Item), N, Set_Ref => False);
    end Set_Elab_Unit_Name;
 
+   -------------------------------
+   -- Update_Primitives_Mapping --
+   -------------------------------
+
+   procedure Update_Primitives_Mapping
+     (Inher_Id : Entity_Id;
+      Subp_Id  : Entity_Id)
+   is
+      function Overridden_Ancestor (S : Entity_Id) return Entity_Id;
+
+      -------------------------
+      -- Overridden_Ancestor --
+      -------------------------
+
+      function Overridden_Ancestor (S : Entity_Id) return Entity_Id is
+         Par : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
+         Anc : Entity_Id;
+
+      begin
+         Anc := S;
+
+         --  Locate the ancestor subprogram with the proper controlling
+         --  type.
+
+         while Present (Overridden_Operation (Anc)) loop
+            Anc := Overridden_Operation (Anc);
+            exit when Find_Dispatching_Type (Anc) = Par;
+         end loop;
+
+         return Anc;
+      end Overridden_Ancestor;
+
+      --  Local variables
+
+      Old_Typ  : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
+      Typ      : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
+      Decl     : Node_Id;
+      Old_Elmt : Elmt_Id;
+      Old_Prim : Entity_Id;
+      Prim     : Entity_Id;
+
+   --  Start of processing for Primitive_Mapping
+
+   begin
+      --  if the types are already in the map, it has been previously built
+      --  for some other overriding primitive.
+
+      if Primitives_Mapping.Get (Old_Typ)  = Typ then
+         return;
+
+      else
+
+         --  initialize new mapping with the primitive operations.
+
+         Decl := First (List_Containing (Unit_Declaration_Node (Subp_Id)));
+
+         --  look for primitive operations of the current type that have
+         --  overridden an operation of the type related to the original
+         --  class-wide precondition. there may be several intermediate
+         --  overridings between them.
+
+         while Present (Decl) loop
+            if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+                               N_Subprogram_Declaration)
+            then
+               Prim := Defining_Entity (Decl);
+
+               if Is_Subprogram (Prim)
+                 and then Present (Overridden_Operation (Prim))
+                 and then Find_Dispatching_Type (Prim) = Typ
+               then
+                  Old_Prim := Overridden_Ancestor (Prim);
+
+                  Primitives_Mapping.Set (Old_Prim, Prim);
+               end if;
+            end if;
+
+            Next (Decl);
+         end loop;
+
+         --  now examine inherited operations. these do not override, but have
+         --  an alias, which is the entity used in a call. that alias may be
+         --  inherited or come from source, in which case it may override an
+         --  earlier operation. we only need to examine inherited functions,
+         --  that can appear within the inherited expression.
+
+         Prim := First_Entity (Scope (Subp_Id));
+         while Present (Prim) loop
+            if not Comes_From_Source (Prim)
+              and then Ekind (Prim) = E_Function
+              and then Present (Alias (Prim))
+            then
+               Old_Prim := Alias (Prim);
+
+               if Comes_From_Source (Old_Prim) then
+                  Old_Prim := Overridden_Ancestor (Old_Prim);
+
+               else
+                  while Present (Alias (Old_Prim))
+                    and then Scope (Old_Prim) /= Scope (Inher_Id)
+                  loop
+                     Old_Prim := Alias (Old_Prim);
+
+                     if Comes_From_Source (Old_Prim) then
+                        Old_Prim := Overridden_Ancestor (Old_Prim);
+                        exit;
+                     end if;
+                  end loop;
+               end if;
+
+               Primitives_Mapping.Set (Old_Prim, Prim);
+            end if;
+
+            Next_Entity (Prim);
+         end loop;
+
+         --  if the parent operation is an interface operation, the
+         --  overriding indicator is not present. instead, we get from
+         --  the interface operation the primitive of the current type
+         --  that implements it.
+
+         if Is_Interface (Old_Typ) then
+            Old_Elmt := First_Elmt (Collect_Primitive_Operations (Old_Typ));
+            while Present (Old_Elmt) loop
+               Old_Prim := Node (Old_Elmt);
+               Prim := Find_Primitive_Covering_Interface (Typ, Old_Prim);
+
+               if Present (Prim) then
+                  Primitives_Mapping.Set (Old_Prim, Prim);
+               end if;
+
+               Next_Elmt (Old_Elmt);
+            end loop;
+         end if;
+      end if;
+
+      --  map the types themselves, so that the process is not repeated for
+      --  other overriding primitives.
+
+      Primitives_Mapping.Set (Old_Typ, Typ);
+   end Update_Primitives_Mapping;
+
    -------------------
    -- Test_Case_Arg --
    -------------------
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index d8607089a8d..064534f6ee3 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;