===================================================================
@@ -26277,9 +26277,10 @@
-----------------------------------
function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty;
+ Keep_Pragma_Id : Boolean := False) return Node_Id
is
Map : Elist_Id;
-- List containing the following mappings
@@ -26361,6 +26362,15 @@
& "for&#", N, Current_Scope);
end if;
+ -- Update type of function call node, which should be the same as
+ -- the function's return type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ then
+ Set_Etype (Parent (N), Etype (Entity (N)));
+ end if;
+
-- The whole expression will be reanalyzed
elsif Nkind (N) in N_Has_Etype then
@@ -26595,7 +26605,6 @@
Set_Analyzed (Check_Prag, False);
Set_Comes_From_Source (Check_Prag, False);
- Set_Class_Present (Check_Prag, False);
-- The tree of the original pragma may contain references to the
-- formal parameters of the related subprogram. At the same time
@@ -26621,16 +26630,21 @@
Nam := Prag_Nam;
end if;
- -- Convert the copy into pragma Check by correcting the name and adding
- -- a check_kind argument.
+ -- Unless Keep_Pragma_Id is True in order to keep the identifier of
+ -- the copied pragma in the newly created pragma, convert the copy into
+ -- pragma Check by correcting the name and adding a check_kind argument.
- Set_Pragma_Identifier
- (Check_Prag, Make_Identifier (Loc, Name_Check));
+ if not Keep_Pragma_Id then
+ Set_Class_Present (Check_Prag, False);
- Prepend_To (Pragma_Argument_Associations (Check_Prag),
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Nam)));
+ Set_Pragma_Identifier
+ (Check_Prag, Make_Identifier (Loc, Name_Check));
+ Prepend_To (Pragma_Argument_Associations (Check_Prag),
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Nam)));
+ end if;
+
-- Update the error message when the pragma is inherited
if Present (Inher_Id) then
@@ -27154,7 +27168,8 @@
end if;
New_Prag :=
- Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp);
+ Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp,
+ Keep_Pragma_Id => True);
Insert_After (Unit_Declaration_Node (Subp), New_Prag);
Preanalyze (New_Prag);
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -245,14 +245,18 @@
-- Perform preanalysis of pragma Test_Case
function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id;
- -- Transform a [refined] pre- or postcondition denoted by Prag into an
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty;
+ Keep_Pragma_Id : Boolean := False) return Node_Id;
+ -- Transform a pre- or [refined] postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
- -- the routine replaces the references of all formals of Inher_Id and
- -- primitive operations of its controlling type by references to the
- -- corresponding entities of Subp_Id and the descendant type.
+ -- the routine replaces the references of all formals of Inher_Id
+ -- and primitive operations of its controlling type by references
+ -- to the corresponding entities of Subp_Id and the descendant type.
+ -- Keep_Pragma_Id is True when the newly created pragma should be
+ -- in fact of the same kind as the source pragma Prag. This is used
+ -- in GNATprove_Mode to generate the inherited pre- and postconditions.
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
===================================================================
@@ -7618,6 +7618,10 @@
-- source, or because a Pre (resp. Post) aspect specification has been
-- broken into AND THEN sections. See Split_PPC for details.
+ -- In GNATprove mode, the inherited classwide pre- and postconditions
+ -- (suitably specialized for the specific type of the overriding
+ -- operation) are also in this list.
+
-- Contract_Test_Cases contains a collection of pragmas that correspond
-- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
-- list is in LIFO fashion.