View Change

3 comments:

• File debug/hw-print.adb:

  • Patch Set #1, Line 48: Format_String'First <= Format_String'Last and

    First precondition seems not needed (anymore)?

  • Patch Set #1, Line 108: Arg.Padding := Arg.Padding * 10 + Char_To_UInt (Format_String (Pos));

    GNATprove is right to complain here about potential overflows. We
    don't know what string we will be called with, e.g. if it starts with
    "%111111111111" it would overflow.

    So we need to explicitly check

       if Arg.Padding <= Natural'Last / 10 - 9 then

    I would say, we can just ignore errors.

    To prove this, we need to know that Char_To_UInt() returns at most 9.
    Three ways come to mind:

    Make it an expression function (this way callers know exactly what it does):

       function Char_To_UInt (Item : in Character) return Natural
       is
          (Character'Pos (Item) - Character'Pos ('0'))
       with
          Pre => Item in '0' .. '9';

    Constrain the return type, e.g.

       subtype Decimal_Digit is Natural range 0 .. 9;

    Or add a post condition:

       Post => Char_To_UInt'Result in 0 .. 9;

  • Patch Set #1, Line 207: pragma loop_invariant (Item_C < Item_B ** String_Begin);

    Maybe we have to make it explicit that `Item_B` doesn't change in […]

    Meh, whatever, even with that and without overflowing Word64 in the exponentiation,
    I don't get anything useful.

    Making the code more explicit shouldn't hurt:

       for Pos in reverse Word64_String_Range loop
          Output_String (Pos) := ...
          ...
          String_Begin := Pos;
          exit when Item_C = 0;
       end loop;

To view, visit change 37530. To unsubscribe, or for help writing mail filters, visit settings.