[Ada] Class-wide pre/postconditions

[Arnaud Charlet <charlet at adacore dot com>]

Class-wide pre- and postconditions of a primitive operation of some type T
apply to the overriding operation of any descendant of T. Therefore, any
mention of of a formal of type T in the expression for the condition must be
interpreted as a being of type  T'class. A similar rule applies to access
paremeters. This patch adds the required type conversion to such references.
The following must execute quietly:

    gnatmake -q -gnatws -gnat12 -gnata r
    r
--
with System.Assertions; use System.Assertions;
with P1.Q1;
procedure R is
   Thing1 : P1.T1;
   Thing2 : P1.Q1.T2;
   Thing3 : aliased P1.Q1.T2;

begin
 P1.P (Thing1);

   begin
     P1.Q1.P (Thing2);
     raise Program_Error;   --  should not reach here
   exception
     when Assert_Failure  => null;
   end;

   --  Test access parameters.

   begin
     P1.Q1.P2 (Thing3'access);
     raise Program_Error;   --  should not reach here
   exception
     when Assert_Failure  => null;
   end;
end R;
---
package P1 is
  type T1 is tagged record
     Value : Integer := 16;
  end record;

  procedure P(X : in out T1) with
    Pre'Class => Precond(X'Old),
    Post'Class => Postcond(X);

  procedure P2 (X : access T1)
  with
    Post'Class => X.all.Value > 0;
  
  function Precond(X : T1) return Boolean;
  function Postcond(X : T1) return Boolean;
end P1;
---
package body P1 is

  procedure P(X : in out T1)  is begin null; end;

  procedure P2 (X : access T1) is
  begin
    X.Value := X.Value + 3;
 end P2;

  function Precond(X : T1) return Boolean is begin return True; end;
  function Postcond(X : T1) return Boolean is begin return X.Value < 20; end;
end P1;
---
package P1.Q1 is
  type T2 is new T1 with null record;

  overriding
    procedure P(X : in out T2);

  overriding
    procedure P2 (X : access T2);
end P1.Q1;
---
package body P1.Q1 is

 --  Overriding procedures that violate inherited postcondition.

 procedure P (X : in out T2) is begin X.Value := 25; end;

 procedure P2 (X : access T2) is
  begin
    X.Value := -X.Value + 3;
 end P2;
end P1.Q1;

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

2011-09-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_PPC_In_Decl_Part): for a class-wide
	condition, a reference to a controlling formal must be interpreted
	as having the class-wide type (or an access to such) so that the
	inherited condition can be properly applied to any overriding
	operation (see ARM12 6.6.1 (7)).

Attachment: difs
Description: Text document