[Ada] Crash on classwide precondition for interface operation

[Pierre-Marie de Rodat]

This patch fixes a crash on a classwide precondition on an interface
primitive with an controlling access parameter, when the precondition is
a call that contains a reference to that formal.

The following must execute quietly:

   gnatmake -q main
   main

---
with Conditional_Interfaces;
with Conditional_Objects;

procedure Main is

   D  : aliased Conditional_Interfaces.Data_Object;
   O  : aliased Conditional_Objects.Object;
   IA : not null access Conditional_Interfaces.Conditional_Interface'Class :=
          O'Access;
   I  : Conditional_Interfaces.Conditional_Interface'Class renames
          Conditional_Interfaces.Conditional_Interface'Class (O);
begin
   O.Do_Stuff;
   O.Do_Stuff_Access;
   O.Update_Data (D'Unchecked_Access);
   IA.Do_Stuff;
   IA.Do_Stuff_Access;
   IA.Update_Data (D'Unchecked_Access); --
                     Commenting this line prevents the error.
   I.Do_Stuff;

   -- These also raises an error
   --  "call to abstract function must be dispatching" which seems incorrect
   --  I.Do_Stuff_Access;
   --  I.Update_Data (D'Unchecked_Access);
end Main;
---
package Conditional_Interfaces is
   type Conditional_Interface is limited interface;

   type Data_Object is tagged null record;

   function Is_Valid
     (This : in Conditional_Interface)
      return Boolean is abstract;

   function Is_Supported_Data
     (This : in Conditional_Interface;
      Data : not null access Data_Object'Class)
      return Boolean is abstract;

   procedure Do_Stuff
     (This : in out Conditional_Interface) is abstract
     with
       Pre'Class => This.Is_Valid;

   procedure Do_Stuff_Access
     (This : not null access Conditional_Interface) is abstract
     with
       Pre'Class => This.Is_Valid;

   procedure Update_Data
     (This : not null access Conditional_Interface;
      Data : not null access Data_Object'Class) is abstract
     with
       Pre'Class => This.Is_Supported_Data (Data)

end Conditional_Interfaces;
---
package body Conditional_Objects is

   procedure Update_Data
     (This : not null access Object;
      Data : not null access Conditional_Interfaces.Data_Object'Class)
   is
   begin
      null;
   end Update_Data;

end Conditional_Objects;
---
with Conditional_Interfaces;

package Conditional_Objects is

   type Object is limited new
     Conditional_Interfaces.Conditional_Interface with null record;

   function Is_Valid
     (This : in Object)
      return Boolean
   is
     (True);

   function Is_Supported_Data
     (This : in Object;
      Data : not null access Conditional_Interfaces.Data_Object'Class)
      return Boolean
   is
     (True);

   procedure Do_Stuff
     (This : in out Object) is null;

   procedure Do_Stuff_Access
     (This : not null access Object) is null;

   procedure Update_Data
     (This : not null access Object;
      Data : not null access Conditional_Interfaces.Data_Object'Class)
-- Doesn't cause errors:
--       with
--         Pre => This.Is_Supported_Data (Data)
   ;
end Conditional_Objects;

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-09-25  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch6.adb (Expand_Call_Helper): The extra accessibility check in a
	call that appears in a classwide precondition and that mentions an
	access formal of the subprogram, must use the accessibility level of
	the actual in the call. This is one case in which a reference to a
	formal parameter appears outside of the body of the subprogram.

-------------- next part --------------
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 253134)
+++ exp_ch6.adb	(working copy)
@@ -3004,6 +3004,20 @@
             then
                Prev_Orig := Prev;
 
+            --  A class-wide precondition generates a test in which formals of
+            --  the subprogram are replaced by actuals that came from source.
+            --  In that case as well, the accessiblity comes from the actual.
+            --  This is the one case in which there are references to formals
+            --  outside of their subprogram.
+
+            elsif Prev_Orig /= Prev
+              and then Is_Entity_Name (Prev_Orig)
+              and then Present (Entity (Prev_Orig))
+              and then Is_Formal (Entity (Prev_Orig))
+              and then not In_Open_Scopes (Scope (Entity (Prev_Orig)))
+            then
+               Prev_Orig := Prev;
+
             --  If the actual is a formal of an enclosing subprogram it is
             --  the right entity, even if it is a rewriting. This happens
             --  when the call is within an inherited condition or predicate.