enable full warnings and style checks

jklmnn · Oct 30, 2018 · fec5945 · fec5945
1 parent bf27162
commit fec5945
Show file tree

Hide file tree

Showing 17 changed files with 190 additions and 150 deletions.
diff --git a/src/base32.adb b/src/base32.adb
@@ -15,18 +15,27 @@ is
       for C in Natural range 0 .. Chunks - 1 loop
          C5 := C * 5;
          C8 := C * 8;
-         Decoded (Decoded'First + C5) := Decode_1 (S (S'First + Integer (C8)),
-                                                   S (S'First + Integer (C8 + 1)));
-         Decoded (Decoded'First + C5 + 1) := Decode_2 (S (S'First + Integer (C8 + 1)),
-                                                       S (S'First + Integer (C8 + 2)),
-                                                       S (S'First + Integer (C8 + 3)));
-         Decoded (Decoded'First + C5 + 2) := Decode_3 (S (S'First + Integer (C8 + 3)),
-                                                       S (S'First + Integer (C8 + 4)));
-         Decoded (Decoded'First + C5 + 3) := Decode_4 (S (S'First + Integer (C8 + 4)),
-                                                       S (S'First + Integer (C8 + 5)),
-                                                       S (S'First + Integer (C8 + 6)));
-         Decoded (Decoded'First + C5 + 4) := Decode_5 (S (S'First + Integer (C8 + 6)),
-                                                       S (S'First + Integer (C8 + 7)));
+         Decoded (Decoded'First + C5) :=
+           Decode_1 (S (S'First + Integer (C8)),
+                     S (S'First + Integer (C8 + 1)));
+
+         Decoded (Decoded'First + C5 + 1) :=
+           Decode_2 (S (S'First + Integer (C8 + 1)),
+                     S (S'First + Integer (C8 + 2)),
+                     S (S'First + Integer (C8 + 3)));
+
+         Decoded (Decoded'First + C5 + 2) :=
+           Decode_3 (S (S'First + Integer (C8 + 3)),
+                     S (S'First + Integer (C8 + 4)));
+
+         Decoded (Decoded'First + C5 + 3) :=
+           Decode_4 (S (S'First + Integer (C8 + 4)),
+                     S (S'First + Integer (C8 + 5)),
+                     S (S'First + Integer (C8 + 6)));
+
+         Decoded (Decoded'First + C5 + 4) :=
+           Decode_5 (S (S'First + Integer (C8 + 6)),
+                     S (S'First + Integer (C8 + 7)));
       end loop;
       return Decoded;
    end Decode;
@@ -42,21 +51,37 @@ is
       Encoded : Base32_String (1 .. Chunks * 8) := (others => 'A');
    begin
       for C in Natural range 0 .. Chunks - 1 loop
-         pragma Loop_Invariant (for all C of Encoded => Valid_Base32_Character (C));
+         pragma Loop_Invariant (for all C of Encoded =>
+                                  Valid_Base32_Character (C));
          C5 := C * 5;
          C8 := C * 8;
-         Encoded (Encoded'First + C8) := Encode_1 (B (B'First + C5));
-         Encoded (Encoded'First + C8 + 1) := Encode_2 (B (B'First + C5),
-                                                       B (B'First + C5 + 1));
-         Encoded (Encoded'First + C8 + 2) := Encode_3 (B (B'First + C5 + 1));
-         Encoded (Encoded'First + C8 + 3) := Encode_4 (B (B'First + C5 + 1),
-                                                       B (B'First + C5 + 2));
-         Encoded (Encoded'First + C8 + 4) := Encode_5 (B (B'First + C5 + 2),
-                                                       B (B'First + C5 + 3));
-         Encoded (Encoded'First + C8 + 5) := Encode_6 (B (B'First + C5 + 3));
-         Encoded (Encoded'First + C8 + 6) := Encode_7 (B (B'First + C5 + 3),
-                                                       B (B'First + C5 + 4));
-         Encoded (Encoded'First + C8 + 7) := Encode_8 (B (B'First + C5 + 4));
+         Encoded (Encoded'First + C8) :=
+           Encode_1 (B (B'First + C5));
+
+         Encoded (Encoded'First + C8 + 1) :=
+           Encode_2 (B (B'First + C5),
+                     B (B'First + C5 + 1));
+
+         Encoded (Encoded'First + C8 + 2) :=
+           Encode_3 (B (B'First + C5 + 1));
+
+         Encoded (Encoded'First + C8 + 3) :=
+           Encode_4 (B (B'First + C5 + 1),
+                     B (B'First + C5 + 2));
+
+         Encoded (Encoded'First + C8 + 4) :=
+           Encode_5 (B (B'First + C5 + 2),
+                     B (B'First + C5 + 3));
+
+         Encoded (Encoded'First + C8 + 5) :=
+           Encode_6 (B (B'First + C5 + 3));
+
+         Encoded (Encoded'First + C8 + 6) :=
+           Encode_7 (B (B'First + C5 + 3),
+                     B (B'First + C5 + 4));
+
+         Encoded (Encoded'First + C8 + 7) :=
+           Encode_8 (B (B'First + C5 + 4));
       end loop;
       return Encoded;
    end Encode;
@@ -67,7 +92,7 @@ is
 
    function Decode_String (S : Base32_String) return String
    is
-      B : Buffer := Decode (S);
+      B : constant Buffer := Decode (S);
       Decoded_String : String (1 .. B'Length) := (others => Character'Val (0));
    begin
       for I in Decoded_String'Range loop

diff --git a/src/base32.ads b/src/base32.ads
@@ -2,40 +2,40 @@ with Interfaces;
 with LSC.Types;
 with LSC.Byte_Arrays;
 
--- @summary
--- Base32 encoder and decoder
+--  @summary
+--  Base32 encoder and decoder
 package Base32
   with SPARK_Mode
 is
 
-   -- Check if a character is in the Base32 alphabet
-   -- @param C Character to Check
-   -- @return True if C is in [a-zA-Z2-7]
+   --  Check if a character is in the Base32 alphabet
+   --  @param C Character to Check
+   --  @return True if C is in [a-zA-Z2-7]
    function Valid_Base32_Character
      (C : Character) return Boolean
    is
      (C in 'a' .. 'z' | 'A' .. 'Z' | '2' .. '7')
          with
            Depends => (Valid_Base32_Character'Result => C);
 
-   -- 8bit unsigned byte
+   --  8bit unsigned byte
    subtype Byte is LSC.Types.Byte;
-   -- Array of bytes
+   --  Array of bytes
    subtype Buffer is LSC.Byte_Arrays.Byte_Array_Type
      with
        Dynamic_Predicate => Buffer'Length mod 5 = 0;
 
-   -- Base32 string that can only contain [a-zA-Z2-7]
+   --  Base32 string that can only contain [a-zA-Z2-7]
    subtype Base32_String is String
      with
        Dynamic_Predicate =>
          Base32_String'Length mod 8 = 0 and
          (for all C of Base32_String =>
             Valid_Base32_Character (C));
 
-   -- Decode Base32 string into a byte array
-   -- @param S Valid Base32 string
-   -- @return Decoded byte array
+   --  Decode Base32 string into a byte array
+   --  @param S Valid Base32 string
+   --  @return Decoded byte array
    function Decode (S : Base32_String) return Buffer
      with
        Depends => (Decode'Result => S),
@@ -46,26 +46,26 @@ is
          Decode'Result'Length = S'Length * 5 / 8;
 
 
-   -- Encodes a byte array into a Base32 string
-   -- @param B byte array
-   -- @return Base32 string
+   --  Encodes a byte array into a Base32 string
+   --  @param B byte array
+   --  @return Base32 string
    function Encode (B : Buffer) return Base32_String
      with
        Depends => (Encode'Result => B),
        Pre => B'Length < Natural'Last / 8;
 
-   -- Decodes Base32 into ASCII
-   -- @param S Base32 string
-   -- @return String
+   --  Decodes Base32 into ASCII
+   --  @param S Base32 string
+   --  @return String
    function Decode_String (S : Base32_String) return String
      with
        Depends => (Decode_String'Result => S),
        Pre =>
          S'Length < Natural'Last / 5 and S'Length >= 8;
 
-   -- Encodes an ASCII string into Base32
-   -- @param ASCII String
-   -- @return Base32 string
+   --  Encodes an ASCII string into Base32
+   --  @param ASCII String
+   --  @return Base32 string
    function Encode_String (S : String) return Base32_String
      with
        Depends => (Encode_String'Result => S),

diff --git a/src/hmac.adb b/src/hmac.adb
@@ -25,8 +25,8 @@ is
       M    : LSC.SHA1.Message_Type (1 .. 1) := (others => MB);
       Hash : LSC.SHA1.Hash_Type;
 
-      Padded_Key : LSC.Byte_Arrays.Byte_Array_Type := Pad4.Pad (Key);
-      Padded_Msg : LSC.Byte_Arrays.Byte_Array_Type := Pad4.Pad (Msg);
+      Padded_Key : constant LSC.Byte_Arrays.Byte_Array_Type := Pad4.Pad (Key);
+      Padded_Msg : constant LSC.Byte_Arrays.Byte_Array_Type := Pad4.Pad (Msg);
    begin
       K (K'First .. K'First + (Padded_Key'Length / 4) - 1) :=
         LSC.Byte_Arrays.To_Word32_Array (Padded_Key);

diff --git a/src/hmac.ads b/src/hmac.ads
@@ -1,16 +1,16 @@
 with LSC.Byte_Arrays;
 
--- @summary
--- HMAC wrapper
+--  @summary
+--  HMAC wrapper
 --
--- @description
--- Wrapper around libsparkcryptos HMAC_SHA1.Authenticate that uses byte arrays
--- instead of 32bit word arrays
+--  @description
+--  Wrapper around libsparkcryptos HMAC_SHA1.Authenticate that uses byte arrays
+--  instead of 32bit word arrays
 package HMAC
 with SPARK_Mode
 is
 
-   -- Byte array of length 20
+   --  Byte array of length 20
    subtype HMAC_Type is LSC.Byte_Arrays.Byte_Array_Type (1 .. 20);
 
    function SHA1

diff --git a/src/lsc-byte_arrays-pad.ads b/src/lsc-byte_arrays-pad.ads
@@ -1,8 +1,8 @@
 
--- @summary
--- Zero right padding of byte arrays
+--  @summary
+--  Zero right padding of byte arrays
 --
--- @param Padding Block size to which padding should be applied
+--  @param Padding Block size to which padding should be applied
 generic
    Padding : LSC.Byte_Arrays.Natural_Index;
 package LSC.Byte_Arrays.Pad is

diff --git a/src/lsc-byte_arrays.adb b/src/lsc-byte_arrays.adb
@@ -29,7 +29,8 @@ is
      (B : Byte_Array_Type)
       return LSC.Types.Word32_Array_Type
    is
-      W : LSC.Types.Word32_Array_Type (1 .. LSC.Types.Index (B'Length / 4)) := (others => 0);
+      W : LSC.Types.Word32_Array_Type (1 .. LSC.Types.Index (B'Length / 4)) :=
+        (others => 0);
       Offset : Natural_Index;
    begin
       for I in W'Range loop

diff --git a/src/lsc-byte_arrays.ads b/src/lsc-byte_arrays.ads
@@ -1,21 +1,21 @@
 with LSC.Types;
 use all type LSC.Types.Index;
 
--- @summary
--- Extension of libsparkcryptos types by a byte array of unconstrained size
+--  @summary
+--  Extension of libsparkcryptos types by a byte array of unconstrained size
 package LSC.Byte_Arrays
 with SPARK_Mode
 is
 
-   -- Natural index type
+   --  Natural index type
    subtype Natural_Index is Natural range Natural'First .. Natural'Last - 1;
 
-   -- Unconstrained byte array
+   --  Unconstrained byte array
    type Byte_Array_Type is array (Natural_Index range <>) of LSC.Types.Byte;
 
-   -- Converts a LSC 32bit word array into a byte array
-   -- @param W32 LSC 32bit word array
-   -- @return byte array
+   --  Converts a LSC 32bit word array into a byte array
+   --  @param W32 LSC 32bit word array
+   --  @return byte array
    function To_Byte_Array
      (W32 : LSC.Types.Word32_Array_Type)
       return Byte_Array_Type
@@ -24,9 +24,9 @@ is
        Pre => W32'Length <= LSC.Types.Index'Last,
        Post => To_Byte_Array'Result'Length = 4 * W32'Length;
 
-   -- Converts a byte array into a LSC 32bit word array
-   -- @param B byte array
-   -- @return LSC 32bit word array
+   --  Converts a byte array into a LSC 32bit word array
+   --  @param B byte array
+   --  @return LSC 32bit word array
    function To_Word32_Array
      (B : Byte_Array_Type)
       return LSC.Types.Word32_Array_Type
@@ -42,23 +42,23 @@ is
    subtype Byte_Array32_Type is Byte_Array_Type (1 .. 4);
    subtype Byte_Array64_Type is Byte_Array_Type (1 .. 8);
 
-   -- Converts LSC 32bit byte array into a 4 byte long byte array
-   -- @param B LSC Byte_Array32
-   -- @return Byte array of length 4
+   --  Converts LSC 32bit byte array into a 4 byte long byte array
+   --  @param B LSC Byte_Array32
+   --  @return Byte array of length 4
    function Convert_Byte_Array
      (B : LSC.Types.Byte_Array32_Type)
       return Byte_Array32_Type is
-     (Byte_Array32_Type' (1 => B (0),
-                          2 => B (1),
-                          3 => B (2),
-                          4 => B (3)))
+     (Byte_Array32_Type'(1 => B (0),
+                         2 => B (1),
+                         3 => B (2),
+                         4 => B (3)))
      with
        Depends => (Convert_Byte_Array'Result => B),
        Inline;
 
-   -- Converts a 4 byte long byte array into an LSC 32bit byte array
-   -- @param B Byte array of length 4
-   -- @return LSC Byte_Array32
+   --  Converts a 4 byte long byte array into an LSC 32bit byte array
+   --  @param B Byte array of length 4
+   --  @return LSC Byte_Array32
    function Convert_Byte_Array
      (B : Byte_Array32_Type)
       return LSC.Types.Byte_Array32_Type is
@@ -70,30 +70,30 @@ is
        Depends => (Convert_Byte_Array'Result => B),
        Inline;
 
-   -- Converts LSC 64bit byte array into a 8 byte long byte array
-   -- @param B LSC Byte_Array64
-   -- @return Byte array of length 8
+   --  Converts LSC 64bit byte array into a 8 byte long byte array
+   --  @param B LSC Byte_Array64
+   --  @return Byte array of length 8
    function Convert_Byte_Array
      (B : LSC.Types.Byte_Array64_Type)
       return Byte_Array64_Type is
-     (Byte_Array64_Type' (1 => B (0), 2 => B (1),
-                          3 => B (2), 4 => B (3),
-                          5 => B (4), 6 => B (5),
-                          7 => B (6), 8 => B (7)))
+     (Byte_Array64_Type'(1 => B (0), 2 => B (1),
+                         3 => B (2), 4 => B (3),
+                         5 => B (4), 6 => B (5),
+                         7 => B (6), 8 => B (7)))
      with
        Depends => (Convert_Byte_Array'Result => B),
        Inline;
 
-   -- Converts a 8 byte long byte array into an LSC 64bit byte array
-   -- @param B Byte array of length 8
-   -- @return LSC Byte_Array64
+   --  Converts a 8 byte long byte array into an LSC 64bit byte array
+   --  @param B Byte array of length 8
+   --  @return LSC Byte_Array64
    function Convert_Byte_Array
      (B : Byte_Array64_Type)
       return LSC.Types.Byte_Array64_Type is
-     (LSC.Types.Byte_Array64_Type' (0 => B (1), 1 => B (2),
-                                    2 => B (3), 3 => B (4),
-                                    4 => B (5), 5 => B (6),
-                                    6 => B (7), 7 => B (8)))
+     (LSC.Types.Byte_Array64_Type'(0 => B (1), 1 => B (2),
+                                   2 => B (3), 3 => B (4),
+                                   4 => B (5), 5 => B (6),
+                                   6 => B (7), 7 => B (8)))
      with
        Depends => (Convert_Byte_Array'Result => B),
        Inline;