[Ada] Ada 2012 predicate checks on (in-) out parameters

[Arnaud Charlet <charlet at adacore dot com>]

RM 3.2.4 (23/3) stipulates that predicates are checked on out and in-out
by-reference parameters on return from a call. If the call is to a primitive
of the type the predicate call is inserted in the postcondition subprogram.
However, if the call is to an inherited operation, the check must be performed
explicitly on exit from the call.

Executing the following:
gnatmake -q -gnata -gnat12 main.adb
main

---

must yield:

   raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at main.adb:6

---
with Derived; use Derived;
procedure Main is
   A : T0 := (X => 0);
   B : T0 := (X => A.X);
begin
   P (A);
   B := A;
end Main;
---
with Parent; use Parent;
package Derived is
  type T0 is new T with null record with Dynamic_Predicate => T0.X = 0;
  procedure Change (x : in out T0);
end Derived;
---
package Parent is
  type T is tagged record
    X : Integer;
  end record;

  procedure P (A : in out T);
end Parent;
---
package body Parent is
   procedure P (A : in out T) is
   begin
      A.X := 1;
   end P;
end Parent;

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-04-22  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch6.adb (Expand_Actuals): If the call is to an
	inherited operation and the actual is a by-reference type with
	predicates, add predicate call to post-call actions.
	* sem_util.adb (Is_Inherited_Operation_For_Type): Fix coding
	error: a type declaration has a defining identifier, not an Etype.
	* sem_res.adb: Restore code removed because of above error.

Attachment: difs
Description: Text document