gnat 4.4.5 generates surprising code when enabling FP checks

["Markus Schöpflin" <no.spam@spam.spam>]

The behaviour described below has been observed for gcc 4.3.5, 4.4.5, and 
gnatpro 6.3.2, maybe someone here has any insight on this.

Given the following short code snippet:

procedure FLOAT_CHECKS is
    F1, F2, F3 : SHORT_FLOAT;
begin
    for I in 1..100_000 loop
       for J in 1..10_000 loop
          F1 := SHORT_FLOAT(I);  -- *
          F2 := SHORT_FLOAT(J);  -- *
          F3 := F1 * F2;         -- *
       end loop;
    end loop;
end FLOAT_CHECKS;

Compiling with gnatmake -O3 -gnatDG -gnatVa float_checks.adb gives the 
following intermediate code for the lines marked with '*':

          f1 := short_float({i});
          f2 := short_float({j});
          [constraint_error when
            not boolean!($system__fat_sflt__attr_short_float.
              system__fat_sflt__attr_short_float__valid (f1'
              unrestricted_access, xF => 0))
            "invalid data"]
          [constraint_error when
            not boolean!($system__fat_sflt__attr_short_float.
              system__fat_sflt__attr_short_float__valid (f2'
              unrestricted_access, xF => 0))
            "invalid data"]
          [constraint_error when
            not boolean!($system__fat_sflt__attr_short_float.
              system__fat_sflt__attr_short_float__valid (f1 * f2'
              unrestricted_access, xF => 0))
            "invalid data"]
          f3 := f1 * f2;

So far so good. What really surprises me is that in the resulting assembler 
code the last multiplication is actually performed twice, the disassembled 
object code looks like this (for the last check and multiplication only):

  8048ed6:       d9 45 e4                flds   -0x1c(%ebp)
  8048ed9:       d8 4d e0                fmuls  -0x20(%ebp)
  8048edc:       c7 44 24 04 00 00 00    movl   $0x0,0x4(%esp)
  8048ee3:       00
  8048ee4:       89 3c 24                mov    %edi,(%esp)
  8048ee7:       d9 5d dc                fstps  -0x24(%ebp)
  8048eea:       e8 61 fc ff ff          call   8048b50 
<system__fat_sflt__attr_short_float__valid@plt>
  8048eef:       84 c0                   test   %al,%al
  8048ef1:       74 2c                   je     8048f1f 
<_ada_float_checks+0xaf>
  8048ef3:       83 c3 01                add    $0x1,%ebx
  8048ef6:       d9 45 e4                flds   -0x1c(%ebp)
  8048ef9:       81 fb 11 27 00 00       cmp    $0x2711,%ebx
  8048eff:       d8 4d e0                fmuls  -0x20(%ebp)
  8048f02:       dd d8                   fstp   %st(0)

Is the second multiplication to be expected? Does anybody know if there is 
an optimizer option which would eliminate the second multiplication?

Regards,
Markus