[multiple changes]

2014-07-31  Arnaud Charlet  <charlet@adacore.com>

	* lib-writ.adb (Write_Unit_Information): Fix case where U =
	No_Unit.

2014-07-31  Claire Dross  <dross@adacore.com>

	* exp_util.adb, exp_util.ads
	(Get_First_Parent_With_External_Axiomatization_For_Entity):
	New routine to find the first parent of an entity with
	a pragma Annotate (GNATprove, External_Axiomatization).
	(Has_Annotate_Pragma_For_External_Axiomatization): New function
	to check if a package has a pragma Annotate (GNATprove,
	External_Axiomatization).
	* einfo.ads, einfo.adb (Is_Generic_Actual_Subprogram): New
	flag on the entity for the declaration created for a formal
	subprogram in an instance. This is a renaming declaration,
	or in GNATprove_Mode the declaration of an expression function
	that captures the axiomatization of the actual.
	* sem_ch6.adb (Analyze_Expression_Function): For a
	Generic_Actual_Subprogram, place body immediately after the
	declaration because it may be used in a subsequent declaration
	in the instance.
	* sem_ch12.adb (Build_Wrapper): Add code to handle instances where
	the actual is a function, not an operator. Handle functions with
	one and two parameters and binary and unary operators.

2014-07-31  Pascal Obry  <obry@adacore.com>

	* cstreams.c (__gnat_is_regular_file_fd): Removed.
	* adaint.c (__gnat_is_regular_file_fd): Added.

From-SVN: r213364

10 files changed, 396 insertions, 99 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0b297d5..08ec13e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,35 @@
+2014-07-31  Arnaud Charlet  <charlet@adacore.com>
+
+	* lib-writ.adb (Write_Unit_Information): Fix case where U =
+	No_Unit.
+
+2014-07-31  Claire Dross  <dross@adacore.com>
+
+	* exp_util.adb, exp_util.ads
+	(Get_First_Parent_With_External_Axiomatization_For_Entity):
+	New routine to find the first parent of an entity with
+	a pragma Annotate (GNATprove, External_Axiomatization).
+	(Has_Annotate_Pragma_For_External_Axiomatization): New function
+	to check if a package has a pragma Annotate (GNATprove,
+	External_Axiomatization).
+	* einfo.ads, einfo.adb (Is_Generic_Actual_Subprogram): New
+	flag on the entity for the declaration created for a formal
+	subprogram in an instance. This is a renaming declaration,
+	or in GNATprove_Mode the declaration of an expression function
+	that captures the axiomatization of the actual.
+	* sem_ch6.adb (Analyze_Expression_Function): For a
+	Generic_Actual_Subprogram, place body immediately after the
+	declaration because it may be used in a subsequent declaration
+	in the instance.
+	* sem_ch12.adb (Build_Wrapper): Add code to handle instances where
+	the actual is a function, not an operator. Handle functions with
+	one and two parameters and binary and unary operators.
+
+2014-07-31  Pascal Obry  <obry@adacore.com>
+
+	* cstreams.c (__gnat_is_regular_file_fd): Removed.
+	* adaint.c (__gnat_is_regular_file_fd): Added.
+
 2014-07-31  Robert Dewar  <dewar@adacore.com>
 
 	* exp_strm.adb: Minor reformatting.
diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c
index 96dedfe..5acb321 100644
--- a/gcc/ada/adaint.c
+++ b/gcc/ada/adaint.c
@@ -2024,6 +2024,16 @@ __gnat_is_regular_file (char *name)
 }
 
 int
+__gnat_is_regular_file_fd (int fd)
+{
+  int ret;
+  GNAT_STRUCT_STAT statbuf;
+
+  ret = GNAT_FSTAT (fd, &statbuf);
+  return (!ret && S_ISREG (statbuf.st_mode));
+}
+
+int
 __gnat_is_directory_attr (char* name, struct file_attributes* attr)
 {
    if (attr->directory == ATTR_UNSET)
diff --git a/gcc/ada/cstreams.c b/gcc/ada/cstreams.c
index 25a867a..5d5bc8d 100644
--- a/gcc/ada/cstreams.c
+++ b/gcc/ada/cstreams.c
@@ -6,7 +6,7 @@
  *                                                                          *
  *              Auxiliary C functions for Interfaces.C.Streams              *
  *                                                                          *
- *          Copyright (C) 1992-2012, 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- *
@@ -106,16 +106,6 @@ __gnat_fileno (FILE *stream)
    return (fileno (stream));
 }
 
