[multiple changes]

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

	* sem_ch12.adb, sem_ch12.ads, sem_ch8.adb: Ongoing work for wrappers
	for operators in SPARK.

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

	* exp_disp.adb: Revert previous patch again.

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

	* sem_aggr.adb (Get_Value): In ASIS mode, preanalyze the
	expression in an others association before making copies for
	separate resolution and accessibility checks. This ensures that
	the type of the expression is available to ASIS in all cases,
	in particular if the expression is itself an aggregate.

From-SVN: r219248

gcc/ada/ChangeLog

+2015-01-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb, sem_ch12.ads, sem_ch8.adb: Ongoing work for wrappers
+	for operators in SPARK.
+
+2015-01-06  Javier Miranda  <miranda@adacore.com>
+
+	* exp_disp.adb: Revert previous patch again.
+
+2015-01-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_aggr.adb (Get_Value): In ASIS mode, preanalyze the
+	expression in an others association before making copies for
+	separate resolution and accessibility checks. This ensures that
+	the type of the expression is available to ASIS in all cases,
+	in particular if the expression is itself an aggregate.
+
 2015-01-06  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* einfo.ads (Has_Independent_Components): Document extended

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

gcc/ada/sem_aggr.adb

@@ -3253,6 +3253,18 @@ package body Sem_Aggr is
                         --  access types, even in compile_only mode.
 
                         if not Inside_A_Generic then
+
+                           --  In ASIS mode, preanalyze the expression in an
+                           --  others association before making copies for
+                           --  separate resolution and accessibility checks.
+                           --  This ensures that the type of the expression is
+                           --  available to ASIS in all cases, in particular if
+                           --  the expression is itself an aggregate.
+
+                           if ASIS_Mode then
+                              Preanalyze_And_Resolve (Expression (Assoc), Typ);
+                           end if;
+
                            return
                              New_Copy_Tree_And_Copy_Dimensions
                                (Expression (Assoc));

gcc/ada/sem_ch12.adb

@@ -5125,10 +5125,10 @@ package body Sem_Ch12 is
    ----------------------------
 
    function Build_Function_Wrapper
-     (Formal : Entity_Id;
-      Actual : Entity_Id) return Node_Id
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : Entity_Id) return Node_Id
    is
-      Loc       : constant Source_Ptr := Sloc (Formal);
+      Loc       : constant Source_Ptr := Sloc (Formal_Subp);
       Actuals   : List_Id;
       Decl      : Node_Id;
       Func_Name : Node_Id;
@@ -5141,22 +5141,22 @@ package body Sem_Ch12 is
       New_F     : Entity_Id;
 
    begin
-      Func_Name := New_Occurrence_Of (Actual, Loc);
+      Func_Name := New_Occurrence_Of (Actual_Subp, Loc);
 
-      Func := Make_Defining_Identifier (Loc, Chars (Formal));
+      Func := Make_Defining_Identifier (Loc, Chars (Formal_Subp));
       Set_Ekind (Func, E_Function);
       Set_Is_Generic_Actual_Subprogram (Func);
 
       Actuals := New_List;
       Profile := New_List;
 
-      if Present (Actual) then
-         Act_F := First_Formal (Actual);
+      if Present (Actual_Subp) then
+         Act_F := First_Formal (Actual_Subp);
       else
          Act_F := Empty;
       end if;
 
-      Form_F := First_Formal (Formal);
+      Form_F := First_Formal (Formal_Subp);
       while Present (Form_F) loop
 
          --  Create new formal for profile of wrapper, and add a reference
@@ -5186,7 +5186,7 @@ package body Sem_Ch12 is
           Defining_Unit_Name       => Func,
           Parameter_Specifications => Profile,
           Result_Definition        =>
-            Make_Identifier (Loc, Chars (Etype (Formal))));
+            Make_Identifier (Loc, Chars (Etype (Formal_Subp))));
 
       Decl :=
         Make_Expression_Function (Loc,
@@ -5204,13 +5204,15 @@ package body Sem_Ch12 is
    ----------------------------
 
    function Build_Operator_Wrapper
-     (Formal : Entity_Id;
-      Actual : Entity_Id) return Node_Id
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : Entity_Id) return Node_Id
    is
-      Loc       : constant Source_Ptr := Sloc (Formal);
-      Typ       : constant Entity_Id := Etype (Formal);
+      Loc       : constant Source_Ptr := Sloc (Formal_Subp);
+      Ret_Type  : constant Entity_Id := Get_Instance_Of (Etype (Formal_Subp));
+      Op_Type   : constant Entity_Id := Get_Instance_Of
+                                          (Etype (First_Formal (Formal_Subp)));
       Is_Binary : constant Boolean :=
