From f3eaeb08ef9ef0d0df25fafef5b5baf10322f420 Mon Sep 17 00:00:00 2001 From: Martin Stein Date: Sun, 29 Sep 2019 01:49:02 +0200 Subject: [PATCH] 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 | 10 + repos/base/mk/global.mk | 10 +- repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb | 37 ++-- repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads | 14 +- repos/libports/lib/mk/libsparkcrypto.inc | 2 + repos/libports/lib/mk/spark.inc | 2 + .../src/test/spark/lib/add_package.adb | 24 +-- .../src/test/spark/lib/add_package.ads | 10 +- repos/libports/src/test/spark/machinery.adb | 2 +- repos/libports/src/test/spark/machinery.ads | 2 +- repos/libports/src/test/spark/main.adb | 26 +-- .../src/test/spark_exception/except.adb | 10 +- .../src/test/spark_exception/except.ads | 2 +- .../src/test/spark_secondary_stack/stack.adb | 189 +++++++++--------- .../src/test/spark_secondary_stack/stack.ads | 42 ++-- 15 files changed, 202 insertions(+), 180 deletions(-) diff --git a/repos/base/mk/generic.mk b/repos/base/mk/generic.mk index d551ac205b..0531c08d58 100644 --- a/repos/base/mk/generic.mk +++ b/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 $< diff --git a/repos/base/mk/global.mk b/repos/base/mk/global.mk index 6ff6ab2abd..808989f248 100644 --- a/repos/base/mk/global.mk +++ b/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 diff --git a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb b/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb index 09fa3e53d3..5903978be7 100644 --- a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb +++ b/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 - return Encrypt (Plaintext => Convert(Block_Number_Text), - Key => Enc_Key(Hash(Key), LSC.AES_Generic.L256)) (Natural'First .. Natural'First + 15); + begin + return + 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), - Key => Dec_Key(Key, LSC.AES_Generic.L256), + IV => Init_IV (Key, Block_Number), + Key => Dec_Key (Key, LSC.AES_Generic.L256), Plaintext => Plaintext); end Decrypt; diff --git a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads b/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads index 8bf8386bd0..62a65aadeb 100644 --- a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads +++ b/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; - subtype Key_Type is Key_Base_type (1 .. 32); + type Key_Base_Type is array (Natural range <>) of Byte; + 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; diff --git a/repos/libports/lib/mk/libsparkcrypto.inc b/repos/libports/lib/mk/libsparkcrypto.inc index 336e909f31..151ef2c6c6 100644 --- a/repos/libports/lib/mk/libsparkcrypto.inc +++ b/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 = diff --git a/repos/libports/lib/mk/spark.inc b/repos/libports/lib/mk/spark.inc index 6366a34540..9a51f63ada 100644 --- a/repos/libports/lib/mk/spark.inc +++ b/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 = diff --git a/repos/libports/src/test/spark/lib/add_package.adb b/repos/libports/src/test/spark/lib/add_package.adb index 7974654d3a..d2c4d36c33 100644 --- a/repos/libports/src/test/spark/lib/add_package.adb +++ b/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; - B : in Integer; - R : out Integer) -is - procedure Ext_C_Print_Add (A, B : Integer; Result : out Integer); - pragma Import (C, Ext_C_Print_Add, "print_add"); -begin - Ext_C_Print_Add (A, B, R); - R := R + 1; -end Add; + procedure Add (A : in Integer; + B : in Integer; + R : out Integer) + is + procedure Ext_C_Print_Add (A, B : Integer; Result : out Integer); + pragma Import (C, Ext_C_Print_Add, "print_add"); + begin + Ext_C_Print_Add (A, B, R); + R := R + 1; + end Add; -end add_package; +end Add_Package; diff --git a/repos/libports/src/test/spark/lib/add_package.ads b/repos/libports/src/test/spark/lib/add_package.ads index 08b4ec6d18..675a7baec9 100644 --- a/repos/libports/src/test/spark/lib/add_package.ads +++ b/repos/libports/src/test/spark/lib/add_package.ads @@ -1,4 +1,6 @@ -package add_package is - procedure Add(A: in Integer; B: in Integer; R: out Integer); -end add_package; - +package Add_Package is + procedure Add ( + A : in Integer; + B : in Integer; + R : out Integer); +end Add_Package; diff --git a/repos/libports/src/test/spark/machinery.adb b/repos/libports/src/test/spark/machinery.adb index 3875e0a1bf..1e334c51d7 100644 --- a/repos/libports/src/test/spark/machinery.adb +++ b/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 diff --git a/repos/libports/src/test/spark/machinery.ads b/repos/libports/src/test/spark/machinery.ads index 4f8b5f6d55..51367756e7 100644 --- a/repos/libports/src/test/spark/machinery.ads +++ b/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"; diff --git a/repos/libports/src/test/spark/main.adb b/repos/libports/src/test/spark/main.adb index 517ff81806..db8c18bf1d 100644 --- a/repos/libports/src/test/spark/main.adb +++ b/repos/libports/src/test/spark/main.adb @@ -1,25 +1,25 @@ -- --- \brief Ada test program --- \author Norman Feske --- \date 2009-09-23 +-- \brief Ada test program +-- \author Norman Feske +-- \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 - -- - procedure ext_c_print_int(a : Integer); - pragma import(C, ext_c_print_int, "print_int"); + -- + -- Declarations of external C functions + -- + procedure ext_c_print_int (a : Integer); + pragma Import (C, ext_c_print_int, "print_int"); begin - add_package.Add(13, 14, result); - ext_c_print_int(result); + Add_Package.Add (13, 14, result); + ext_c_print_int (result); end main; diff --git a/repos/libports/src/test/spark_exception/except.adb b/repos/libports/src/test/spark_exception/except.adb index ecc9a6157b..a551185d5b 100644 --- a/repos/libports/src/test/spark_exception/except.adb +++ b/repos/libports/src/test/spark_exception/except.adb @@ -1,9 +1,9 @@ package body Except is - procedure Raise_Task - is - begin - raise Program_Error; - end Raise_Task; + procedure Raise_Task + is + begin + raise Program_Error; + end Raise_Task; end Except; diff --git a/repos/libports/src/test/spark_exception/except.ads b/repos/libports/src/test/spark_exception/except.ads index 0234d6ba0d..dfcc1cb5d4 100644 --- a/repos/libports/src/test/spark_exception/except.ads +++ b/repos/libports/src/test/spark_exception/except.ads @@ -1,5 +1,5 @@ package Except is - procedure Raise_Task; + procedure Raise_Task; end Except; diff --git a/repos/libports/src/test/spark_secondary_stack/stack.adb b/repos/libports/src/test/spark_secondary_stack/stack.adb index a063951510..69b52af8a3 100644 --- a/repos/libports/src/test/spark_secondary_stack/stack.adb +++ b/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 - procedure Print (Str : System.Address) - with - Import, - Convention => C, - External_Name => "print_stack"; + is + procedure Print (Str : System.Address) + with + Import, + Convention => C, + External_Name => "print_stack"; - Buf : Buffer := Alloc (Size) & Character'Val (0); - begin - Print (Buf'Address); - end Calloc; + Buf : Buffer := Alloc (Size) & Character'Val (0); + begin + Print (Buf'Address); + end Calloc; - procedure Ralloc - is - R : constant Integer := 0; - B : Buffer := Recursive_Alloc (R); - pragma Unreferenced (B); - begin - null; - end Ralloc; + procedure Ralloc + is + R : constant Integer := 0; + B : Buffer := Recursive_Alloc (R); + pragma Unreferenced (B); + begin + null; + end Ralloc; - ----------- - -- Alloc -- - ----------- + ----------- + -- Alloc -- + ----------- - function Alloc + function Alloc (Size : Integer) - return Buffer - is - Buf : constant Buffer (1 .. Size) := (others => '0'); - begin - return Buf; - end Alloc; + return Buffer + is + Buf : constant Buffer (1 .. Size) := (others => '0'); + begin + return Buf; + end Alloc; - function Recursive_Alloc (Round : Integer) return Buffer - is - procedure Print (R : Integer) - with - Import, - Convention => C, - External_Name => "print_recursion"; + function Recursive_Alloc (Round : Integer) return Buffer + is + procedure Print (R : Integer) + with + Import, + Convention => C, + External_Name => "print_recursion"; - Buf : constant Buffer (1 .. 256) := (others => '0'); - begin - Print (Round); - if Round < 10 then - return Buf & Recursive_Alloc (Round + 1); - else - return Buf; - end if; - end Recursive_Alloc; + Buf : constant Buffer (1 .. 256) := (others => '0'); + begin + Print (Round); + if Round < 10 then + return Buf & Recursive_Alloc (Round + 1); + else + return Buf; + end if; + end Recursive_Alloc; - procedure Salloc - is - S : constant Integer := 16; - B : Buffer := Stage_1 (S); - pragma Unreferenced (B); - begin - Print_Stage (0); - end Salloc; + procedure Salloc + is + S : constant Integer := 16; + B : Buffer := Stage_1 (S); + pragma Unreferenced (B); + begin + Print_Stage (0); + end Salloc; - function Stage_1 ( - Size : Integer - ) return Buffer - is - Buf : Buffer (1 .. Size) := (others => '0'); - begin - Print_Stage (1); - declare - Buf_2 : constant Buffer := Stage_2 (Size); - begin - Buf := Buf_2; - end; - return Buf; - end Stage_1; + function Stage_1 ( + Size : Integer + ) return Buffer + is + Buf : Buffer (1 .. Size) := (others => '0'); + begin + Print_Stage (1); + declare + Buf_2 : constant Buffer := Stage_2 (Size); + begin + Buf := Buf_2; + end; + return Buf; + 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 ( - 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_3 ( - Size : Integer - ) return Buffer - is - Buf : constant Buffer (1 .. Size) := (others => '3'); - begin - Print_Stage (3); - return Buf; - end Stage_3; + 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; diff --git a/repos/libports/src/test/spark_secondary_stack/stack.ads b/repos/libports/src/test/spark_secondary_stack/stack.ads index ea60571564..c108d69d4d 100644 --- a/repos/libports/src/test/spark_secondary_stack/stack.ads +++ b/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 ( - Size : Integer - ); + procedure Calloc (Size : Integer); - procedure Ralloc; + procedure Ralloc; - function Alloc ( - Size : Integer - ) return Buffer; + function Alloc (Size : Integer) return Buffer; - function Recursive_Alloc ( - Round : Integer - ) return Buffer; + function Recursive_Alloc (Round : Integer) return Buffer; - procedure Salloc; + procedure Salloc; - function Stage_1 ( - Size : Integer - ) return Buffer; + function Stage_1 (Size : Integer) return Buffer; - function Stage_2 ( - Size : Integer - ) return Buffer; + function Stage_2 (Size : Integer) return Buffer; - function Stage_3 ( - Size : Integer - ) return Buffer; + function Stage_3 (Size : Integer) return Buffer; private - procedure Print_Stage ( - Stage : Integer - ) - with - Import, - Convention => C, - External_Name => "print_stage"; + procedure Print_Stage (Stage : Integer) + with + Import, + Convention => C, + External_Name => "print_stage"; end Stack;