[Ada] Allow for GNATprove specific versions of routines from Sem_Disp

2018-05-28  Claire Dross  <dross@adacore.com>

gcc/ada/

	* sem_disp.ads, sem_disp.adb (Inheritance_Utilities): Package for
	generic inheritance utilities.
	(Generic_Inherited_Subprograms): Generic version of
	Inherited_Subprograms, generic in Find_Dispatching_Type function.
	(Generic_Is_Overriding_Subprogram): Generic version of
	Is_Overriding_Subprogram, generic in Find_Dispatching_Type function.
	(Inherited_Subprograms): Instance of Generic_Inherited_Subprograms with
	Sem_Disp.Find_Dispatching_Type.
	(Is_Overriding_Subprogram): Instance of
	Generic_Is_Overriding_Subprogram with Sem_Disp.Find_Dispatching_Type.
	(Inheritance_Utilities_Inst): Instance of Inheritance_Utilities
	with Sem_Disp.Find_Dispatching_Type.

From-SVN: r260835

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b10bd6e..4310667 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2018-05-28  Claire Dross  <dross@adacore.com>
+
+       * sem_disp.ads, sem_disp.adb (Inheritance_Utilities): Package for
+       generic inheritance utilities.
+       (Generic_Inherited_Subprograms): Generic version of
+       Inherited_Subprograms, generic in Find_Dispatching_Type function.
+       (Generic_Is_Overriding_Subprogram): Generic version of
+       Is_Overriding_Subprogram, generic in Find_Dispatching_Type function.
+       (Inherited_Subprograms): Instance of Generic_Inherited_Subprograms with
+       Sem_Disp.Find_Dispatching_Type.
+       (Is_Overriding_Subprogram): Instance of
+       Generic_Is_Overriding_Subprogram with Sem_Disp.Find_Dispatching_Type.
+       (Inheritance_Utilities_Inst): Instance of Inheritance_Utilities
+       with Sem_Disp.Find_Dispatching_Type.
+
 2018-05-28  Eric Botcazou  <ebotcazou@adacore.com>
 
        * exp_ch4.adb (Expand_Composite_Equality): For a composite (or FP)

diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 69c2a56..54c20b5 100644 (file)
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -2201,137 +2201,181 @@ package body Sem_Disp is
    end Find_Primitive_Covering_Interface;
 
    ---------------------------
-   -- Inherited_Subprograms --
+   -- Inheritance_Utilities --
    ---------------------------
 
-   function Inherited_Subprograms
-     (S               : Entity_Id;
-      No_Interfaces   : Boolean := False;
-      Interfaces_Only : Boolean := False;
-      One_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
-      --  could reasonably exceed this value.
+   package body Inheritance_Utilities is
 
-      N : Nat := 0;
-      --  Number of entries in Result
+      ---------------------------
+      -- Inherited_Subprograms --
+      ---------------------------
 
-      Parent_Op : Entity_Id;
-      --  Traverses the Overridden_Operation chain
+      function Inherited_Subprograms
+        (S               : Entity_Id;
+         No_Interfaces   : Boolean := False;
+         Interfaces_Only : Boolean := False;
+         One_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
+         --  could reasonably exceed this value.
 
-      procedure Store_IS (E : Entity_Id);
-      --  Stores E in Result if not already stored
+         N      : Nat := 0;
+         --  Number of entries in Result
 
-      --------------
-      -- Store_IS --
-      --------------
+         Parent_Op : Entity_Id;
+         --  Traverses the Overridden_Operation chain
 
-      procedure Store_IS (E : Entity_Id) is
-      begin
-         for J in 1 .. N loop
-            if E = Result (J) then
-               return;
-            end if;
-         end loop;
+         procedure Store_IS (E : Entity_Id);
+         --  Stores E in Result if not already stored
 
-         N := N + 1;
-         Result (N) := E;
-      end Store_IS;
+         --------------
+         -- Store_IS --
+         --------------
 
-   --  Start of processing for Inherited_Subprograms
+         procedure Store_IS (E : Entity_Id) is
+         begin
+            for J in 1 .. N loop
+               if E = Result (J) then
+                  return;
+               end if;
+            end loop;
 
-   begin
-      pragma Assert (not (No_Interfaces and Interfaces_Only));
+            N := N + 1;
+            Result (N) := E;
+         end Store_IS;
 
-      if Present (S) and then Is_Dispatching_Operation (S) then
+         --  Start of processing for Inherited_Subprograms
 
-         --  Deal with direct inheritance
+      begin
+         pragma Assert (not (No_Interfaces and Interfaces_Only));
 
-         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)));
+         --  When used from backends, visibility can be handled differently
+         --  resulting in no dispatching type being found.
 
-               if Is_Subprogram_Or_Generic_Subprogram (Parent_Op) then
-                  Store_IS (Parent_Op);
+         if Present (S)
+           and then Is_Dispatching_Operation (S)
+           and then Present (Find_DT (S))
+         then
 
