ada/spark: all warnings, warn strict, style checks

* enable all common warnings through default value of CC_ADA_WARN
* treat warnings like errors through default value of CC_ADA_WARN_STRICT
* enable almost all style checks through default value of CC_ADA_WARN_STRICT
* style fixes for aes_cbc_4k
* disable strict warnings and style checks for libsparkcrypto and spark lib

Ref #3848

repos/base/mk/generic.mk

@@ -82,6 +82,16 @@ CUSTOM_ADA_FLAGS   ?= --RTS=$(ADA_RTS)
 CUSTOM_ADA_OPT     ?= $(CC_ADA_OPT) -gnatef
 CUSTOM_ADA_INCLUDE ?= -I- $(INCLUDES)
 
+#
+# The files generated by the binder would not pass our GNAT style checks
+# thus we handle them separately and disable style checks via compiler option
+# '-gnatyN'
+#
+b~%.ali b~%.o: b~%.adb
+	$(MSG_COMP)$@
+	$(VERBOSE)$(CUSTOM_ADA_CC) $(CUSTOM_ADA_FLAGS) $(CUSTOM_ADA_OPT) -gnatyN $(CUSTOM_ADA_INCLUDE) -c $<
+	$(VERBOSE)$(ALI2DEP) $(dir $<) $(ALL_INC_DIR) b~$*.ali
+
 %.ali %.o: %.adb
 	$(MSG_COMP)$@
 	$(VERBOSE)$(CUSTOM_ADA_CC) $(CUSTOM_ADA_FLAGS) $(CUSTOM_ADA_OPT) $(CUSTOM_ADA_INCLUDE) -c $<

repos/base/mk/global.mk

@@ -146,6 +146,12 @@ CC_WARN += -Wno-error=implicit-fallthrough
 CC_CXX_WARN_STRICT ?= -Wextra -Weffc++ -Werror -Wsuggest-override
 CC_CXX_WARN        ?= $(CC_WARN) $(CC_CXX_WARN_STRICT)
 
+#
+# Additional warnings for Ada/SPARK
+#
+CC_ADA_WARN_STRICT ?= -gnatwe -gnatyyBdSux
+CC_ADA_WARN        ?= -gnatwa $(CC_ADA_WARN_STRICT)
+
 #
 # Aggregate compiler options that are common for C and C++
 #
@@ -174,7 +180,9 @@ CC_OPT     += $(CC_OPT_PIC)
 #
 CC_CXX_OPT += $(CC_OPT) $(CC_CXX_WARN)
 CC_C_OPT   += $(CC_OPT)
-CC_ADA_OPT += $(filter-out -fno-builtin-cos -fno-builtin-sin -fno-builtin-cosf -fno-builtin-sinf ,$(CC_OPT)) -fexceptions
+CC_ADA_OPT += $(CC_ADA_WARN) -fexceptions
+CC_ADA_OPT += $(filter-out -fno-builtin-cos -fno-builtin-sin \
+                           -fno-builtin-cosf -fno-builtin-sinf ,$(CC_OPT))
 
 #
 # Enable C++11 by default

repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb

@@ -24,16 +24,20 @@ is
       type Padding_Type is array (Natural range <>) of Byte;
       type Block_Number_Text_Type is record
          Block_Number : Block_Number_Type;
-         Padding      : Padding_Type(1 .. 8);
+         Padding      : Padding_Type (1 .. 8);
       end record
       with Size => 128;
 
       Block_Number_Text : constant Block_Number_Text_Type :=
          (Block_Number => Block_Number, Padding => (others => 0));
 
-      type Block_Number_Plaintext_Base_Type is array (Natural range <>) of Byte;
+      type Block_Number_Plaintext_Base_Type
+      is array (Natural range <>) of Byte;
+
       subtype Block_Number_Plaintext_Index_Type is Natural range 1 .. 16;
