===================================================================
@@ -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 --
--------------------------------------
===================================================================
@@ -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
===================================================================
@@ -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,
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 <schonberg@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.