[Ada] Disallow renamings declaring tagged primitives

[Pierre-Marie de Rodat <derodat at adacore dot com>]

This patch implements the following SPARK rules from SPARK RM 6.1.1(3):

   A subprogram_renaming_declaration shall not declare a primitive operation of
   a tagged type.

------------
-- Source --
------------

--  renamings.ads

package Renamings with SPARK_Mode is
   type T is tagged null record;

   procedure Null_Proc (Obj : in out T) is null;

   procedure Proc_1 (Obj : in out T);
   procedure Proc_2 (Obj : in out T);

   function Func_1 (Obj : T) return Integer;
   function Func_2 (Obj : T) return Integer;

   function Func_3 return T;
   function Func_4 return T;

   procedure Error_1 (Obj : in out T) renames Null_Proc;             --  Error
   procedure Error_2 (Obj : in out T) renames Proc_1;                --  Error
   function  Error_3 (Obj : T) return Integer renames Func_1;        --  Error
   function  Error_4 return T renames Func_3;                        --  Error

   package Nested is
      procedure OK_1 (Obj : in out T) renames Null_Proc;             --  OK
      procedure OK_2 (Obj : in out T) renames Proc_1;                --  OK
      function  OK_3 (Obj : T) return Integer renames Func_1;        --  OK
      function  OK_4 return T renames Func_3;                        --  OK
   end Nested;
end Renamings;

--  renamings.adb

package body Renamings with SPARK_Mode is
   procedure Proc_1 (Obj : in out T) is begin null; end Proc_1;

   procedure Proc_2 (Obj : in out T) renames Proc_1;                 --  OK

   function Func_1 (Obj : T) return Integer is
   begin
      return 0;
   end Func_1;

   function Func_2 (Obj : T) return Integer renames Func_1;          --  OK

   function Func_3 return T is
      Result : T;
   begin
      return Result;
   end Func_3;

   function Func_4 return T renames Func_3;                          --  OK
end Renamings;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c renamings.adb
renamings.ads:15:39: subprogram renaming "Error_1" cannot declare primitive of
  type "T" (SPARK RM 6.1.1(3))
renamings.ads:16:39: subprogram renaming "Error_2" cannot declare primitive of
  type "T" (SPARK RM 6.1.1(3))
renamings.ads:17:47: subprogram renaming "Error_3" cannot declare primitive of
  type "T" (SPARK RM 6.1.1(3))
renamings.ads:18:31: subprogram renaming "Error_4" cannot declare primitive of
  type "T" (SPARK RM 6.1.1(3))

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

2017-11-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch8.adb (Analyze_Subprogram_Renaming): Ensure that a renaming
	declaration does not define a primitive operation of a tagged type for
	SPARK.
	(Check_SPARK_Primitive_Operation): New routine.

Attachment: difs
Description: Text document