[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

gcc/ada/ChangeLog

+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.

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)

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 */
 

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));

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);

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 --
    ----------------------------------

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

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;

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;