[multiple changes]

2014-08-04  Claire Dross  <dross@adacore.com>

	* exp_util.adb (Get_First_Parent_With_Ext_Axioms_For_Entity):
	For an instance, look at the scope before the generic parent.

2014-08-04  Yannick Moy  <moy@adacore.com>

	* lib-writ.ads: Update comments.
	* sem_disp.ads, sem_disp.adb (Inherited_Subprograms): Add
	parameters to filter inherited subprograms.

From-SVN: r213590

gcc/ada/ChangeLog

+2014-08-04  Claire Dross  <dross@adacore.com>
+
+	* exp_util.adb (Get_First_Parent_With_Ext_Axioms_For_Entity):
+	For an instance, look at the scope before the generic parent.
+
+2014-08-04  Yannick Moy  <moy@adacore.com>
+
+	* lib-writ.ads: Update comments.
+	* sem_disp.ads, sem_disp.adb (Inherited_Subprograms): Add
+	parameters to filter inherited subprograms.
+
 2014-08-04  Robert Dewar  <dewar@adacore.com>
 
 	* gnat_rm.texi: Add section on use of address clause for memory

gcc/ada/exp_util.adb

@@ -3319,27 +3319,36 @@ package body Exp_Util is
         and then Has_Annotate_Pragma_For_External_Axiomatization (E)
       then
          return E;
+      end if;
 
-         --  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_Ext_Axioms_For_Entity (Generic_Parent (Decl));
+      --  If E's scope is axiomatized, E is axiomatized.
 
-         --  Otherwise, look at E's scope instead if present
+      declare
+         First_Ax_Parent_Scope : Entity_Id := Empty;
 
-      elsif Present (Scope (E)) then
-         return
+      begin
+         if Present (Scope (E)) then
+            First_Ax_Parent_Scope :=
               Get_First_Parent_With_Ext_Axioms_For_Entity (Scope (E));
+         end if;
+
+         if Present (First_Ax_Parent_Scope) then
+            return First_Ax_Parent_Scope;
+         end if;
 
-         --  Else there is no such axiomatized package
+         --  otherwise, if E is a package instance, it is axiomatized if the
+         --  corresponding generic package is axiomatized.
 
+         if Ekind (E) = E_Package
+           and then Present (Generic_Parent (Decl))
+         then
+            return
+              Get_First_Parent_With_Ext_Axioms_For_Entity
+                (Generic_Parent (Decl));
          else
             return Empty;
          end if;
+      end;
    end Get_First_Parent_With_Ext_Axioms_For_Entity;
 
    ---------------------

gcc/ada/lib-writ.ads

@@ -917,7 +917,8 @@ package Lib.Writ is
    procedure Write_ALI (Object : Boolean);
    --  This procedure writes the library information for the current main unit
    --  The Object parameter is true if an object file is created, and false
-   --  otherwise.
+   --  otherwise. Note that the pseudo-object file generated in GNATProve mode
+   --  does count as an object file from this point of view.
    --
    --  Note: in the case where we are not generating code (-gnatc mode), this
    --  routine only writes an ALI file if it cannot find an existing up to

gcc/ada/sem_disp.adb

@@ -2044,7 +2044,11 @@ package body Sem_Disp is
    -- Inherited_Subprograms --
    ---------------------------
 
-   function Inherited_Subprograms (S : Entity_Id) return Subprogram_List is
+   function Inherited_Subprograms
+     (S               : Entity_Id;
+      No_Interfaces   : Boolean := False;
+      Interfaces_Only : Boolean := False) return Subprogram_List
+   is
       Result : Subprogram_List (1 .. 6000);
       --  6000 here is intended to be infinity. We could use an expandable
       --  table, but it would be awfully heavy, and there is no way that we
@@ -2078,24 +2082,34 @@ package body Sem_Disp is
    --  Start of processing for Inherited_Subprograms
 
    begin
+      pragma Assert (not (No_Interfaces and Interfaces_Only));
+
       if Present (S) and then Is_Dispatching_Operation (S) then
 
          --  Deal with direct inheritance
 
+         if not Interfaces_Only then
             Parent_Op := S;
             loop
                Parent_Op := Overridden_Operation (Parent_Op);
-            exit when No (Parent_Op);
+               exit when No (Parent_Op)
+                 or else
+                   (No_Interfaces
+                     and then
+                       Is_Interface (Find_Dispatching_Type (Parent_Op)));
 
                if Is_Subprogram         (Parent_Op)
-              or else Is_Generic_Subprogram (Parent_Op)
+                    or else
+                  Is_Generic_Subprogram (Parent_Op)
                then
                   Store_IS (Parent_Op);
                end if;
             end loop;
+         end if;
 
          --  Now deal with interfaces
 
+         if not No_Interfaces then
             declare
                Tag_Typ : Entity_Id;
                Prim    : Entity_Id;
@@ -2141,6 +2155,7 @@ package body Sem_Disp is
                end if;
             end;
          end if;
+      end if;
 
       return Result (1 .. N);
    end Inherited_Subprograms;

gcc/ada/sem_disp.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          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- --
@@ -97,13 +97,22 @@ package Sem_Disp is
    type Subprogram_List is array (Nat range <>) of Entity_Id;
    --  Type returned by Inherited_Subprograms function
 
-   function Inherited_Subprograms (S : Entity_Id) return Subprogram_List;
+   function Inherited_Subprograms
+     (S               : Entity_Id;
+      No_Interfaces   : Boolean := False;
+      Interfaces_Only : Boolean := False) return Subprogram_List;
    --  Given the spec of a subprogram, this function gathers any inherited
-   --  subprograms from direct inheritance or via interfaces. The list is
-   --  a list of entity id's of the specs of inherited subprograms. Returns
-   --  a null array if passed an Empty spec id. Note that the returned array
+   --  subprograms from direct inheritance or via interfaces. The list is a
+   --  list of entity id's of the specs of inherited subprograms. Returns a
+   --  null array if passed an Empty spec id. Note that the returned array
    --  only includes subprograms and generic subprograms (and excludes any
-   --  other inherited entities, in particular enumeration literals).
+   --  other inherited entities, in particular enumeration literals). If
+   --  No_Interfaces is True, only return inherited subprograms not coming
+   --  from an interface. If Interfaces_Only is True, only return inherited
+   --  subprograms from interfaces. Otherwise, subprograms inherited directly
+   --  come first, starting with the closest ancestors, and are followed by
+   --  subprograms inherited from interfaces. At most one of No_Interfaces
+   --  and Interfaces_Only should be True.
 
    function Is_Dynamically_Tagged (N : Node_Id) return Boolean;
    --  Used to determine whether a call is dispatching, i.e. if is an