-                  if One_Only then
-                     goto Done;
+            --  Deal with direct inheritance
+
+            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_DT (Parent_Op)));
+
+                  if Is_Subprogram_Or_Generic_Subprogram (Parent_Op) then
+                     Store_IS (Parent_Op);
+
+                     if One_Only then
+                        goto Done;
+                     end if;
                   end if;
-               end if;
-            end loop;
-         end if;
+               end loop;
+            end if;
 
-         --  Now deal with interfaces
+            --  Now deal with interfaces
 
-         if not No_Interfaces then
-            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_DT (S);
 
-               --  In the presence of limited views there may be no visible
-               --  dispatching type. Primitives will be inherited when non-
-               --  limited view is frozen.
+                  --  In the presence of limited views there may be no visible
+                  --  dispatching type. Primitives will be inherited when non-
+                  --  limited view is frozen.
 
-               if No (Tag_Typ) then
-                  return Result (1 .. 0);
-               end if;
+                  if No (Tag_Typ) then
+                     return Result (1 .. 0);
+                  end if;
 
-               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_Or_Generic_Subprogram (Prim) then
-                        null;
+                        if not Is_Subprogram_Or_Generic_Subprogram (Prim) then
+                           null;
 
-                     --  For [generic] subprogram, look at interface alias
+                           --  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));
+                           Store_IS (Interface_Alias (Prim));
 
-                        if One_Only then
-                           goto Done;
+                           if One_Only then
+                              goto Done;
+                           end if;
                         end if;
-                     end if;
 
-                     Next_Elmt (Elmt);
-                  end loop;
-               end if;
-            end;
+                        Next_Elmt (Elmt);
+                     end loop;
+                  end if;
+               end;
+            end if;
          end if;
-      end if;
 
-      <<Done>>
+         <<Done>>
+
+         return Result (1 .. N);
+      end Inherited_Subprograms;
 
-      return Result (1 .. N);
-   end Inherited_Subprograms;
+      ------------------------------
+      -- Is_Overriding_Subprogram --
+      ------------------------------
+
+      function Is_Overriding_Subprogram (E : Entity_Id) return Boolean is
+         Inherited : constant Subprogram_List :=
+           Inherited_Subprograms (E, One_Only => True);
+      begin
+         return Inherited'Length > 0;
+      end Is_Overriding_Subprogram;
+   end Inheritance_Utilities;
+
+   --------------------------------
+   -- Inheritance_Utilities_Inst --
+   --------------------------------
+
+   package Inheritance_Utilities_Inst is new
+     Inheritance_Utilities (Find_Dispatching_Type);
+
+   ---------------------------
+   -- Inherited_Subprograms --
+   ---------------------------
+
+   function Inherited_Subprograms
+     (S               : Entity_Id;
+      No_Interfaces   : Boolean := False;
+      Interfaces_Only : Boolean := False;
+      One_Only        : Boolean := False) return Subprogram_List renames
+     Inheritance_Utilities_Inst.Inherited_Subprograms;
 
    ---------------------------
    -- Is_Dynamically_Tagged --
@@ -2410,12 +2454,8 @@ package body Sem_Disp is
    -- Is_Overriding_Subprogram --
    ------------------------------
 
-   function Is_Overriding_Subprogram (E : Entity_Id) return Boolean is
-      Inherited : constant Subprogram_List :=
-                    Inherited_Subprograms (E, One_Only => True);
-   begin
-      return Inherited'Length > 0;
-   end Is_Overriding_Subprogram;
+   function Is_Overriding_Subprogram (E : Entity_Id) return Boolean renames
+     Inheritance_Utilities_Inst.Is_Overriding_Subprogram;
 
    --------------------------
    -- Is_Tag_Indeterminate --

diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads
index 1d3e762..f1a86c0 100644 (file)
--- a/gcc/ada/sem_disp.ads
+++ b/gcc/ada/sem_disp.ads
@@ -100,6 +100,24 @@ package Sem_Disp is
    type Subprogram_List is array (Nat range <>) of Entity_Id;
    --  Type returned by Inherited_Subprograms function
 
+   generic
+      with function Find_DT (Subp : Entity_Id) return Entity_Id;
+   package Inheritance_Utilities is
+
+      --  This package provides generic versions of inheritance utilities
+      --  provided here. These versions are used in GNATprove backend to
+      --  adapt these utilities to GNATprove specific version of visibility of
+      --  types.
+
+      function Inherited_Subprograms
+        (S               : Entity_Id;
+         No_Interfaces   : Boolean := False;
+         Interfaces_Only : Boolean := False;
+         One_Only        : Boolean := False) return Subprogram_List;
+
+      function Is_Overriding_Subprogram (E : Entity_Id) return Boolean;
+   end Inheritance_Utilities;
+
    function Inherited_Subprograms
      (S               : Entity_Id;
       No_Interfaces   : Boolean := False;