Class wide preconditions: error in GNAT implementation?

[ytomino <aghia05@gmail.com>]

Hello.
I read https://groups.google.com/d/topic/comp.lang.ada/03cKrGghF2Y/discussion and recall a related question.

See below example:

package preconds is
   package Tools is
      function Write_In_Expr (S : String) return Boolean; -- Put_Line (S) and return True
   end Tools;
   package As is
      type A is tagged null record;
      procedure foo (Object : A) -- empty body
         with Pre'Class => Tools.Write_In_Expr ("A, in!"),
              Post'Class => Tools.Write_In_Expr ("A, out!");
   end As;
   package Bs is
      type B is new As.A with null record;
      overriding procedure foo (Object : B) -- empty body
         with Pre'Class  => Tools.Write_In_Expr ("B, in!"), -- [*]
              Post'Class => Tools.Write_In_Expr ("B, out!");
   end Bs;
end preconds;

with preconds; use preconds;
procedure precondmain is
   x : access As.A'Class := new Bs.B;
begin
   As.foo (x.all); -- dispatching call as A'Class
end precondmain;

% gnatmake -gnat2012 -gnata precondmain.adb
% ./precondmain
B, in!
B, out!
A, out!

And change [*] to Pre'Class => Tools.Write_In_Expr ("B, in!") and False,

% gnatmake -gnat2012 -gnata precondmain.adb
% ./precondmain                            
B, in!
A, in!
B, out!
A, out!

It seems that the preconditions were evaluated as pragma Assert (B'Pre'Class and then A'Pre'Class);

By the way, AARM 6.1.1 38.a/3-b/3 says

> Ramification: For a dispatching call, we are talking about the Pre'Class(es) that apply to the subprogram that the dispatching call is resolving to, not the Pre'Class(es) for the subprogram that is ultimately dispatched to. The class-wide precondition of the resolved call is necessarily the same or stronger than that of the invoked call. For a statically bound call, these are the same; for an access-to-subprogram, (which has no class-wide preconditions of its own), we check the class-wide preconditions of the invoked routine. 

>Implementation Note: These rules imply that logically, class-wide preconditions of routines must be checked at the point of call (other than for access-to-subprogram calls, which must be checked in the body, probably using a wrapper). Specific preconditions that might be called with a dispatching call or via an access-to-subprogram value must be checked inside of the subprogram body. In contrast, the postcondition checks always need to be checked inside the body of the routine. Of course, an implementation can evaluate all of these at the point of call for statically bound calls if the implementation uses wrappers for dispatching bodies and for 'Access values.

I think(hope), this two lines mean only A'Pre'Class should be evaluated in this case.

B'Pre'Class should not be evaluated in this case. Isn't it?

P.S. dmd (D language compiler) had same error. Its discussion may help for reference.
http://d.puremagic.com/issues/show_bug.cgi?id=6857