-                    Present (Next_Formal (First_Formal (Formal)));
+                    Present (Next_Formal (First_Formal (Formal_Subp)));
 
       Decl    : Node_Id;
       Expr    : Node_Id;
@@ -5221,7 +5223,7 @@ package body Sem_Ch12 is
       L, R    : Node_Id;
 
    begin
-      Op_Name := Chars (Actual);
+      Op_Name := Chars (Actual_Subp);
 
       --  Create entities for wrapper function and its formals
 
@@ -5230,7 +5232,7 @@ package body Sem_Ch12 is
       L  := New_Occurrence_Of (F1, Loc);
       R  := New_Occurrence_Of (F2, Loc);
 
-      Func := Make_Defining_Identifier (Loc, Chars (Formal));
+      Func := Make_Defining_Identifier (Loc, Chars (Formal_Subp));
       Set_Ekind (Func, E_Function);
       Set_Is_Generic_Actual_Subprogram (Func);
 
@@ -5240,29 +5242,25 @@ package body Sem_Ch12 is
           Parameter_Specifications => New_List (
             Make_Parameter_Specification (Loc,
                Defining_Identifier => F1,
-               Parameter_Type      =>
-                 Make_Identifier (Loc,
-                   Chars => Chars (Etype (First_Formal (Formal)))))),
-          Result_Definition        => Make_Identifier (Loc, Chars (Typ)));
+               Parameter_Type      => New_Occurrence_Of (Op_Type, Loc))),
+          Result_Definition        =>  New_Occurrence_Of (Ret_Type, Loc));
 
       if Is_Binary then
          Append_To (Parameter_Specifications (Spec),
             Make_Parameter_Specification (Loc,
               Defining_Identifier => F2,
-              Parameter_Type      =>
-                Make_Identifier (Loc,
-                  Chars (Etype (Next_Formal (First_Formal (Formal)))))));
+              Parameter_Type      => New_Occurrence_Of (Op_Type, Loc)));
       end if;
 
       --  Build expression as a function call, or as an operator node
       --  that corresponds to the name of the actual, starting with
       --  binary operators.
 
-      if Present (Actual) and then Op_Name not in Any_Operator_Name then
+      if Op_Name not in Any_Operator_Name then
          Expr :=
            Make_Function_Call (Loc,
              Name                   =>
-               New_Occurrence_Of (Entity (Actual), Loc),
+               New_Occurrence_Of (Actual_Subp, Loc),
              Parameter_Associations => New_List (L));
 
          if Is_Binary then
@@ -5322,13 +5320,6 @@ package body Sem_Ch12 is
          end if;
       end if;
 
-      --  Propagate visible entity to operator node, either from a
-      --  given actual or from a default.
-
-      if Is_Entity_Name (Actual) and then Nkind (Expr) in N_Op then
-         Set_Entity (Expr, Entity (Actual));
-      end if;
-
       Decl :=
         Make_Expression_Function (Loc,
           Specification => Spec,

gcc/ada/sem_ch12.ads

@@ -38,8 +38,8 @@ package Sem_Ch12 is
    procedure Analyze_Formal_Package_Declaration         (N : Node_Id);
 
    function Build_Function_Wrapper
-     (Formal : Entity_Id;
-      Actual : Entity_Id) return Node_Id;
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : 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
@@ -47,11 +47,12 @@ package Sem_Ch12 is
    --  instance has been analyzed, and the actual is known.
 
    function Build_Operator_Wrapper
-     (Formal : Entity_Id;
-      Actual : Entity_Id) return Node_Id;
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : 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.
+   --  declarations generated for them. The types are (the instances of)
+   --  the types of the formal subprogram.
 
    procedure Start_Generic;
    --  Must be invoked before starting to process a generic spec or body

gcc/ada/sem_ch8.adb

@@ -3465,8 +3465,13 @@ package body Sem_Ch8 is
          if Ekind (Old_S) = E_Function then
             Rewrite (N, Build_Function_Wrapper (New_S, Old_S));
             Analyze (N);
+
+         --  For wrappers of operators, the types are obtained from (the
+         --  instances of) the types of the formal subprogram, not from the
+         --  actual subprogram, that carries predefined types.
+
          elsif Ekind (Old_S) = E_Operator then
-            Rewrite (N, Build_Operator_Wrapper (New_S, Old_S));
+            Rewrite (N, Build_Operator_Wrapper (Formal_Spec, Old_S));
             Analyze (N);
          end if;
       end if;