-int
-__gnat_is_regular_file_fd (int fd)
-{
-  int ret;
-  GNAT_STRUCT_STAT statbuf;
-
-  ret = GNAT_FSTAT (fd, &statbuf);
-  return (!ret && S_ISREG (statbuf.st_mode));
-}
-
 /* on some systems, the constants for seek are not defined, if so, then
    provide the conventional definitions */
 
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 95d94ec..d4929c3 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -569,10 +569,11 @@ package body Einfo is
    --    (SSO_Set_Low_By_Default)        Flag272
    --    (SSO_Set_Low_By_Default)        Flag273
 
+   --    Is_Generic_Actual_Subprogram    Flag274
+
    --    (unused)                        Flag2
    --    (unused)                        Flag3
 
-   --    (unused)                        Flag274
    --    (unused)                        Flag275
    --    (unused)                        Flag276
    --    (unused)                        Flag277
@@ -2053,6 +2054,12 @@ package body Einfo is
       return Flag4 (Id);
    end Is_Frozen;
 
+   function Is_Generic_Actual_Subprogram (Id : E) return B is
+   begin
+      pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+      return Flag274 (Id);
+   end Is_Generic_Actual_Subprogram;
+
    function Is_Generic_Actual_Type (Id : E) return B is
    begin
       pragma Assert (Is_Type (Id));
@@ -4840,6 +4847,12 @@ package body Einfo is
       Set_Flag4 (Id, V);
    end Set_Is_Frozen;
 
