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 <[email protected]>
* 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.
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 254797)
+++ sem_ch8.adb (working copy)
@@ -59,6 +59,7 @@
with Sem_Dist; use Sem_Dist;
with Sem_Elab; use Sem_Elab;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sem_Type; use Sem_Type;
@@ -1924,6 +1925,10 @@
-- have one. Otherwise the subtype of Sub's return profile must
-- exclude null.
+ procedure Check_SPARK_Primitive_Operation (Subp_Id : Entity_Id);
+ -- Ensure that a SPARK renaming denoted by its entity Subp_Id does not
+ -- declare a primitive operation of a tagged type (SPARK RM 6.1.1(3)).
+
procedure Freeze_Actual_Profile;
-- In Ada 2012, enforce the freezing rule concerning formal incomplete
-- types: a callable entity freezes its profile, unless it has an
@@ -2519,6 +2524,52 @@
end if;
end Check_Null_Exclusion;
+ -------------------------------------
+ -- Check_SPARK_Primitive_Operation --
+ -------------------------------------
+
+ procedure Check_SPARK_Primitive_Operation (Subp_Id : Entity_Id) is
+ Prag : constant Node_Id := SPARK_Pragma (Subp_Id);
+ 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)
+ then
+ return;
+
+ -- Nothing to do when the subprogram is not a primitive operation
+
+ elsif not Is_Primitive (Subp_Id) then
+ return;
+ end if;
+
+ Typ := Find_Dispatching_Type (Subp_Id);
+
+ -- Nothing to do when the subprogram is a primitive operation of an
+ -- untagged type.
+
+ if No (Typ) then
+ return;
+ end if;
+
+ -- At this point a renaming declaration introduces a new primitive
+ -- operation for a tagged type.
+
+ Error_Msg_Node_2 := Typ;
+ Error_Msg_NE
+ ("subprogram renaming & cannot declare primitive for type & "
+ & "(SPARK RM 6.1.1(3))", N, Subp_Id);
+ end Check_SPARK_Primitive_Operation;
+
---------------------------
-- Freeze_Actual_Profile --
---------------------------
@@ -2899,7 +2950,7 @@
-- Set SPARK mode from current context
- Set_SPARK_Pragma (New_S, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma (New_S, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (New_S);
Rename_Spec := Find_Corresponding_Spec (N);
@@ -3009,13 +3060,16 @@
Generate_Definition (New_S);
New_Overloaded_Entity (New_S);
- if Is_Entity_Name (Nam)
- and then Is_Intrinsic_Subprogram (Entity (Nam))
+ if not (Is_Entity_Name (Nam)
+ and then Is_Intrinsic_Subprogram (Entity (Nam)))
then
- null;
- else
Check_Delayed_Subprogram (New_S);
end if;
+
+ -- Verify that a SPARK renaming does not declare a primitive
+ -- operation of a tagged type.
+
+ Check_SPARK_Primitive_Operation (New_S);
end if;
-- There is no need for elaboration checks on the new entity, which may
@@ -3205,10 +3259,9 @@
elsif Requires_Overriding (Old_S)
or else
- (Is_Abstract_Subprogram (Old_S)
- and then Present (Find_Dispatching_Type (Old_S))
- and then
- not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
+ (Is_Abstract_Subprogram (Old_S)
+ and then Present (Find_Dispatching_Type (Old_S))
+ and then not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
then
Error_Msg_N
("renamed entity cannot be subprogram that requires overriding "
