Permalink
Browse files

Enabled SPARK_Mode

Added global pragma SPARK_Mode.
Added pragma SPARK_Mode(Off) to files that cannot be compiled
in SPARK mode.

Signed-off-by: German Rivera <jgrivera67@gmail.com>
  • Loading branch information...
jgrivera67 committed Oct 31, 2016
1 parent f207d2a commit 7faa7c4e6bc401a41ee06af2b07f16cd090f7a77
Showing with 38 additions and 8 deletions.
  1. +1 −0 SVD/nxp_kinetis_k64f/mk64f12-sim.ads
  2. +1 −1 building_blocks/cpu_specific/arm_cortex_m0plus/microcontroller-cpu_specific.ads
  3. +1 −0 building_blocks/mcu_specific/nxp_kinetis_k64f/networking-layer2-build_local_mac_address.adb
  4. +1 −0 building_blocks/portable/color_led.adb
  5. +1 −0 building_blocks/portable/color_led.ads
  6. +1 −0 building_blocks/portable/networking/networking-layer2.adb
  7. +1 −0 building_blocks/portable/networking/networking-layer2.ads
  8. +1 −0 building_blocks/portable/networking/networking-layer3_ipv4.adb
  9. +1 −0 building_blocks/portable/networking/networking-layer3_ipv4.ads
  10. +1 −0 building_blocks/portable/networking/networking.adb
  11. +1 −1 building_blocks/portable/networking/networking.ads
  12. +1 −0 building_blocks/portable/serial_console.adb
  13. +2 −0 drivers/board_specific/frdm_k64f/networking/ethernet_phy_mdio_driver-board_specific_private.ads
  14. +1 −0 ...rd_specific/frdm_k64f/networking/networking-layer2-ethernet_mac_driver-board_specific_private.ads
  15. +2 −0 drivers/board_specific/frdm_k64f/uart_driver-board_specific_private.ads
  16. +1 −0 drivers/board_specific/frdm_kl25z/uart_driver-board_specific_private.ads
  17. +1 −0 drivers/mcu_specific/nxp_kinetis_k64f/crc_32_accelerator_driver.adb
  18. +1 −0 drivers/mcu_specific/nxp_kinetis_k64f/gpio_driver-mcu_specific_private.ads
  19. +1 −0 drivers/mcu_specific/nxp_kinetis_k64f/networking/ethernet_phy_mdio_driver.adb
  20. +1 −0 ...ecific/nxp_kinetis_k64f/networking/networking-layer2-ethernet_mac_driver-mcu_specific_private.ads
  21. +1 −0 drivers/mcu_specific/nxp_kinetis_k64f/networking/networking-layer2-ethernet_mac_driver.adb
  22. +6 −5 drivers/mcu_specific/nxp_kinetis_k64f/pin_mux_driver-mcu_specific_private.ads
  23. +1 −0 drivers/mcu_specific/nxp_kinetis_k64f/uart_driver.adb
  24. +1 −0 drivers/mcu_specific/nxp_kinetis_kl25z/gpio_driver-mcu_specific_private.ads
  25. +1 −0 drivers/mcu_specific/nxp_kinetis_kl25z/pin_mux_driver-mcu_specific_private.ads
  26. +1 −0 drivers/mcu_specific/nxp_kinetis_kl25z/uart_driver.adb
  27. +1 −0 drivers/portable/networking/ethernet_phy_mdio_driver.ads
  28. +1 −0 drivers/portable/uart_driver.ads
  29. +1 −0 frdm_k64f_iot_stack/iot_stack_demo.adb
  30. +1 −0 frdm_k64f_iot_stack/iot_stack_demo.ads
  31. +1 −1 gnat_pragmas.adc