+   procedure Set_Is_Generic_Actual_Subprogram (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+      Set_Flag274 (Id, V);
+   end Set_Is_Generic_Actual_Subprogram;
+
    procedure Set_Is_Generic_Actual_Type (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Type (Id));
@@ -8391,6 +8404,7 @@ package body Einfo is
       W ("Is_For_Access_Subtype",           Flag118 (Id));
       W ("Is_Formal_Subprogram",            Flag111 (Id));
       W ("Is_Frozen",                       Flag4   (Id));
+      W ("Is_Generic_Actual_Subprogram",    Flag274 (Id));
       W ("Is_Generic_Actual_Type",          Flag94  (Id));
       W ("Is_Generic_Instance",             Flag130 (Id));
       W ("Is_Generic_Type",                 Flag13  (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 4ca1baf..e71b576 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2388,6 +2388,17 @@ package Einfo is
 --       Defined in all type and subtype entities. Set if type or subtype has
 --       been frozen.
 
+--    Is_Generic_Actual_Subprogram (Flag274)
+--       Defined on functions and procedures. Set on the entity of the renaming
+--       declaration created within an instance for an actual subprogram.
+--       Used to generate constraint checks on calls to these subprograms, even
+--       within an instance of a predefined run-time unit, in which checks
+--       are otherwise suppressed.
+--
+--       The flag is also set on the entity of the expression function created
+--       within an instance, for a function that has external axiomatization,
+--       for use in GNATprove mode.
+
 --    Is_Generic_Actual_Type (Flag94)
 --       Defined in all type and subtype entities. Set in the subtype
 --       declaration that renames the generic formal as a subtype of the
@@ -5674,6 +5685,7 @@ package Einfo is
    --    Is_Discrim_SO_Function              (Flag176)
    --    Is_Discriminant_Check_Function      (Flag264)
    --    Is_Eliminated                       (Flag124)
+   --    Is_Generic_Actual_Subprogram        (Flag274)  (non-generic case only)
    --    Is_Inlined_Always                   (Flag1)    (non-generic case only)
    --    Is_Instantiated                     (Flag126)  (generic case only)
    --    Is_Intrinsic_Subprogram             (Flag64)
@@ -5968,6 +5980,7 @@ package Einfo is
    --    Is_Eliminated                       (Flag124)
    --    Is_Inlined_Always                   (Flag1)    (non-generic case only)
    --    Is_Instantiated                     (Flag126)  (generic case only)
+   --    Is_Generic_Actual_Subprogram        (Flag274)  (non-generic case only)
    --    Is_Interrupt_Handler                (Flag89)
    --    Is_Intrinsic_Subprogram             (Flag64)
    --    Is_Invariant_Procedure              (Flag257)  (non-generic case only)
@@ -6905,6 +6918,7 @@ package Einfo is
    function Is_Formal                           (Id : E) return B;
    function Is_Formal_Object                    (Id : E) return B;
    function Is_Formal_Subprogram                (Id : E) return B;
+   function Is_Generic_Actual_Subprogram        (Id : E) return B;
    function Is_Generic_Actual_Type              (Id : E) return B;
    function Is_Generic_Unit                     (Id : E) return B;
    function Is_Generic_Type                     (Id : E) return B;
@@ -7314,6 +7328,7 @@ package Einfo is
    procedure Set_Is_For_Access_Subtype           (Id : E; V : B := True);
    procedure Set_Is_Formal_Subprogram            (Id : E; V : B := True);
    procedure Set_Is_Frozen                       (Id : E; V : B := True);
+   procedure Set_Is_Generic_Actual_Subprogram    (Id : E; V : B := True);
    procedure Set_Is_Generic_Actual_Type          (Id : E; V : B := True);
    procedure Set_Is_Generic_Instance             (Id : E; V : B := True);
    procedure Set_Is_Generic_Type                 (Id : E; V : B := True);
@@ -8081,6 +8096,7 @@ package Einfo is
    pragma Inline (Is_Formal_Object);
    pragma Inline (Is_Formal_Subprogram);
    pragma Inline (Is_Frozen);
+   pragma Inline (Is_Generic_Actual_Subprogram);
    pragma Inline (Is_Generic_Actual_Type);
    pragma Inline (Is_Generic_Instance);
    pragma Inline (Is_Generic_Subprogram);
@@ -8541,6 +8557,7 @@ package Einfo is
    pragma Inline (Set_Is_For_Access_Subtype);
    pragma Inline (Set_Is_Formal_Subprogram);
    pragma Inline (Set_Is_Frozen);
+   pragma Inline (Set_Is_Generic_Actual_Subprogram);
    pragma Inline (Set_Is_Generic_Actual_Type);
    pragma Inline (Set_Is_Generic_Instance);
    pragma Inline (Set_Is_Generic_Type);
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index c99a674..5b7447c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -3228,6 +3228,53 @@ package body Exp_Util is
       end;
    end Get_Current_Value_Condition;
 
+   --------------------------------------------------------------
+   -- Get_First_Parent_With_External_Axiomatization_For_Entity --
+   --------------------------------------------------------------
+
+   function Get_First_Parent_With_External_Axiomatization_For_Entity
+     (E : Entity_Id) return Entity_Id is
+
+      Decl : Node_Id;
+
+   begin
+      if Ekind (E) = E_Package then
+         if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then
+            Decl := Parent (Parent (E));
+         else
+            Decl := Parent (E);
+         end if;
+      end if;
+
+      --  E is the package which is externally axiomatized
+
+      if Ekind (E) = E_Package
+        and then Has_Annotate_Pragma_For_External_Axiomatization (E)
+      then
+         return E;
+
+         --  E is a package instance, in which case it is axiomatized iff the
+         --  corresponding generic package is Axiomatized.
+
+      elsif Ekind (E) = E_Package
+        and then Present (Generic_Parent (Decl))
+      then
+         return Get_First_Parent_With_External_Axiomatization_For_Entity
+           (Generic_Parent (Decl));
+
+         --  Otherwise, look at E's scope instead if present
+
+      elsif Present (Scope (E)) then
+         return Get_First_Parent_With_External_Axiomatization_For_Entity
+             (Scope (E));
+
+         --  Else there is no such axiomatized package
+
+      else
+         return Empty;
+      end if;
+   end Get_First_Parent_With_External_Axiomatization_For_Entity;
+
    ---------------------
    -- Get_Stream_Size --
    ---------------------
@@ -3271,6 +3318,119 @@ package body Exp_Util is
       end if;
    end Has_Access_Constraint;
 
+   -----------------------------------------------------
+   -- Has_Annotate_Pragma_For_External_Axiomatization --
+   -----------------------------------------------------
+
+   function Has_Annotate_Pragma_For_External_Axiomatization
+     (E : Entity_Id) return Boolean
+   is
+
+      function Is_Annotate_Pragma_For_External_Axiomatization
+        (N : Node_Id) return Boolean;
+      --  Returns whether N is
+      --    pragma Annotate (GNATprove, External_Axiomatization);
+
+      ----------------------------------------------------
+      -- Is_Annotate_Pragma_For_External_Axiomatization --
+      ----------------------------------------------------
+
+      --  The general form of pragma Annotate is
+
+      --    pragma Annotate (IDENTIFIER [, IDENTIFIER {, ARG}]);
+      --    ARG ::= NAME | EXPRESSION
+
+      --  The first two arguments are by convention intended to refer to an
+      --  external tool and a tool-specific function. These arguments are
+      --  not analyzed.
+
+      --  The following is used to annotate a package specification which
+      --  GNATprove should treat specially, because the axiomatization of
+      --  this unit is given by the user instead of being automatically
+      --  generated.
+
+      --    pragma Annotate (GNATprove, External_Axiomatization);
+
+      function Is_Annotate_Pragma_For_External_Axiomatization
+        (N : Node_Id) return Boolean is
+
+         -------------------
+         -- Special Names --
+         -------------------
+
+         Name_GNATprove : constant String := "gnatprove";
+         Name_External_Axiomatization : constant String :=
+           "external_axiomatization";
+      begin
+         if Nkind (N) = N_Pragma
+           and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
+           and then List_Length (Pragma_Argument_Associations (N)) = 2
+         then
+            declare
+               Arg1 : constant Node_Id :=
+                 First (Pragma_Argument_Associations (N));
+               Arg2 : constant Node_Id := Next (Arg1);
+               Nam1 : Name_Id;
+               Nam2 : Name_Id;
+            begin
+               --  Fill in Name_Buffer with Name_GNATprove first, and then with
+               --  Name_External_Axiomatization so that Name_Find returns the
+               --  corresponding name. This takes care of all possible casings.
+
+               Name_Len := 0;
+               Add_Str_To_Name_Buffer (Name_GNATprove);
+               Nam1 := Name_Find;
+
+               Name_Len := 0;
+               Add_Str_To_Name_Buffer (Name_External_Axiomatization);
+               Nam2 := Name_Find;
+
+               return Chars (Get_Pragma_Arg (Arg1)) = Nam1
+                 and then
+                   Chars (Get_Pragma_Arg (Arg2)) = Nam2;
+            end;
+
+         else
+            return False;
+         end if;
+      end Is_Annotate_Pragma_For_External_Axiomatization;
+
+      Decl : Node_Id;
+      Vis_Decls : List_Id;
+      N         : Node_Id;
+
+   begin
+      if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then
+         Decl := Parent (Parent (E));
+      else
+         Decl := Parent (E);
+      end if;
+
+      Vis_Decls := Visible_Declarations (Decl);
+
+      N := First (Vis_Decls);
+      while Present (N) loop
+
+         --  Skip declarations generated by the frontend. Skip all pragmas
+         --  that are not the desired Annotate pragma. Stop the search on
+         --  the first non-pragma source declaration.
+
+         if Comes_From_Source (N) then
+            if Nkind (N) = N_Pragma then
+               if Is_Annotate_Pragma_For_External_Axiomatization (N) then
+                  return True;
+               end if;
+            else
+               return False;
+            end if;
+         end if;
+
+         Next (N);
+      end loop;
+
+      return False;
+   end Has_Annotate_Pragma_For_External_Axiomatization;
+
    ----------------------------------
    -- Has_Following_Address_Clause --
    ----------------------------------
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index a47c787..d5db0f6 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -525,12 +525,23 @@ package Exp_Util is
    --  N_Op_Eq), or to determine the result of some other test in other cases
    --  (e.g. no access check required if N_Op_Ne Null).
 
+   function Get_First_Parent_With_External_Axiomatization_For_Entity
+     (E : Entity_Id) return Entity_Id;
+   --  Returns the package entity with an external axiomatization containing E,
+   --  if any, or Empty if none.
+
    function Get_Stream_Size (E : Entity_Id) return Uint;
    --  Return the stream size value of the subtype E
 
    function Has_Access_Constraint (E : Entity_Id) return Boolean;
    --  Given object or type E, determine if a discriminant is of an access type
 
+   function Has_Annotate_Pragma_For_External_Axiomatization
+     (E : Entity_Id) return Boolean;
+   --  Returns whether E is a package entity, for which the initial list of
+   --  pragmas at the start of the package declaration contains
+   --    pragma Annotate (GNATprove, External_Axiomatization);
+
    function Has_Following_Address_Clause (D : Node_Id) return Boolean;
    --  D is the node for an object declaration. This function searches the
    --  current declarative part to look for an address clause for the object
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb
index 61d48e2..b4346a6 100644
--- a/gcc/ada/lib-writ.adb
+++ b/gcc/ada/lib-writ.adb
@@ -662,7 +662,9 @@ package body Lib.Writ is
                --  compilation unit.
 
             begin
-               if Nkind (Unit (Cunit (U))) = N_Subunit then
+               if U /= No_Unit
+                 and then Nkind (Unit (Cunit (U))) = N_Subunit
+               then
                   Note_Unit := Main_Unit;
                else
                   Note_Unit := U;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 2cae224..3637862 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -954,10 +954,14 @@ package body Sem_Ch12 is
       --  In Ada 2005, indicates partial parameterization of a formal
       --  package. As usual an other association must be last in the list.
 
-      function Build_Wrapper (Formal : Entity_Id) return Node_Id;
+      function Build_Wrapper
+        (Formal : Entity_Id;
+         Actual : Entity_Id := Empty) 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. If the actual is absent, this is
+      --  a formal with a default, and the name of the operator is that of the
+      --  formal.
 
       procedure Check_Overloaded_Formal_Subprogram (Formal : Entity_Id);
       --  Apply RM 12.3 (9): if a formal subprogram is overloaded, the instance
@@ -1010,20 +1014,31 @@ package body Sem_Ch12 is
       -- Build_Wrapper --
       -------------------
 
-      function Build_Wrapper (Formal : Entity_Id) return Node_Id is
+      function Build_Wrapper
+        (Formal : Entity_Id;
+         Actual : Entity_Id := Empty) return Node_Id
+      is
          Loc     : constant Source_Ptr := Sloc (I_Node);
-         Op_Name : constant Name_Id := Chars (Formal);
          Typ     : constant Entity_Id := Etype (Formal);
+         Is_Binary : constant Boolean :=
+                        Present (Next_Formal (First_Formal (Formal)));
 
          Decl   : Node_Id;
          Expr   : Node_Id;
          F1, F2 : Entity_Id;
          Func   : Entity_Id;
+         Op_Name : Name_Id;
          Spec   : Node_Id;
 
          L, R   : Node_Id;
 
       begin
+         if No (Actual) then
+            Op_Name := Chars (Formal);
+         else
+            Op_Name := Chars (Actual);
+         end if;
+
          --  Create entities for wrapper function and its formals
 
          F1 := Make_Temporary (Loc, 'A');
@@ -1031,92 +1046,109 @@ package body Sem_Ch12 is
          L  := New_Occurrence_Of (F1, Loc);
          R  := New_Occurrence_Of (F2, Loc);
 
-         Func := Make_Temporary (Loc, 'F');
+         Func := Make_Defining_Identifier (Loc, Chars (Formal));
+         Set_Ekind (Func, E_Function);
+         Set_Is_Generic_Actual_Subprogram (Func);
 
          Spec := Make_Function_Specification (Loc,
-               Defining_Unit_Name => Func,
+            Defining_Unit_Name => Func,
 
             Parameter_Specifications => New_List (
               Make_Parameter_Specification (Loc,
                 Defining_Identifier => F1,
-                Parameter_Type => Make_Identifier (Loc, Chars (Typ))),
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier => F2,
-                Parameter_Type => Make_Identifier (Loc, Chars (Typ)))),
+                Parameter_Type => Make_Identifier
+                  (Loc, Chars (Etype (First_Formal (Formal)))))),
 
             Result_Definition => Make_Identifier (Loc, Chars (Typ)));
 
