[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Mon, 4 Aug 2014 13:20:30 +0000 (15:20 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Mon, 4 Aug 2014 13:20:30 +0000 (15:20 +0200)
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
gcc/ada/exp_util.adb
gcc/ada/lib-writ.ads
gcc/ada/sem_disp.adb
gcc/ada/sem_disp.ads

index ca0d4e8..70db1c1 100644 (file)
@@ -1,3 +1,14 @@
+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
index bfba403..d5d269c 100644 (file)
@@ -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.
+      --  If E's scope is axiomatized, E 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));
+      declare
+         First_Ax_Parent_Scope : Entity_Id := Empty;
 
-         --  Otherwise, look at E's scope instead if present
+      begin
+         if Present (Scope (E)) then
+            First_Ax_Parent_Scope :=
+              Get_First_Parent_With_Ext_Axioms_For_Entity (Scope (E));
+         end if;
 
-      elsif Present (Scope (E)) then
-         return
-           Get_First_Parent_With_Ext_Axioms_For_Entity (Scope (E));
+         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.
 
-      else
-         return Empty;
-      end if;
+         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;
 
    ---------------------
index 941c69f..5a061e4 100644 (file)
@@ -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
index 35f6181..6d6078d 100644 (file)
@@ -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,68 +2082,79 @@ 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
 
-         Parent_Op := S;
-         loop
-            Parent_Op := Overridden_Operation (Parent_Op);
-            exit when No (Parent_Op);
-
-            if Is_Subprogram (Parent_Op)
-              or else Is_Generic_Subprogram (Parent_Op)
-            then
-               Store_IS (Parent_Op);
-            end if;
-         end loop;
+         if not Interfaces_Only then
+            Parent_Op := S;
+            loop
+               Parent_Op := Overridden_Operation (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)
+               then
+                  Store_IS (Parent_Op);
+               end if;
+            end loop;
+         end if;
 
          --  Now deal with interfaces
 
-         declare
-            Tag_Typ : Entity_Id;
-            Prim    : Entity_Id;
-            Elmt    : Elmt_Id;
+         if not No_Interfaces then
+            declare
+               Tag_Typ : Entity_Id;
+               Prim    : Entity_Id;
+               Elmt    : Elmt_Id;
 
-         begin
-            Tag_Typ := Find_Dispatching_Type (S);
+            begin
+               Tag_Typ := Find_Dispatching_Type (S);
 
-            if Is_Concurrent_Type (Tag_Typ) then
-               Tag_Typ := Corresponding_Record_Type (Tag_Typ);
-            end if;
+               if Is_Concurrent_Type (Tag_Typ) then
+                  Tag_Typ := Corresponding_Record_Type (Tag_Typ);
+               end if;
 
-            --  Search primitive operations of dispatching type
+               --  Search primitive operations of dispatching type
 
-            if Present (Tag_Typ)
-              and then Present (Primitive_Operations (Tag_Typ))
-            then
-               Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
-               while Present (Elmt) loop
-                  Prim := Node (Elmt);
+               if Present (Tag_Typ)
+                 and then Present (Primitive_Operations (Tag_Typ))
+               then
+                  Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
+                  while Present (Elmt) loop
+                     Prim := Node (Elmt);
 
-                  --  The following test eliminates some odd cases in which
-                  --  Ekind (Prim) is Void, to be investigated further ???
+                     --  The following test eliminates some odd cases in which
+                     --  Ekind (Prim) is Void, to be investigated further ???
 
-                  if not (Is_Subprogram (Prim)
-                            or else
-                          Is_Generic_Subprogram (Prim))
-                  then
-                     null;
+                     if not (Is_Subprogram         (Prim)
+                                or else
+                             Is_Generic_Subprogram (Prim))
+                     then
+                        null;
 
                      --  For [generic] subprogram, look at interface alias
 
-                  elsif Present (Interface_Alias (Prim))
-                    and then Alias (Prim) = S
-                  then
-                     --  We have found a primitive covered by S
+                     elsif Present (Interface_Alias (Prim))
+                       and then Alias (Prim) = S
+                     then
+                        --  We have found a primitive covered by S
 
-                     Store_IS (Interface_Alias (Prim));
-                  end if;
+                        Store_IS (Interface_Alias (Prim));
+                     end if;
 
-                  Next_Elmt (Elmt);
-               end loop;
-            end if;
-         end;
+                     Next_Elmt (Elmt);
+                  end loop;
+               end if;
+            end;
+         end if;
       end if;
 
       return Result (1 .. N);
index ff1ebc4..7dbec1b 100644 (file)
@@ -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
-   --  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