Commit 461778af authored by yoogx's avatar yoogx

* Various quickfix for SPARK2014, as supported by SPARK GPL 2015

        For issue #4
parent f485d15f
......@@ -29,8 +29,6 @@
-- --
------------------------------------------------------------------------------
with Ada.Synchronous_Task_Control;
with PolyORB_HI.Output;
with PolyORB_HI.Suspenders;
......@@ -41,11 +39,10 @@ package body PolyORB_HI.Background_Task is
use PolyORB_HI_Generated.Deployment;
use PolyORB_HI.Suspenders;
use Ada.Real_Time;
use Ada.Synchronous_Task_Control;
-----------------------
--------------------------
-- The_Background_Task --
-----------------------
-------------------------
task body The_Background_Task is
Error : Error_Kind;
......@@ -64,7 +61,7 @@ package body PolyORB_HI.Background_Task is
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
Block_Task (Entity);
delay until System_Startup_Time;
pragma Debug (Put_Line
......
......@@ -31,6 +31,8 @@
with PolyORB_HI.Output_Low_Level;
with PolyORB_HI.Suspenders;
pragma Elaborate_All (PolyORB_HI.Suspenders);
with Ada.Real_Time;
with System;
......@@ -164,7 +166,7 @@ package body PolyORB_HI.Output is
---------------------
procedure Unprotected_Put (Text : in String) is
Start_Time : Time renames PolyORB_HI.Suspenders.System_Startup_Time;
Start_Time : Time renames PolyORB_HI.Suspenders.System_Startup_Time;
Elapsed : Time_Span;
begin
if Start_Time = Time_First then
......
......@@ -29,19 +29,20 @@
-- --
------------------------------------------------------------------------------
with Ada.Synchronous_Task_Control;
pragma SPARK_Mode (Off);
with PolyORB_HI.Output;
with PolyORB_HI.Suspenders;
pragma Elaborate_All (PolyORB_HI.Suspenders);
package body PolyORB_HI.Periodic_Task is
use Ada.Real_Time;
use PolyORB_HI.Errors;
use PolyORB_HI.Output;
use Ada.Real_Time;
use PolyORB_HI.Suspenders;
use PolyORB_HI_Generated.Deployment;
use Ada.Synchronous_Task_Control;
Next_Deadline_Val : Time;
......@@ -64,7 +65,7 @@ package body PolyORB_HI.Periodic_Task is
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
Block_Task (Entity);
Next_Start := System_Startup_Time + Dispatch_Offset;
delay until Next_Start;
......@@ -96,6 +97,10 @@ package body PolyORB_HI.Periodic_Task is
-- Put_Line (Normal, "Lag: " +
-- Duration'Image (To_Duration (Next_Start - T)));
-- end if;
pragma Debug
(Put_Line
(Verbose,
"Periodic Task " + Entity_Image (Entity) + ": End of Cycle"));
delay until Next_Start;
Next_Start := Next_Start + Task_Period;
......
......@@ -28,9 +28,9 @@
-- (taste-users@lists.tuxfamily.org) --
-- --
------------------------------------------------------------------------------
pragma SPARK_Mode (Off);
-- Define a periodic task that executes a Job
with System;
with Ada.Real_Time;
with PolyORB_HI.Errors;
......
......@@ -30,6 +30,7 @@
------------------------------------------------------------------------------
with PolyORB_HI.Marshallers_G;
pragma Elaborate_All (PolyORB_HI.Marshallers_G);
with Interfaces;
package PolyORB_HI.Port_Type_Marshallers is
......
......@@ -29,19 +29,16 @@
-- --
------------------------------------------------------------------------------
with Ada.Synchronous_Task_Control;
with PolyORB_HI.Output;
with PolyORB_HI.Suspenders;
package body PolyORB_HI.Sporadic_Task is
use Ada.Real_Time;
use PolyORB_HI.Errors;
use PolyORB_HI.Output;
use PolyORB_HI_Generated.Deployment;
use PolyORB_HI.Suspenders;
use Ada.Real_Time;
use Ada.Synchronous_Task_Control;
Next_Deadline_Val : Time;
......@@ -68,8 +65,8 @@ package body PolyORB_HI.Sporadic_Task is
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
-- delay until System_Startup_Time;
Block_Task (Entity);
delay until System_Startup_Time;
pragma Debug (Put_Line
(Verbose,
......
......@@ -31,6 +31,7 @@
with Ada.Real_Time;
with PolyORB_HI.Marshallers_G;
pragma Elaborate_All (PolyORB_HI.Marshallers_G);
package PolyORB_HI.Time_Marshallers is
new PolyORB_HI.Marshallers_G (Ada.Real_Time.Time);
......@@ -29,6 +29,10 @@
-- --
------------------------------------------------------------------------------
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;
......@@ -39,6 +43,8 @@ with Ada.Unchecked_Conversion;
with GNAT.Sockets;
with PolyORB_HI.Output;
pragma Elaborate_All (PolyORB_HI.Output);
with PolyORB_HI.Messages;
with PolyORB_HI.Utils;
with PolyORB_HI_Generated.Naming;
......@@ -46,12 +52,7 @@ with PolyORB_HI_Generated.Transport;
-- Transport low-level service of PolyORB HI, using BSD sockets
package body PolyORB_HI.Transport_Low_Level
with Spark_Mode => Off
-- SPARK_Mode is disabled for this unit, it relies on OS-specific
-- libraries. We discard this unit for now.
is
package body PolyORB_HI.Transport_Low_Level is
pragma Suppress (Elaboration_Check, PolyORB_HI_Generated.Transport);
-- We do not want a pragma Elaborate_All to be implicitely
......
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