Commit ec1408b8 authored by yoogx's avatar yoogx

* Solve various mis-placement of SPARK_Mode pragma, for

      compatibility with older GNAT
parent 11858d59
......@@ -48,9 +48,9 @@ with POHICDRIVER_IP;
-- This package provides support for the TCP_IP device driver as
-- defined in the tcp_protocol.aadl AADLv2 model.
package body PolyORB_HI_Drivers_Native_TCP_IP
with SPARK_Mode => Off
is
package body PolyORB_HI_Drivers_Native_TCP_IP is
pragma SPARK_Mode (Off);
pragma Suppress (Elaboration_Check, PolyORB_HI_Generated.Transport);
-- We do not want a pragma Elaborate_All to be implicitely
......
......@@ -35,6 +35,7 @@ with PolyORB_HI.Streams;
with PolyORB_HI.Utils;
package PolyORB_HI_Drivers_Native_TCP_IP is
pragma SPARK_Mode (Off);
use PolyORB_HI.Errors;
use PolyORB_HI_Generated.Deployment;
......
......@@ -16,7 +16,7 @@ pragma Locking_Policy (Ceiling_Locking); -- D.13.1
-- target: the code has Spark_Mode disabled in some occurences,
-- without this pragma the code would be rejected.
pragma Spark_Mode (On);
--pragma Spark_Mode (On);
--------------------------------------------------------------------------------
-- The following define restrictions to be supported by the
......
......@@ -29,6 +29,8 @@
-- --
------------------------------------------------------------------------------
pragma SPARK_MOde (Off);
with PolyORB_HI.Output_Low_Level;
with PolyORB_HI.Suspenders;
pragma Elaborate_All (PolyORB_HI.Suspenders);
......@@ -60,7 +62,6 @@ package body PolyORB_HI.Output is
end Output_Lock;
package body Output_Lock is
pragma SPARK_MOde (Off);
protected Lock is
-- This lock has been defined to guarantee thread-safe output
......
......@@ -31,6 +31,8 @@
-- Debug facility of PolyORB HI
pragma SPARK_Mode (Off);
with PolyORB_HI.Streams;
package PolyORB_HI.Output is
......
......@@ -29,6 +29,8 @@
-- --
------------------------------------------------------------------------------
pragma SPARK_Mode (Off);
package PolyORB_HI.Output_Low_Level is
procedure New_Line;
......
......@@ -29,6 +29,8 @@
-- --
------------------------------------------------------------------------------
pragma SPARK_Mode (Off);
with Interfaces.C;
with System;
......@@ -39,7 +41,6 @@ package body PolyORB_HI.Output_Low_Level is
---------
procedure Put (S : String)
with SPARK_Mode => Off
-- SPARK_Mode is distabled because of the Address attribute
is
procedure C_Write
......
......@@ -29,12 +29,11 @@
-- --
------------------------------------------------------------------------------
pragma SPARK_Mode (Off);
with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;
pragma Elaborate_All (Ada.Synchronous_Task_Control);
package body PolyORB_HI.Suspenders is
pragma SPARK_Mode (Off);
use Ada.Real_Time;
......@@ -62,7 +61,7 @@ package body PolyORB_HI.Suspenders is
---------------------
procedure Suspend_Forever
with SPARK_Mode => Off
-- with SPARK_Mode => Off
-- XXX: delay until not supported in GNATProve GPL2014
is
begin
......
......@@ -30,6 +30,7 @@
------------------------------------------------------------------------------
-- This package implements routines to suspend application tasks
pragma SPARK_Mode (Off);
with Ada.Real_Time;
......
......@@ -37,6 +37,9 @@ with PolyORB_HI.Streams;
with PolyORB_HI_Generated.Deployment;
package PolyORB_HI.Transport_Low_Level is
pragma SPARK_Mode (Off);
-- SPARK_Mode is disabled for this unit, it relies on OS-specific
-- libraries. We discard this unit for now.
pragma Elaborate_Body;
......
......@@ -29,10 +29,6 @@
-- --
------------------------------------------------------------------------------
pragma SPARK_Mode (Off);
-- SPARK_Mode is disabled for this unit, it relies on OS-specific
-- libraries. We discard this unit for now.
with Ada.Synchronous_Task_Control;
with Ada.Exceptions;
with Ada.Real_Time;
......@@ -54,6 +50,10 @@ with PolyORB_HI_Generated.Transport;
package body PolyORB_HI.Transport_Low_Level is
pragma SPARK_Mode (Off);
-- SPARK_Mode is disabled for this unit, it relies on OS-specific
-- libraries. We discard this unit for now.
pragma Suppress (Elaboration_Check, PolyORB_HI_Generated.Transport);
-- We do not want a pragma Elaborate_All to be implicitely
-- generated for Transport.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment