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 <[email protected]>
* sem_ch8.adb (Check_SPARK_Primitive_Operation): Enable the check in
instantiations.
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;
