[multiple changes]

2015-01-06  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (New_Overloaded_Entity): In GNATprove mode, a
	function wrapper may be a homonym of another local declaration.
	* sem_ch8.adb (Analyze_Subprogram_Renaming): In GNATprove mode,
	build function and operator wrappers after the actual subprogram
	has been resolved, and replace the standard renaming declaration
	with the declaration of wrapper.
	* sem_ch12.ads (Build_Function_Wrapper, Build_Operator_Wraooer):
	make public for use elsewhere.
	* sem_ch12.adb (Build_Function_Wrapper, Build_Operator_Wraooer):
	rewrite, now that actual is fully resolved when wrapper is
	constructed.

2015-01-06  Javier Miranda  <miranda@adacore.com>

	* exp_disp.adb: Revert previous change.

From-SVN: r219232

gcc/ada/ChangeLog

+2015-01-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (New_Overloaded_Entity): In GNATprove mode, a
+	function wrapper may be a homonym of another local declaration.
+	* sem_ch8.adb (Analyze_Subprogram_Renaming): In GNATprove mode,
+	build function and operator wrappers after the actual subprogram
+	has been resolved, and replace the standard renaming declaration
+	with the declaration of wrapper.
+	* sem_ch12.ads (Build_Function_Wrapper, Build_Operator_Wraooer):
+	make public for use elsewhere.
+	* sem_ch12.adb (Build_Function_Wrapper, Build_Operator_Wraooer):
+	rewrite, now that actual is fully resolved when wrapper is
+	constructed.
+
+2015-01-06  Javier Miranda  <miranda@adacore.com>
+
+	* exp_disp.adb: Revert previous change.
+
 2015-01-06  Robert Dewar  <dewar@adacore.com>
 
 	* exp_util.adb: Change name Name_Table_Boolean to

gcc/ada/exp_disp.adb

@@ -1138,25 +1138,6 @@ package body Exp_Disp is
          Operand_Typ := Base_Type (Corresponding_Record_Type (Operand_Typ));
       end if;
 
-      --  No displacement of the pointer to the object needed when the type of
-      --  the operand is not an interface type and the interface is one of
-      --  its parent types (since they share the primary dispatch table).
-
-      declare
-         Opnd : Entity_Id := Operand_Typ;
-
-      begin
-         if Is_Access_Type (Opnd) then
-            Opnd := Designated_Type (Opnd);
-         end if;
-
-         if not Is_Interface (Opnd)
-           and then Is_Ancestor (Iface_Typ, Opnd, Use_Full_View => True)
-         then
-            return;
-         end if;
-      end;
-
       --  Evaluate if we can statically displace the pointer to the object
 
       declare
@@ -1196,6 +1177,11 @@ package body Exp_Disp is
                        Prefix         => New_Occurrence_Of (Iface_Typ, Loc),
                        Attribute_Name => Name_Tag))));
             end if;
+
+            --  Just do a conversion ???
+
+            Rewrite (N, Unchecked_Convert_To (Etype (N), N));
+            Analyze (N);
          end if;
 
          return;

gcc/ada/sem_ch12.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -37,6 +37,22 @@ package Sem_Ch12 is
    procedure Analyze_Formal_Subprogram_Declaration      (N : Node_Id);
    procedure Analyze_Formal_Package_Declaration         (N : Node_Id);
 
+   function Build_Function_Wrapper
+     (Formal : Entity_Id;
+      Actual : Entity_Id) return Node_Id;
+   --  In GNATprove mode, create a wrapper function for actuals that are
+   --  functions with any number of formal parameters, in order to propagate
+   --  their contract to the renaming declarations generated for them. This
+   --  is called after the renaming declaration created for the formal in the
+   --  instance has been analyzed, and the actual is known.
+
+   function Build_Operator_Wrapper
+     (Formal : Entity_Id;
+      Actual : Entity_Id) return Node_Id;
+   --  In GNATprove mode, create a wrapper function for actuals that are
+   --  operators, in order to propagate their contract to the renaming
+   --  declarations generated for them.
+
    procedure Start_Generic;
    --  Must be invoked before starting to process a generic spec or body
 

gcc/ada/sem_ch6.adb

@@ -9641,11 +9641,26 @@ package body Sem_Ch6 is
                      --  in the formal part, because in a generic body the
                      --  entity chain starts with the formals.
 
-                     pragma Assert
-                       (Present (Prev) or else Chars (E) = Name_Op_Concat);
+                     --  In GNATprove mode, a wrapper for an operation with
+                     --  axiomatization may be a homonym of another declaration
+                     --  for an actual subprogram (needs refinement ???).
+
+                     if No (Prev) then
+                        if In_Instance
+                          and then GNATprove_Mode
+                          and then
+                            Nkind (Original_Node (Unit_Declaration_Node (S))) =
+                                             N_Subprogram_Renaming_Declaration
+                        then
+                           return;
+                        else
+                           pragma Assert (Chars (E) = Name_Op_Concat);
+                           null;
+                        end if;
+                     end if;
 
                      --  E must be removed both from the entity_list of the
-                     --  current scope, and from the visibility chain
+                     --  current scope, and from the visibility chain.
 
                      if Debug_Flag_E then
                         Write_Str ("Override implicit operation ");

gcc/ada/sem_ch8.adb

@@ -3451,6 +3451,24 @@ package body Sem_Ch8 is
       Ada_Version := Save_AV;
       Ada_Version_Pragma := Save_AVP;
       Ada_Version_Explicit := Save_AV_Exp;
+
+      --  In GNATprove mode, the renamings of actual subprograms are replaced
+      --  with wrapper functions that make it easier to propagate axioms to the
+      --  points of call within an instance.
+
+      if Is_Actual
+        and then GNATprove_Mode
+        and then Present (Containing_Package_With_Ext_Axioms (Old_S))
+        and then not Inside_A_Generic
+      then
+         if Ekind (Old_S) = E_Function then
+            Rewrite (N, Build_Function_Wrapper (New_S, Old_S));
+            Analyze (N);
+         elsif Ekind (Old_S) = E_Operator then
+            Rewrite (N, Build_Operator_Wrapper (New_S, Old_S));
+            Analyze (N);
+         end if;
+      end if;
    end Analyze_Subprogram_Renaming;
 
    -------------------------