Integer Conversion

main.adb

with Types; use Types;
with Test;

procedure Main
   with SPARK_Mode
is
   function Data return Bytes is (255, 255);
   Result : U16;
begin
   Result := Test.Convert_To_U16 (Data);
end Main;

test.adb

package body Test
   with SPARK_Mode
is

   function Convert_To_U16 (Buffer : Bytes) return U16
   is
      Value : U16 := 0;
      T : Byte;
   begin
      for i in Natural range 0 .. (U16'Size / 8) - 1 loop
         T := Buffer (Buffer'Last - i);
         pragma Assert (2**16 - 1 = U16'Last);
         pragma Assert (Value + 255 * 256**i <= U16'Last);
         pragma Assert (U16 (T) <= 255);
         pragma Assert (Value + U16 (T) * 256**i <= U16'Last);
         Value := Value + U16 (T) * U16 (256**i);
      end loop;
      return Value;
   end Convert_To_U16;

end Test;

test.ads

with Types; use Types;

package Test
   with SPARK_Mode
is

   function Convert_To_U16 (Buffer : Bytes) return U16
     with
       Pre => U16'Size rem 8 = 0 and then Buffer'Length = U16'Size / 8;

end Test;

types.ads

package Types is

   type Byte is mod 2**8;
   type Bytes is array (Positive range <>) of Byte;

   type U16 is range 0 .. 2**16 - 1 with Size => 16;

end Types;