Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright <simon@pushface.org>]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> OTOH, I didn't realize that you had a dispatching call. In that case,
> the precondition is supposed to just be the Pre'Class for A, which is
> stronger that A or B which a direct call would use. Probably GNAT
> dispatched and then checked the precondition. Technically, that's
> wrong (although I would have a hard time caring, the reason for the
> stronger precondition on dispatching calls is to allow analysis
> without knowing the actual tag, it doesn't have anything to do with
> correctness).

I think that the rule that GNAT appears to be breaking is 6.6.1(38)[1]?

I've constructed an example where GNAT's behaviour results in caller
code that used to work (with checks enabled) no longer working,
depending on the actual type for a classwide (an access-to-classwide,
as might be used if say the application logger could be changed at run
time):

with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO; use Ada.Text_IO;

procedure Conditions is

   package A_Pack is
      type T is tagged null record;
      not overriding
      procedure P (This : T; Var : Integer) is null
        with Pre'Class => Var >= 1;
   end A_Pack;

   package B_Pack is
      type T is new A_Pack.T with null record;
      overriding
      procedure P (This : T; Var : Integer) is null
        with Pre'Class => Var >= 0;                -- widening
   end B_Pack;

   package C_Pack is
      type T is new A_Pack.T with null record;
      overriding
      procedure P (This : T; Var : Integer) is null;
   end C_Pack;

begin

   declare
      O : access A_Pack.T'Class;
   begin
      O := new B_Pack.T;
      Put_Line ("passing 0 to an actual B_Pack.T");
      O.P (0);
      Put_Line ("success.");
      O := new C_Pack.T;
      Put_Line ("passing 0 to an actual C_Pack.T");
      O.P (0);
      Put_Line ("success.");
   exception
      when E : others =>
         Put_Line (Exception_Information (E));
   end;

end Conditions;

and the output is

$ ./conditions 
passing 0 to an actual B_Pack.T
success.
passing 0 to an actual C_Pack.T
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed inherited precondition from conditions.adb:10


[1] http://www.ada-auth.org/standards/12aarm/html/AA-6-1-1.html#p38