-      subtype Block_Number_Plaintext_Type is Block_Number_Plaintext_Base_Type (Block_Number_Plaintext_Index_Type);
+
+      subtype Block_Number_Plaintext_Type
+      is Block_Number_Plaintext_Base_Type (Block_Number_Plaintext_Index_Type);
 
       function Convert is new Ada.Unchecked_Conversion
          (Block_Number_Text_Type, Block_Number_Plaintext_Type);
@@ -42,11 +46,15 @@ is
          (Natural, Byte, IV_Key_Base_Type);
 
       function Encrypt is new LSC.AES_Generic.Encrypt
-         (Natural, Byte, Block_Number_Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+         (Natural, Byte, Block_Number_Plaintext_Base_Type, Natural, Byte,
+          Ciphertext_Base_Type);
 
-  begin
+   begin
-     return Encrypt (Plaintext => Convert(Block_Number_Text),
+      return
-                     Key       => Enc_Key(Hash(Key), LSC.AES_Generic.L256)) (Natural'First .. Natural'First + 15);
+         Encrypt (
+            Plaintext => Convert (Block_Number_Text),
+            Key       => Enc_Key (Hash (Key), LSC.AES_Generic.L256))
+         (Natural'First .. Natural'First + 15);
    end Init_IV;
 
    procedure Encrypt (Key          :     Key_Type;
@@ -58,18 +66,18 @@ is
          (Natural, Byte, Key_Base_Type);
 
       procedure Encrypt is new LSC.AES_Generic.CBC.Encrypt
-         (Natural, Byte, Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+         (Natural, Byte, Plaintext_Base_Type, Natural, Byte,
+          Ciphertext_Base_Type);
 
-      IV : constant Ciphertext_Base_Type := Init_IV(Key, Block_Number);
+      IV : constant Ciphertext_Base_Type := Init_IV (Key, Block_Number);
    begin
 
       Encrypt (Plaintext  => Plaintext,
                IV         => IV,
-               Key        => Enc_Key(Key, LSC.AES_Generic.L256),
+               Key        => Enc_Key (Key, LSC.AES_Generic.L256),
                Ciphertext => Ciphertext);
    end Encrypt;
 
-
    procedure Decrypt (Key          :     Key_Type;
                       Block_Number :     Block_Number_Type;
                       Ciphertext   :     Ciphertext_Type;
@@ -79,12 +87,13 @@ is
          (Natural, Byte, Key_Base_Type);
 
       procedure Decrypt is new LSC.AES_Generic.CBC.Decrypt
-         (Natural, Byte, Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+         (Natural, Byte, Plaintext_Base_Type, Natural, Byte,
+          Ciphertext_Base_Type);
 
    begin
       Decrypt (Ciphertext => Ciphertext,
-               IV         => Init_IV(Key, Block_Number),
+               IV         => Init_IV (Key, Block_Number),
-               Key        => Dec_Key(Key, LSC.AES_Generic.L256),
+               Key        => Dec_Key (Key, LSC.AES_Generic.L256),
                Plaintext  => Plaintext);
    end Decrypt;
 

repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads

@@ -1,11 +1,11 @@
 package Aes_Cbc_4k with SPARK_Mode
 is
 
-   -- pragma Pure; -- not possible because libsparkcrypto is not known as pure
+   --  pragma Pure; -- not possible because libsparkcrypto is not known as pure
 
    type Byte              is mod 2**8 with Size => 8;
-   type Key_Base_type     is array (Natural range <>) of Byte;
+   type Key_Base_Type     is array (Natural range <>) of Byte;
-   subtype Key_Type       is Key_Base_type (1 .. 32);
+   subtype Key_Type       is Key_Base_Type (1 .. 32);
    type Block_Number_Type is mod 2**64 with Size => 64;
 
    type Plaintext_Base_Type is array (Natural range <>) of Byte;
@@ -22,7 +22,9 @@ is
                       Ciphertext   : out Ciphertext_Type)
    with Export,
       Convention    => C,
-      External_Name => "_ZN10Aes_cbc_4k7encryptERKNS_3KeyENS_12Block_numberERKNS_9PlaintextERNS_10CiphertextE";
+      External_Name =>
+         "_ZN10Aes_cbc_4k7encryptERKNS_3KeyENS_12Block_numberERKNS_" &
+         "9PlaintextERNS_10CiphertextE";
 
    procedure Decrypt (Key          :     Key_Type;
                       Block_Number :     Block_Number_Type;
@@ -30,6 +32,8 @@ is
                       Plaintext    : out Plaintext_Type)
    with Export,
       Convention    => C,
-      External_Name => "_ZN10Aes_cbc_4k7decryptERKNS_3KeyENS_12Block_numberERKNS_10CiphertextERNS_9PlaintextE";
+      External_Name =>
+         "_ZN10Aes_cbc_4k7decryptERKNS_3KeyENS_12Block_numberERKNS_" &
+         "10CiphertextERNS_9PlaintextE";
 
 end Aes_Cbc_4k;

repos/libports/lib/mk/libsparkcrypto.inc

@@ -78,3 +78,5 @@ vpath %.ads $(LSC_DIR)/shared/generic
 
 SHARED_LIB = yes
 CC_ADA_OPT += -gnatec=$(LSC_DIR)/../build/pragmas.adc -fPIC
+
+CC_ADA_WARN_STRICT =

repos/libports/lib/mk/spark.inc

@@ -9,3 +9,5 @@ ada_source_path: ada_object_path
 ada_object_path:
 	$(VERBOSE)mkdir -p $(ADA_RTS)
 	$(VERBOSE)echo $(ADA_RTS) > $(ADA_RTS)/ada_object_path
+
+CC_ADA_WARN_STRICT =

repos/libports/src/test/spark/lib/add_package.adb

@@ -1,14 +1,14 @@
-package body add_package is
+package body Add_Package is
 
-procedure Add (A : in Integer;
+   procedure Add (A : in Integer;
-               B : in Integer;
+                  B : in Integer;
-               R : out Integer)
+                  R : out Integer)
-is
+   is
-	procedure Ext_C_Print_Add (A, B : Integer; Result : out Integer);
+      procedure Ext_C_Print_Add (A, B : Integer; Result : out Integer);
-	pragma Import (C, Ext_C_Print_Add, "print_add");
+      pragma Import (C, Ext_C_Print_Add, "print_add");
-begin
+   begin
-    Ext_C_Print_Add (A, B, R);
+      Ext_C_Print_Add (A, B, R);
-    R := R + 1;
+      R := R + 1;
-end Add;
+   end Add;
 
-end add_package;
+end Add_Package;

repos/libports/src/test/spark/lib/add_package.ads

@@ -1,4 +1,6 @@
-package add_package is
+package Add_Package is
-    procedure Add(A: in Integer; B: in Integer; R: out Integer);
+   procedure Add (
-end add_package;
+      A : in Integer;
-
+      B : in Integer;
+      R : out Integer);
+end Add_Package;

repos/libports/src/test/spark/machinery.adb

@@ -9,7 +9,7 @@ package body Machinery is
 
    procedure Initialize (Machinery : out Machinery_Type) is
    begin
-      Machinery := ( Temperature => 25 );
+      Machinery := (Temperature => 25);
    end Initialize;
 
    function Temperature (Machinery : Machinery_Type) return Temperature_Type is

repos/libports/src/test/spark/machinery.ads

@@ -23,7 +23,7 @@ package Machinery is
           Convention    => C,
           External_Name => "_ZNK5Spark9Machinery11temperatureEv";
 
-   procedure Heat_up (Machinery : in out Machinery_Type)
+   procedure Heat_Up (Machinery : in out Machinery_Type)
      with Export,
           Convention    => C,
           External_Name => "_ZN5Spark9Machinery7heat_upEv";

repos/libports/src/test/spark/main.adb

@@ -1,25 +1,25 @@
 --
--- \brief  Ada test program
+--  \brief  Ada test program
--- \author Norman Feske
+--  \author Norman Feske
--- \date   2009-09-23
+--  \date   2009-09-23
 --
 
-with add_package;
+with Add_Package;
 
 --
--- Main program
+--  Main program
 --
 procedure main is
 
-	result : Integer;
+   result : Integer;
 
-	--
+   --
-	-- Declarations of external C functions
+   --  Declarations of external C functions
-	--
+   --
-	procedure ext_c_print_int(a : Integer);
+   procedure ext_c_print_int (a : Integer);
-	pragma import(C, ext_c_print_int, "print_int");
+   pragma Import (C, ext_c_print_int, "print_int");
 
 begin
-	add_package.Add(13, 14, result);
+   Add_Package.Add (13, 14, result);
-	ext_c_print_int(result);
+   ext_c_print_int (result);
 end main;

repos/libports/src/test/spark_exception/except.adb

@@ -1,9 +1,9 @@
 package body Except is
 
-    procedure Raise_Task
+   procedure Raise_Task
-    is
+   is
-    begin
+   begin
-        raise Program_Error;
+      raise Program_Error;
-    end Raise_Task;
+   end Raise_Task;
 
 end Except;

repos/libports/src/test/spark_exception/except.ads

@@ -1,5 +1,5 @@
 package Except is
 
-    procedure Raise_Task;
+   procedure Raise_Task;
 
 end Except;

repos/libports/src/test/spark_secondary_stack/stack.adb

@@ -4,115 +4,114 @@ package body Stack
 with SPARK_Mode
 is
 
-    pragma Suppress (All_Checks);
+   pragma Suppress (All_Checks);
 
-    ------------
+   ------------
-    -- Calloc --
+   -- Calloc --
-    ------------
+   ------------
 
-    procedure Calloc
+   procedure Calloc
       (Size : Integer)
       with SPARK_Mode => Off
-    is
+   is
-        procedure Print (Str : System.Address)
+      procedure Print (Str : System.Address)
-          with
+         with
-            Import,
+         Import,
-            Convention => C,
+         Convention => C,
-            External_Name => "print_stack";
+         External_Name => "print_stack";
 
-        Buf : Buffer := Alloc (Size) & Character'Val (0);
+         Buf : Buffer := Alloc (Size) & Character'Val (0);
-    begin
+   begin
-        Print (Buf'Address);
+      Print (Buf'Address);
-    end Calloc;
+   end Calloc;
 
-    procedure Ralloc
+   procedure Ralloc
-    is
+   is
-        R : constant Integer := 0;
+      R : constant Integer := 0;
-        B : Buffer := Recursive_Alloc (R);
+      B : Buffer := Recursive_Alloc (R);
-        pragma Unreferenced (B);
+      pragma Unreferenced (B);
-    begin
+   begin
-        null;
+      null;
-    end Ralloc;
+   end Ralloc;
 
-    -----------
+   -----------
-    -- Alloc --
+   -- Alloc --
-    -----------
+   -----------
 
-    function Alloc
+   function Alloc
       (Size : Integer)
-       return Buffer
+      return Buffer
-    is
+   is
-        Buf : constant Buffer (1 .. Size) := (others => '0');
+      Buf : constant Buffer (1 .. Size) := (others => '0');
-    begin
+   begin
-        return Buf;
+      return Buf;
-    end Alloc;
+   end Alloc;
 
-    function Recursive_Alloc (Round : Integer) return Buffer
+   function Recursive_Alloc (Round : Integer) return Buffer
-    is
+   is
-        procedure Print (R : Integer)
+      procedure Print (R : Integer)
-          with
+         with
-            Import,
+         Import,
-            Convention => C,
+         Convention => C,
-            External_Name => "print_recursion";
+         External_Name => "print_recursion";
 
-        Buf : constant Buffer (1 .. 256) := (others => '0');
+         Buf : constant Buffer (1 .. 256) := (others => '0');
-    begin
+   begin
-        Print (Round);
+      Print (Round);
-        if Round < 10 then
+      if Round < 10 then
-            return Buf & Recursive_Alloc (Round + 1);
+         return Buf & Recursive_Alloc (Round + 1);
-        else
+      else
-            return Buf;
+         return Buf;
-        end if;
+      end if;
-    end Recursive_Alloc;
+   end Recursive_Alloc;
 
-    procedure Salloc
+   procedure Salloc
-    is
+   is
-        S : constant Integer := 16;
+      S : constant Integer := 16;
-        B : Buffer := Stage_1 (S);
+      B : Buffer := Stage_1 (S);
-        pragma Unreferenced (B);
+      pragma Unreferenced (B);
-    begin
+   begin
-        Print_Stage (0);
+      Print_Stage (0);
-    end Salloc;
+   end Salloc;
 
-    function Stage_1 (
+   function Stage_1 (
-                      Size : Integer
+      Size : Integer
-                     ) return Buffer
+      ) return Buffer
-    is
+   is
-        Buf : Buffer (1 .. Size) := (others => '0');
+      Buf : Buffer (1 .. Size) := (others => '0');
-    begin
+   begin
-        Print_Stage (1);
+      Print_Stage (1);
-        declare
+      declare
-            Buf_2 : constant Buffer := Stage_2 (Size);
+         Buf_2 : constant Buffer := Stage_2 (Size);
-        begin
+      begin
-            Buf := Buf_2;
+         Buf := Buf_2;
-        end;
+      end;
-        return Buf;
+      return Buf;
-    end Stage_1;
+   end Stage_1;
 
+   function Stage_2 (
+      Size : Integer
+      ) return Buffer
+   is
+      Buf : Buffer (1 .. Size);
+   begin
+      Print_Stage (2);
+      declare
+         Buf2 : constant Buffer := Stage_3 (Size);
+      begin
+         Buf := Buf2;
+      end;
+      return Buf;
+   end Stage_2;
 
-    function Stage_2 (
+   function Stage_3 (
-                      Size : Integer
+      Size : Integer
-                     ) return Buffer
+      ) return Buffer
-    is
+   is
-        Buf : Buffer (1 .. Size);
+      Buf : constant Buffer (1 .. Size) := (others => '3');
-    begin
+   begin
-        Print_Stage (2);
+      Print_Stage (3);
-        declare
+      return Buf;
-            Buf2 : constant Buffer := Stage_3 (Size);
+   end Stage_3;
-        begin
-            Buf := Buf2;
-        end;
-        return Buf;
-    end Stage_2;
-
-    function Stage_3 (
-                      Size : Integer
-                     ) return Buffer
-    is
-        Buf : constant Buffer (1 .. Size) := (others => '3');
-    begin
-        Print_Stage (3);
-        return Buf;
-    end Stage_3;
 
 end Stack;

repos/libports/src/test/spark_secondary_stack/stack.ads

@@ -2,44 +2,30 @@ package Stack
 with SPARK_Mode
 is
 
-    type Buffer is array (Integer range <>) of Character;
+   type Buffer is array (Integer range <>) of Character;
 
-    procedure Calloc (
+   procedure Calloc (Size : Integer);
-                      Size : Integer
-                     );
 
-    procedure Ralloc;
+   procedure Ralloc;
 
-    function Alloc (
+   function Alloc (Size : Integer) return Buffer;
-                    Size : Integer
-                   ) return Buffer;
 
-    function Recursive_Alloc (
+   function Recursive_Alloc (Round : Integer) return Buffer;
-                              Round : Integer
-                             ) return Buffer;
 
-    procedure Salloc;
+   procedure Salloc;
 
-    function Stage_1 (
+   function Stage_1 (Size : Integer) return Buffer;
-                      Size : Integer
-                     ) return Buffer;
 
-    function Stage_2 (
+   function Stage_2 (Size : Integer) return Buffer;
-                      Size : Integer
-                     ) return Buffer;
 
-    function Stage_3 (
+   function Stage_3 (Size : Integer) return Buffer;
-                      Size : Integer
-                     ) return Buffer;
 
 private
 
-    procedure Print_Stage (
+   procedure Print_Stage (Stage : Integer)
-                           Stage : Integer
+   with
-                          )
+      Import,
-      with
+      Convention => C,
-        Import,
+      External_Name => "print_stage";
-        Convention => C,
-        External_Name => "print_stage";
 
 end Stack;