-         --  Build expression as an operator node that corresponds to the
-         --  name of the actual, starting with binary operators.
+         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)))))));
+         end if;
 
-         if Op_Name = Name_Op_And then
-            Expr := Make_Op_And (Loc, Left_Opnd => L, Right_Opnd => R);
+         --  Build expression as a function call, or as an operator node
+         --  that corresponds to the name of the actual, starting with binary
+         --  operators.
 
-         elsif Op_Name = Name_Op_Or then
-            Expr := Make_Op_Or (Loc, Left_Opnd => L, Right_Opnd => R);
+         if Present (Actual) and then Op_Name not in Any_Operator_Name then
+            Expr := Make_Function_Call (Loc,
+                      Name => New_Occurrence_Of (Entity (Actual), Loc),
+                      Parameter_Associations => New_List (L));
 
-         elsif Op_Name = Name_Op_Xor then
-            Expr := Make_Op_Xor (Loc, Left_Opnd => L, Right_Opnd => R);
+            if Is_Binary then
+               Append_To (Parameter_Associations (Expr), R);
+            end if;
 
-         elsif Op_Name = Name_Op_Eq then
-            Expr := Make_Op_Eq (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Is_Binary then
+            if Op_Name = Name_Op_And then
+               Expr := Make_Op_And (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Ne then
-            Expr := Make_Op_Ne (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Or then
+               Expr := Make_Op_Or (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Le then
-            Expr := Make_Op_Le (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Xor then
+               Expr := Make_Op_Xor (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Gt then
-            Expr := Make_Op_Gt (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Eq then
+               Expr := Make_Op_Eq (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Ge then
-            Expr := Make_Op_Ge (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Ne then
+               Expr := Make_Op_Ne (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Lt then
-            Expr := Make_Op_Lt (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Le then
+               Expr := Make_Op_Le (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Add then
-            Expr := Make_Op_Add (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Gt then
+               Expr := Make_Op_Gt (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Subtract then
-            Expr := Make_Op_Subtract (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Ge then
+               Expr := Make_Op_Ge (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Concat then
-            Expr := Make_Op_Concat (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Lt then
+               Expr := Make_Op_Lt (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Multiply then
-            Expr := Make_Op_Multiply (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Add then
+               Expr := Make_Op_Add (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Divide then
-            Expr := Make_Op_Divide (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Subtract then
+               Expr := Make_Op_Subtract (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Mod then
-            Expr := Make_Op_Mod (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Concat then
+               Expr := Make_Op_Concat (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Rem then
-            Expr := Make_Op_Rem (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Multiply then
+               Expr := Make_Op_Multiply (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Expon then
-            Expr := Make_Op_Expon (Loc, Left_Opnd => L, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Divide then
+               Expr := Make_Op_Divide (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         --  Unary operators.
+            elsif Op_Name = Name_Op_Mod then
+               Expr := Make_Op_Mod (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Add
-           and then No (Next_Formal (First_Formal (Actual)))
-         then
-            Expr := Make_Op_Plus (Loc, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Rem then
+               Expr := Make_Op_Rem (Loc, Left_Opnd => L, Right_Opnd => R);
 
-         elsif Op_Name = Name_Op_Subtract
-           and then No (Next_Formal (First_Formal (Actual)))
-         then
-            Expr := Make_Op_Minus (Loc, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Expon then
+               Expr := Make_Op_Expon (Loc, Left_Opnd => L, Right_Opnd => R);
+            end if;
+
+         else    --  Unary operators.
+
+            if Op_Name = Name_Op_Add then
+               Expr := Make_Op_Plus (Loc, Right_Opnd => L);
 
-         elsif Op_Name = Name_Op_Abs then
-            Expr := Make_Op_Abs (Loc, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Subtract then
+               Expr := Make_Op_Minus (Loc, Right_Opnd => L);
 
-         elsif Op_Name = Name_Op_Not then
-            Expr := Make_Op_Not (Loc, Right_Opnd => R);
+            elsif Op_Name = Name_Op_Abs then
+               Expr := Make_Op_Abs (Loc, Right_Opnd => L);
+
+            elsif Op_Name = Name_Op_Not then
+               Expr := Make_Op_Not (Loc, Right_Opnd => L);
+            end if;
          end if;
 
          Decl := Make_Expression_Function (Loc,
@@ -1642,24 +1674,42 @@ package body Sem_Ch12 is
                      end if;
 
                   else
-                     Append_To (Assoc,
-                       Instantiate_Formal_Subprogram
-                         (Formal, Match, Analyzed_Formal));
+                     if GNATprove_Mode
+                        and then Ekind (Defining_Entity (Analyzed_Formal))
+                          = E_Function
+                     then
+
+                        --  If actual is an entity (function or operator),
+                        --  build wrapper for it.
 
-                     if GNATprove_Mode then
-                        if Nkind (Match) = N_Operator_Symbol then
+                        if Present (Match) and then Is_Entity_Name (Match) then
                            Append_To (Assoc,
                              Build_Wrapper
-                               (Defining_Entity (Analyzed_Formal)));
+                               (Defining_Entity (Analyzed_Formal), Match));
+
+                        --  Ditto if formal is an operator with a default.
 
                         elsif Box_Present (Formal)
                            and then Nkind (Defining_Entity (Analyzed_Formal))
                              = N_Defining_Operator_Symbol
+
                         then
                            Append_To (Assoc,
                              Build_Wrapper
                                (Defining_Entity (Analyzed_Formal)));
+
+                        --  Otherwise create renaming declaration.
+
+                        else
+                           Append_To (Assoc,
+                             Instantiate_Formal_Subprogram
+                               (Formal, Match, Analyzed_Formal));
                         end if;
+
+                     else
+                        Append_To (Assoc,
+                          Instantiate_Formal_Subprogram
+                            (Formal, Match, Analyzed_Formal));
                      end if;
 
                      --  An instantiation is a freeze point for the actuals,
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 3143a93..9b261d9 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -473,34 +473,45 @@ package body Sem_Ch6 is
             Id    : constant Entity_Id := Defining_Entity (N);
 
          begin
-            if Nkind (Par) = N_Package_Specification
-              and then Decls = Visible_Declarations (Par)
-              and then Present (Private_Declarations (Par))
-              and then not Is_Empty_List (Private_Declarations (Par))
+            --  If this is a wrapper created for in an instance for a formal
+            --  subprogram, insert body after declaration, to be analyzed when
+            --  the enclosing instance is analyzed.
+
+            if GNATprove_Mode
+              and then Is_Generic_Actual_Subprogram (Defining_Entity (N))
             then
-               Decls := Private_Declarations (Par);
-            end if;
+               Insert_After (N, New_Body);
 
-            Insert_After (Last (Decls), New_Body);
-            Push_Scope (Id);
-            Install_Formals (Id);
+            else
+               if Nkind (Par) = N_Package_Specification
+                 and then Decls = Visible_Declarations (Par)
+                 and then Present (Private_Declarations (Par))
+                 and then not Is_Empty_List (Private_Declarations (Par))
+               then
+                  Decls := Private_Declarations (Par);
+               end if;
 
-            --  Preanalyze the expression for name capture, except in an
-            --  instance, where this has been done during generic analysis,
-            --  and will be redone when analyzing the body.
+               Insert_After (Last (Decls), New_Body);
+               Push_Scope (Id);
+               Install_Formals (Id);
 
-            declare
-               Expr : constant Node_Id := Expression (Ret);
+               --  Preanalyze the expression for name capture, except in an
+               --  instance, where this has been done during generic analysis,
+               --  and will be redone when analyzing the body.
 
-            begin
-               Set_Parent (Expr, Ret);
+               declare
+                  Expr : constant Node_Id := Expression (Ret);
 
-               if not In_Instance then
-                  Preanalyze_Spec_Expression (Expr, Etype (Id));
-               end if;
-            end;
+               begin
+                  Set_Parent (Expr, Ret);
 
-            End_Scope;
+                  if not In_Instance then
+                     Preanalyze_Spec_Expression (Expr, Etype (Id));
+                  end if;
+               end;
+
+               End_Scope;
+            end if;
          end;
       end if;