diff mbox series

[Ada] Disallow renamings declaring tagged primitives

Message ID 20171116102405.GA48698@adacore.com
State New
Headers show
Series [Ada] Disallow renamings declaring tagged primitives | expand

Commit Message

Pierre-Marie de Rodat Nov. 16, 2017, 10:24 a.m. UTC 
This patch enables the check which ensures that a subprogram renaming does not
declare a primitive operation of a tagged type in instantiations.

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

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

	* sem_ch8.adb (Check_SPARK_Primitive_Operation): Enable the check in
	instantiations.
diff mbox series

Patch

Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb	(revision 254804)
+++ sem_ch8.adb	(working copy)
@@ -2533,16 +2533,11 @@ 
          Typ  : Entity_Id;
 
       begin
-         --  Nothing to do when the subprogram appears within an instance
-
-         if In_Instance then
-            return;
-
          --  Nothing to do when the subprogram is not subject to SPARK_Mode On
          --  because this check applies to SPARK code only.
 
-         elsif not (Present (Prag)
-                     and then Get_SPARK_Mode_From_Annotation (Prag) = On)
+         if not (Present (Prag)
+                  and then Get_SPARK_Mode_From_Annotation (Prag) = On)
          then
             return;