This patch fixes the handling of overriding operations that have both an
explicit postcondition and an inherited classwide one.
Executing:
gnatmake -q -gnata post_class.adb
post_class
must yield:
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
failed inherited postcondition from the_package.ads:4
---
with The_Package; use The_Package;
procedure Post_Class is
X : D;
begin
Proc (X);
end Post_Class;
---
package The_Package is
type T is tagged null record;
function F (X : T) return Boolean is (True);
procedure Proc (X : in out T) with Post => True, post'class => F (X);
type D is new T with null record;
overriding function F (X : D) return Boolean is (False);
end The_Package;
---
package body The_Package is
procedure Proc (X : in out T) is
begin
null;
end Proc;
end The_Package;
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-09-06 Ed Schonberg <schonb...@adacore.com>
* einfo.ads, einfo.adb (Get_Classwwide_Pragma): New utility,
to retrieve the inherited classwide precondition/postcondition
of a subprogram.
* freeze.adb (Freeze_Entity): Use Get_Classwide_Pragma when
freezing a subprogram, to complete the generation of the
corresponding checking code.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 251783)
+++ einfo.adb (working copy)
@@ -7481,6 +7481,39 @@
return Empty;
end Get_Pragma;
+ --------------------------
+ -- Get_Classwide_Pragma --
+ --------------------------
+
+ function Get_Classwide_Pragma
+ (E : Entity_Id;
+ Id : Pragma_Id) return Node_Id
+ is
+ Item : Node_Id;
+ Items : Node_Id;
+
+ begin
+ Items := Contract (E);
+ if No (Items) then
+ return Empty;
+ end if;
+
+ Item := Pre_Post_Conditions (Items);
+
+ while Present (Item) loop
+ if Nkind (Item) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name_Unmapped (Item)) = Id
+ and then Class_Present (Item)
+ then
+ return Item;
+ else
+ Item := Next_Pragma (Item);
+ end if;
+ end loop;
+
+ return Empty;
+ end Get_Classwide_Pragma;
+
--------------------------------------
-- Get_Record_Representation_Clause --
--------------------------------------
Index: einfo.ads
===================================================================
--- einfo.ads (revision 251783)
+++ einfo.ads (working copy)
@@ -8295,6 +8295,12 @@
-- Test_Case
-- Volatile_Function
+ function Get_Classwide_Pragma
+ (E : Entity_Id;
+ Id : Pragma_Id) return Node_Id;
+ -- Examine Rep_Item chain to locate a classwide pre- or postcondition
+ -- of a primitive operation. Returns Empty if not present.
+
function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for a record
-- representation clause, and if found, returns it. Returns Empty
Index: freeze.adb
===================================================================
--- freeze.adb (revision 251781)
+++ freeze.adb (working copy)
@@ -1418,8 +1418,8 @@
New_Prag : Node_Id;
begin
- A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition);
- if Present (A_Pre) and then Class_Present (A_Pre) then
+ A_Pre := Get_Classwide_Pragma (Par_Prim, Pragma_Precondition);
+ if Present (A_Pre) then
New_Prag := New_Copy_Tree (A_Pre);
Build_Class_Wide_Expression
(Prag => New_Prag,
@@ -1436,9 +1436,9 @@
end if;
end if;
- A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
+ A_Post := Get_Classwide_Pragma (Par_Prim, Pragma_Postcondition);
- if Present (A_Post) and then Class_Present (A_Post) then
+ if Present (A_Post) then
New_Prag := New_Copy_Tree (A_Post);
Build_Class_Wide_Expression
(Prag => New_Prag,
