[Ada] Handling of inherited and explicit postconditions

[Arnaud Charlet <charlet at adacore dot com>]

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.

Attachment: difs
Description: Text document