@@ -29,6 +29,7 @@ with System;
-- System Integration Module
package MK64F12.SIM is
pragma Preelaborate;
pragma SPARK_Mode (Off);
---------------
-- Registers --
@@ -109,7 +109,7 @@ package Microcontroller.CPU_Specific is
SCR : Word;
CCR : Word;
Reserved1 : Word;
SHP : Words_Array (1 .. 2);
SHP : Words_Array_Type (1 .. 2);
SHCSR : Word;
end record with Volatile, Size => 16#28# * Byte'Size;
@@ -30,6 +30,7 @@ with Kinetis_K64F.SIM;
separate (Networking.Layer2)
procedure Build_Local_Mac_Address (
Mac_Address : out Ethernet_Mac_Address_Type) is
pragma SPARK_Mode (Off);
Reg_Value : Word;
begin
--
@@ -29,6 +29,7 @@ with Color_Led.Board_Specific_Private;
with Runtime_Logs;
package body Color_Led is
pragma SPARK_Mode (Off);
use Color_Led.Board_Specific_Private;
type Rgb_Color_Type is record
@@ -83,6 +83,7 @@ package Color_Led is
--
private
pragma SPARK_Mode (Off);
use Gpio_Driver;
use Ada.Synchronous_Task_Control;
@@ -34,6 +34,7 @@ with Number_Conversion_Utils;
with Atomic_Utils;
package body Networking.Layer2 is
pragma SPARK_Mode (Off);
use Networking.Layer2.Ethernet_Mac_Driver;
use Networking.Layer3_IPv4;
use Networking.Layer3_IPv6;
@@ -139,6 +139,7 @@ package Networking.Layer2 is
-- ** --
private
pragma SPARK_Mode (Off);
--
-- Network packet receiver task type
@@ -31,6 +31,7 @@ with Number_Conversion_Utils;
with Atomic_Utils;
package body Networking.Layer3_IPv4 is
pragma SPARK_Mode (Off);
use Number_Conversion_Utils;
use Networking.Layer2;
use Atomic_Utils;
@@ -139,6 +139,7 @@ package Networking.Layer3_IPv4 is
with Pre => Initialized;
private
pragma SPARK_Mode (Off);
--
-- Number of entries for the IPv4 ARP cache table
@@ -28,6 +28,7 @@
with Ada.Real_Time;
package body Networking is
pragma SPARK_Mode (Off);
----------------------------
-- Dequeue_Network_Packet --
@@ -300,7 +300,7 @@ package Networking is
(Tx_Packet_Pool : in out Net_Tx_Packet_Pool_Type);
private
pragma SPARK_Mode (Off);
use Microcontroller.Arm_Cortex_M;
use Ada.Synchronous_Task_Control;
@@ -33,6 +33,7 @@ with Ada.Synchronous_Task_Control;
with System;
package body Serial_Console is
pragma SPARK_Mode (Off);
use Devices.MCU_Specific;
use Ada.Synchronous_Task_Control;
use Number_Conversion_Utils;
@@ -29,6 +29,8 @@
-- @summary Board-specific Ethernet PHY MDIO driver private declarations
--
private package Ethernet_Phy_Mdio_Driver.Board_Specific_Private is
pragma SPARK_Mode (Off);
--
-- Array of Ethernet PHY MDIO device constant objects to be placed on
-- flash:
@@ -32,6 +32,7 @@ with Pin_Mux_Driver;
-- @summary Board-specific Ethernet MAC driver private declarations
--
private package Networking.Layer2.Ethernet_Mac_Driver.Board_Specific_Private is
pragma SPARK_Mode (Off);
use Networking.Layer2.Ethernet_Mac_Driver.MCU_Specific_Private;
use Pin_Mux_Driver;
@@ -29,6 +29,8 @@
-- @summary Board-specific UART driver private declarations
--
private package Uart_Driver.Board_Specific_Private is
pragma SPARK_Mode (Off);
--
-- Array of UART device objects to be placed on flash:
--
@@ -29,6 +29,7 @@
-- @summary Board-specific UART driver private declarations
--
private package Uart_Driver.Board_Specific_Private is
pragma SPARK_Mode (Off);
--
-- Array of UART device objects to be placed on flash:
@@ -30,6 +30,7 @@ with Kinetis_K64F.CRC;
with Interfaces.Bit_Types;
package body Crc_32_Accelerator_Driver is
pragma SPARK_Mode (Off);
use MK64F12.SIM;
use Kinetis_K64F;
use Interfaces.Bit_Types;
@@ -32,6 +32,7 @@ with Devices.MCU_Specific;
--
private package Gpio_Driver.MCU_Specific_Private is
pragma Preelaborate;
pragma SPARK_Mode (Off);
use Devices.MCU_Specific;
--
@@ -35,6 +35,7 @@ with Runtime_Logs;
-- K64F MCU
--
package body Ethernet_Phy_Mdio_Driver is
pragma SPARK_Mode (Off);
use Ethernet_Phy_Mdio_Driver.Board_Specific_Private;
use Microcontroller;
use MK64F12;
@@ -29,6 +29,7 @@ with Pin_Mux_Driver;
with System;
private package Networking.Layer2.Ethernet_Mac_Driver.MCU_Specific_Private is
pragma SPARK_Mode (Off);
use Pin_Mux_Driver;
use System;
@@ -43,6 +43,7 @@ with System;
with MPU_Driver;
package body Networking.Layer2.Ethernet_Mac_Driver is
pragma SPARK_Mode (Off);
use Networking.Layer2.Ethernet_Mac_Driver.MCU_Specific_Private;
use Networking.Layer2.Ethernet_Mac_Driver.Board_Specific_Private;
use MK64F12.SIM;
@@ -30,15 +30,16 @@
--
private package Pin_Mux_Driver.MCU_Specific_Private is
pragma Preelaborate;
pragma SPARK_Mode (Off);
--
-- Table of pointers to the PORT registers for each GPIO port
--
Ports : constant array (Pin_Port_Type) of access PORT.Registers_Type :=
(PIN_PORT_A => PORT.PORTA_Registers'Access,
PIN_PORT_B => PORT.PORTB_Registers'Access,
PIN_PORT_C => PORT.PORTC_Registers'Access,
PIN_PORT_D => PORT.PORTD_Registers'Access,
PIN_PORT_E => PORT.PORTE_Registers'Access);
(PIN_PORT_A => PORT.PortA_Registers'Access,
PIN_PORT_B => PORT.PortB_Registers'Access,
PIN_PORT_C => PORT.PortC_Registers'Access,
PIN_PORT_D => PORT.PortD_Registers'Access,
PIN_PORT_E => PORT.PortE_Registers'Access);
end Pin_Mux_Driver.MCU_Specific_Private;
@@ -31,6 +31,7 @@ with Uart_Driver.Board_Specific_Private;
with Microcontroller.Arm_Cortex_M;
package body Uart_Driver is
pragma SPARK_Mode (Off);
use Ada.Interrupts;
use Uart_Driver.Board_Specific_Private;
use Microcontroller.Arm_Cortex_M;
@@ -32,6 +32,7 @@ with Devices.MCU_Specific;
--
private package Gpio_Driver.MCU_Specific_Private is
pragma Preelaborate;
pragma SPARK_Mode (Off);
use Devices.MCU_Specific;
--
@@ -27,6 +27,7 @@
private package Pin_Mux_Driver.MCU_Specific_Private is
pragma Preelaborate;
pragma SPARK_Mode (Off);
--
-- Table of pointers to the PORT registers for each GPIO port
@@ -31,6 +31,7 @@ with System;
with Uart_Driver.Board_Specific_Private;
package body Uart_Driver is
pragma SPARK_Mode (Off);
use Ada.Interrupts;
use Uart_Driver.Board_Specific_Private;
@@ -96,6 +96,7 @@ package Ethernet_Phy_Mdio_Driver is
--
private
pragma SPARK_Mode (Off);
use Pin_Mux_Driver;
use Ada.Synchronous_Task_Control;
@@ -97,6 +97,7 @@ package Uart_Driver is
--
private
pragma SPARK_Mode (Off);
use Interfaces.Bit_Types;
use Microcontroller_Clocks;
use Pin_Mux_Driver;
@@ -35,6 +35,7 @@ with Networking.Layer3_IPv4;
with Devices.MCU_Specific;
package body IoT_Stack_Demo is
pragma SPARK_Mode (Off);
use Ada.Real_Time;
use Interfaces;
use Networking.Layer2;
@@ -39,6 +39,7 @@ package IoT_Stack_Demo is
with Pre => not Initialized;
private
pragma SPARK_Mode (Off);
use Ada.Synchronous_Task_Control;
type IoT_Stack_Demo_Type is limited record
@@ -2,7 +2,7 @@ pragma Warnings (Off, """Constraint_Error"" may call Last_Chance_Handler");
pragma Warnings (Off, "pragma Restrictions (No_Exception_Propagation) in effect");
pragma Profile (Ravenscar);
pragma Ada_2012;
--pragma SPARK_Mode (On);
pragma SPARK_Mode (On);
pragma Assertion_Policy (Check);
pragma Restrictions (No_Recursion);
pragma Restrictions (No_Allocators);

0 comments on commit 7faa7c4

Please sign in to comment.