SPARK and Width/Image attributes

General
1

I’ve noticed that SPARK doesn’t seem to know the properties of the Width attribute, or there is something that I’m missing.

with Ada.Text_IO;

procedure Image_Width with SPARK_Mode is

   function Image (Number : Integer) return String
     with Post => Image'Result'Length <= Integer'Width;

   function Image (Number : Integer) return String is
   begin
      return Integer'Image (Number);
   end Image;

begin
   Ada.Text_IO.Put_Line (Image (123));
   Ada.Text_IO.Put_Line (Integer'Last'Image'Length'Image);
   Ada.Text_IO.Put_Line (Integer'First'Image'Length'Image);

end Image_Width;

When it is run:

 123
 11
 11

When passed to gnatprove:

alr exec -- gnatprove -P /home/mgr/tmp/image_width/image_width.gpr -j0 -u image_width.adb -cargs -gnatef 

QSocketNotifier: Can only be used with threads started with QThread
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...

/home/mgr/tmp/image_width/src/image_width.adb:6:19: medium: postcondition might fail
    6 |     with Post => Image'Result'Length <= Integer'Width;
      |                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Summary logged in /home/mgr/tmp/image_width/obj/development/gnatprove/gnatprove.out

I’m using gnatprove from Alire (14.1.1).

Shouldn’t SPARK know the properties of the Image and Width arguments? Isn’t my postcondition a direct consequent of the definition of those attributes?

Moreover, if I simply add + 1, that is, changing:

     with Post => Image'Result'Length <= Integer'Width;

to

     with Post => Image'Result'Length <= Integer'Width + 1;

Then gnatprove gives its green light. Is this a bug in gnatprove or is there some special case where the length of Integer’Image can be 12?

2

A related question is which are the preconditions and postconditions of attributes, as the Ada reference manual doesn’t seem to define them and there’s no available source specification to look for them.

For example:

with Ada.Text_IO;

procedure Image_Width with SPARK_Mode is

   function Value (Number : String) return Integer
   with
     Pre =>
       Number'Length <= Integer'Width
       and then (for all C of Number => C in '0' .. '9');

   function Value (Number : String) return Integer is
   begin
      return Integer'Value (Number);
   end Value;

   My_Number : constant Integer := Value ("123");
begin
   Ada.Text_IO.Put_Line (My_Number'Image);

end Image_Width;

alr exec -- gnatprove -P /home/mgr/tmp/image_width/image_width.gpr -j0 -u image_width.adb -cargs -gnatef 

QSocketNotifier: Can only be used with threads started with QThread
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...

/home/mgr/tmp/image_width/src/image_width.adb:13:21: medium: precondition might fail
   13 |      return Integer'Value (Number);
      |             ~~~~~~~^~~~~~~~~~~~~~
Summary logged in /home/mgr/tmp/image_width/obj/development/gnatprove/gnatprove.out

I cannot image what is that precondition, which isn’t already guaranteed by the Value function preconditions.