[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

gcc/ada/ChangeLog

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

gcc/ada/sem_disp.adb

@@ -2201,6 +2201,12 @@ package body Sem_Disp is
    end Find_Primitive_Covering_Interface;
 
    ---------------------------
+   -- Inheritance_Utilities --
+   ---------------------------
+
+   package body Inheritance_Utilities is
+
+      ---------------------------
       -- Inherited_Subprograms --
       ---------------------------
 
@@ -2245,7 +2251,13 @@ package body Sem_Disp is
       begin
          pragma Assert (not (No_Interfaces and Interfaces_Only));
 
-      if Present (S) and then Is_Dispatching_Operation (S) then
+         --  When used from backends, visibility can be handled differently
+         --  resulting in no dispatching type being found.
+
+         if Present (S)
+           and then Is_Dispatching_Operation (S)
+           and then Present (Find_DT (S))
+         then
 
             --  Deal with direct inheritance
 
@@ -2257,7 +2269,7 @@ package body Sem_Disp is
                     or else
                       (No_Interfaces
                        and then
-                       Is_Interface (Find_Dispatching_Type (Parent_Op)));
+                       Is_Interface (Find_DT (Parent_Op)));
 
                   if Is_Subprogram_Or_Generic_Subprogram (Parent_Op) then
                      Store_IS (Parent_Op);
@@ -2278,7 +2290,7 @@ package body Sem_Disp is
                   Elmt    : Elmt_Id;
 
                begin
-               Tag_Typ := Find_Dispatching_Type (S);
+                  Tag_Typ := Find_DT (S);
 
                   --  In the presence of limited views there may be no visible
                   --  dispatching type. Primitives will be inherited when non-
@@ -2301,13 +2313,15 @@ package body Sem_Disp is
                      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;
 
-                     --  For [generic] subprogram, look at interface alias
+                           --  For [generic] subprogram, look at interface
+                           --  alias.
 
                         elsif Present (Interface_Alias (Prim))
                           and then Alias (Prim) = S
@@ -2333,6 +2347,36 @@ package body Sem_Disp is
          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 --

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;