Commit 0f4972a2 authored by yoogx's avatar yoogx

* Implement a "+" operator for string for concatenation, as

          the regular "&" operator for concatenation is not (yet)
          supported by GNATProve as of version GPL2013
parent a3094c89
......@@ -51,7 +51,7 @@ package body Ping is
begin
Order := not Order;
Data_Source := Order;
Put_Line (Normal, "Sending ORDER: " & Opaque_Type'Image (Order));
Put_Line (Normal, "Sending ORDER: " + Opaque_Type'Image (Order));
end Do_Ping_Spg;
--------------------
......@@ -63,14 +63,14 @@ package body Ping is
Data_Source : out Simple_type)
is
begin
Put_Line (Normal, "ORDER: " & Opaque_Type'Image (Data_Sink));
Put_Line (Normal, "ORDER: " + Opaque_Type'Image (Data_Sink));
if Data_Sink then
Var := Var + 1;
Put_Line (Normal, "Sending (+1) PING" & Simple_Type'Image (Var));
Put_Line (Normal, "Sending (+1) PING" + Simple_Type'Image (Var));
else
Var := Var + 5;
Put_Line (Normal, "Sending (+5) PING" & Simple_Type'Image (Var));
Put_Line (Normal, "Sending (+5) PING" + Simple_Type'Image (Var));
end if;
Data_Source := Var;
......
......@@ -64,8 +64,8 @@ package body PolyORB_HI.Aperiodic_Task is
(Put_Line
(Verbose,
"Aperiodic Task "
& Entity_Image (Entity)
& ": Wait initialization"));
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
delay until System_Startup_Time;
......@@ -73,7 +73,7 @@ package body PolyORB_HI.Aperiodic_Task is
pragma Debug (Put_Line
(Verbose,
"Aperiodic task initialized for entity "
& Entity_Image (Entity)));
+ Entity_Image (Entity)));
-- Main task loop
......@@ -83,8 +83,8 @@ package body PolyORB_HI.Aperiodic_Task is
(Put_Line
(Verbose,
"Aperiodic Task "
& Entity_Image (Entity)
& ": New Dispatch"));
+ Entity_Image (Entity)
+ ": New Dispatch"));
-- Block until an event is received
......@@ -94,8 +94,8 @@ package body PolyORB_HI.Aperiodic_Task is
(Put_Line
(Verbose,
"Aperiodic Task "
& Entity_Image (Entity)
& ": received event"));
+ Entity_Image (Entity)
+ ": received event"));
-- Execute the job
......
......@@ -63,8 +63,8 @@ package body PolyORB_HI.Background_Task is
(Put_Line
(Verbose,
"Background Task "
& Entity_Image (Entity)
& ": Wait initialization"));
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
delay until System_Startup_Time;
......@@ -72,14 +72,14 @@ package body PolyORB_HI.Background_Task is
pragma Debug (Put_Line
(Verbose,
"Background task initialized for entity "
& Entity_Image (Entity)));
+ Entity_Image (Entity)));
pragma Debug
(Put_Line
(Verbose,
"Background Task "
& Entity_Image (Entity)
& ": Run job"));
+ Entity_Image (Entity)
+ ": Run job"));
Error := Job;
......
......@@ -65,8 +65,8 @@ package body PolyORB_HI.Hybrid_Task is
(Put_Line
(Verbose,
"Hybrid Task "
& Entity_Image (Entity)
& ": Wait initialization"));
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
delay until System_Startup_Time;
......@@ -74,7 +74,7 @@ package body PolyORB_HI.Hybrid_Task is
pragma Debug (Put_Line
(Verbose,
"Hybrid task initialized for entity "
& Entity_Image (Entity)));
+ Entity_Image (Entity)));
-- Run the initialize entrypoint (if any)
......@@ -87,8 +87,8 @@ package body PolyORB_HI.Hybrid_Task is
(Put_Line
(Verbose,
"Hybrid Task "
& Entity_Image (Entity)
& ": New Dispatch"));
+ Entity_Image (Entity)
+ ": New Dispatch"));
-- Block until an event is received
......@@ -98,8 +98,8 @@ package body PolyORB_HI.Hybrid_Task is
(Put_Line
(Verbose,
"Hybrid Task "
& Entity_Image (Entity)
& ": received event"));
+ Entity_Image (Entity)
+ ": received event"));
-- Calculate the next deadline according to the minimal
-- inter-arrival time.
......
......@@ -104,7 +104,7 @@ package body PolyORB_HI.Hybrid_Task_Driver is
(Put_Line
(Verbose,
"Hybrid thread driver: Triggering task: "
& Entity_Image (T.The_Task)));
+ Entity_Image (T.The_Task)));
Trigger (T);
end if;
......@@ -144,7 +144,7 @@ package body PolyORB_HI.Hybrid_Task_Driver is
(Put_Line
(Verbose,
"Hybrid thread driver: Eligible task: "
& Entity_Image (T.The_Task)));
+ Entity_Image (T.The_Task)));
T.Eligible := True;
end if;
......
......@@ -39,12 +39,23 @@ with System;
package body PolyORB_HI.Output is
use Ada.Real_Time;
procedure Unprotected_Put_Line (Text : in String);
-- Not thread-safe Put_Line function
procedure Unprotected_Put (Text : in String);
-- Not thread-safe Put function
----------
-- Lock --
----------
protected Lock is
-- This lock has been defined to guarantee thread-safe output
-- display
procedure Put (Text : in String);
-- To guarantee thread-safe output display
procedure Put_Line (Text : in String);
-- To guarantee thread-safe output display
private
pragma Priority (System.Priority'Last);
......@@ -180,4 +191,17 @@ package body PolyORB_HI.Output is
Put_Line (Mode, Output);
end Dump;
---------
-- "+" --
---------
function "+" (S1 : String; S2 : String) return String is
S : String (1 .. S1'Length + S2'Length);
begin
S (1 .. S1'Length) := S1 (S1'First .. S1'Last);
S (S1'Length + 1 .. S'Last) := S2 (S2'First .. S2'Last);
return S;
end "+";
end PolyORB_HI.Output;
......@@ -63,25 +63,20 @@ package PolyORB_HI.Output is
procedure Put_Line (Text : in String);
-- As above but always displays the message
procedure Unprotected_Put_Line (Text : in String);
-- As above but this routine is not thread-safe
procedure Put (Mode : in Verbosity := Normal; Text : in String);
-- Display Text iff Mode is greater than Current_Mode. This
-- routine is thread-safe.
procedure Put (Text : in String);
-- As above but displays the message reguards less the mode
procedure Unprotected_Put (Text : in String);
-- As above but this routine is not thread-safe
-- As above but always displays the message
procedure Dump (Stream : Stream_Element_Array; Mode : Verbosity := Verbose);
-- Dump the content of Stream in an hexadecimal format
function "+" (S1 : String; S2 : String) return String;
private
pragma Inline (Put_Line);
pragma Inline (Unprotected_Put_Line);
end PolyORB_HI.Output;
......@@ -63,8 +63,8 @@ package body PolyORB_HI.Periodic_Task is
(Put_Line
(Verbose,
"Periodic Task "
& Entity_Image (Entity)
& ": Wait initialization"));
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
Next_Start := System_Startup_Time + Dispatch_Offset;
......@@ -81,7 +81,7 @@ package body PolyORB_HI.Periodic_Task is
pragma Debug
(Put_Line
(Verbose,
"Periodic Task " & Entity_Image (Entity) & ": New Cycle"));
"Periodic Task " + Entity_Image (Entity) + ": New Cycle"));
-- Execute the task's job
......@@ -94,8 +94,8 @@ package body PolyORB_HI.Periodic_Task is
-- T := Ada.Real_Time.Clock;
-- if T > Next_Start then
-- Put_Line (Normal, "***** Overload detected in task "
-- & Entity_Image (Entity) & " *****");
-- Put_Line (Normal, "Lag: " &
-- + Entity_Image (Entity) + " *****");
-- Put_Line (Normal, "Lag: " +
-- Duration'Image (To_Duration (Next_Start - T)));
-- end if;
......
......@@ -67,8 +67,8 @@ package body PolyORB_HI.Sporadic_Task is
(Put_Line
(Verbose,
"Sporadic Task "
& Entity_Image (Entity)
& ": Wait initialization"));
+ Entity_Image (Entity)
+ ": Wait initialization"));
Suspend_Until_True (Task_Suspension_Objects (Entity));
-- delay until System_Startup_Time;
......@@ -76,7 +76,7 @@ package body PolyORB_HI.Sporadic_Task is
pragma Debug (Put_Line
(Verbose,
"Sporadic task initialized for entity "
& Entity_Image (Entity)));
+ Entity_Image (Entity)));
-- Main task loop
......@@ -86,8 +86,8 @@ package body PolyORB_HI.Sporadic_Task is
(Put_Line
(Verbose,
"Sporadic Task "
& Entity_Image (Entity)
& ": New Dispatch"));
+ Entity_Image (Entity)
+ ": New Dispatch"));
-- Block until an event is received
......@@ -97,8 +97,8 @@ package body PolyORB_HI.Sporadic_Task is
(Put_Line
(Verbose,
"Sporadic Task "
& Entity_Image (Entity)
& ": received event"));
+ Entity_Image (Entity)
+ ": received event"));
-- Calculate the next start time according to the minimal
-- inter-arrival time.
......
......@@ -72,15 +72,15 @@ package body PolyORB_HI.Suspenders is
pragma Debug
(Put_Line
(Verbose, "Unblocking task "
& PolyORB_HI_Generated.Deployment.Entity_Image (J)));
+ PolyORB_HI_Generated.Deployment.Entity_Image (J)));
Set_True (Task_Suspension_Objects (J));
pragma Debug
(Put_Line
(Verbose, "Task "
& PolyORB_HI_Generated.Deployment.Entity_Image (J)
& " unblocked"));
+ PolyORB_HI_Generated.Deployment.Entity_Image (J)
+ " unblocked"));
end loop;
end Unblock_All_Tasks;
......
......@@ -244,8 +244,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Wait_Event: oldest unread event port = "
& Thread_Port_Images (P)));
+ ": Wait_Event: oldest unread event port = "
+ Thread_Port_Images (P)));
end Wait_Event;
----------------
......@@ -262,8 +262,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_Event: read valid event [data] on "
& Thread_Port_Images (P)));
+ ": Read_Event: read valid event [data] on "
+ Thread_Port_Images (P)));
end if;
end Read_Event;
......@@ -291,8 +291,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Dequeue: Empty queue for "
& Thread_Port_Images (T)));
+ ": Dequeue: Empty queue for "
+ Thread_Port_Images (T)));
P := Get_Most_Recent_Value (T);
......@@ -303,8 +303,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Dequeue: NO FIFO for "
& Thread_Port_Images (T)));
+ ": Dequeue: NO FIFO for "
+ Thread_Port_Images (T)));
P := Get_Most_Recent_Value (T);
......@@ -312,8 +312,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Dequeue: dequeuing "
& Thread_Port_Images (T)));
+ ": Dequeue: dequeuing "
+ Thread_Port_Images (T)));
if First = Last then
-- Update the value of N_Empties only when this is the
......@@ -368,32 +368,32 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_In: Empty queue for port "
& Thread_Port_Images (T)
& ". Reading the last stored value."));
+ ": Read_In: Empty queue for port "
+ Thread_Port_Images (T)
+ ". Reading the last stored value."));
P := Get_Most_Recent_Value (T);
else
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_In: Reading the oldest element in the"
& " queue of port "
& Thread_Port_Images (T)));
+ ": Read_In: Reading the oldest element in the"
+ " queue of port "
+ Thread_Port_Images (T)));
P := Global_Data_Queue (First + Offset - 1);
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_In: Global reading position: "
& Integer'Image (First + Offset - 1)));
+ ": Read_In: Global reading position: "
+ Integer'Image (First + Offset - 1)));
end if;
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_In: Value read from port "
& Thread_Port_Images (T)));
+ ": Read_In: Value read from port "
+ Thread_Port_Images (T)));
return P;
end Read_In;
......@@ -409,8 +409,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Read_Out: Value read from port "
& Thread_Port_Images (T)));
+ ": Read_Out: Value read from port "
+ Thread_Port_Images (T)));
return Most_Recent_Values (T);
end Read_Out;
......@@ -433,8 +433,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Set_Invalid: Setting INVALID for sending: port "
& Thread_Port_Images (T)));
+ ": Set_Invalid: Setting INVALID for sending: port "
+ Thread_Port_Images (T)));
Value_Put (T) := False;
end Set_Invalid;
......@@ -490,10 +490,10 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Store_In: FIFO is full."
& " Dropping oldest element."
& " Global storage position: "
& Integer'Image (First + Offset - 1)));
+ ": Store_In: FIFO is full."
+ " Dropping oldest element."
+ " Global storage position: "
+ Integer'Image (First + Offset - 1)));
Last := First;
......@@ -540,10 +540,10 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Store_In: FIFO is full."
& " Dropping newest element"
& " Global storage position: "
& Integer'Image (Last + Offset - 1)));
+ ": Store_In: FIFO is full."
+ " Dropping newest element"
+ " Global storage position: "
+ Integer'Image (Last + Offset - 1)));
-- Search the newest element in the history
......@@ -568,7 +568,7 @@ package body PolyORB_HI.Thread_Interrogators is
end if;
when Error =>
raise Program_Error with
CE & ": Store_In: FIFO is full";
CE + ": Store_In: FIFO is full";
end case;
-- Remove event in the history and shift
......@@ -578,9 +578,9 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Store_In: FIFO is full."
& " Removed element in history at"
& Integer'Image (Frst)));
+ ": Store_In: FIFO is full."
+ " Removed element in history at"
+ Integer'Image (Frst)));
loop
exit when Frst = Global_Data_Queue_Size
......@@ -622,8 +622,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Global storage position: "
& Integer'Image (Last + Offset - 1)));
+ ": Store_In: Global storage position: "
+ Integer'Image (Last + Offset - 1)));
end if;
......@@ -684,17 +684,17 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Insert event"
& " in history at: "
& Integer'Image (1)));
+ ": Store_In: Insert event"
+ " in history at: "
+ Integer'Image (1)));
else
GDH (Frst + 1) := PT;
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Insert event"
& " in history at: "
& Integer'Image (Frst + 1)));
+ ": Store_In: Insert event"
+ " in history at: "
+ Integer'Image (Frst + 1)));
end if;
end;
......@@ -707,9 +707,9 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Enqueued Event [Data] message"
& " for port "
& Thread_Port_Images (PT)));
+ ": Store_In: Enqueued Event [Data] message"
+ " for port "
+ Thread_Port_Images (PT)));
-- Update the barrier
......@@ -724,16 +724,16 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Storing Data message in DATA port "
& Thread_Port_Images (PT)));
+ ": Store_In: Storing Data message in DATA port "
+ Thread_Port_Images (PT)));
Set_Most_Recent_Value (PT, P, T);
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_In: Stored Data message in DATA port "
& Thread_Port_Images (PT)));
+ ": Store_In: Stored Data message in DATA port "
+ Thread_Port_Images (PT)));
end if;
end Store_In;
......@@ -750,8 +750,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_Out: Storing value for sending: port "
& Thread_Port_Images (PT)));
+ ": Store_Out: Storing value for sending: port "
+ Thread_Port_Images (PT)));
-- Mark as valid for sending
......@@ -760,8 +760,8 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Store_Out: Value stored for sending: port "
& Thread_Port_Images (PT)));
+ ": Store_Out: Value stored for sending: port "
+ Thread_Port_Images (PT)));
-- No need to go through the Set_ routine since we are
-- sending, not receiving.
......@@ -793,32 +793,32 @@ package body PolyORB_HI.Thread_Interrogators is
pragma Debug (Put_Line
(Verbose,
CE
& ": Count: Not initialized port: "
& Thread_Port_Images (T)));
+ ": Count: Not initialized port: "
+ Thread_Port_Images (T)));
return -1;
elsif Is_Empty then
pragma Debug (Put_Line
(Verbose,
CE
& ": Count: Empty FIFO for port "
& Thread_Port_Images (T)));
+ ": Count: Empty FIFO for port "
+ Thread_Port_Images (T)));
return 0;
elsif Fifo_Size = 0 then
pragma Debug (Put_Line
(Verbose,
CE
& ": Count: No FIFO for port "
& Thread_Port_Images (T)));
+ ": Count: No FIFO for port "
+ Thread_Port_Images (T)));
return 0;
else
pragma Debug (Put_Line
(Verbose,
CE
& ": Count: FIFO exists for port "
& Thread_Port_Images (T)));
+ ": Count: FIFO exists for port "
+ Thread_Port_Images (T)));
if Last >= First then
-- First configuration
......@@ -864,8 +864,8 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: event [data] port "
& Thread_Port_Images (P)));
+ ": Get_Most_Recent_Value: event [data] port "
+ Thread_Port_Images (P)));
S := Most_Recent_Values (P);
end if;
......@@ -878,33 +878,33 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: data port "
& Thread_Port_Images (P)
& ". Immediate connection"));
+ ": Get_Most_Recent_Value: data port "
+ Thread_Port_Images (P)
+ ". Immediate connection"));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: First ="
& Integer'Image (First)));
+ ": Get_Most_Recent_Value: First ="
+ Integer'Image (First)));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Last = "
& Integer'Image (Last)));
+ ": Get_Most_Recent_Value: Last = "
+ Integer'Image (Last)));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Offset = "
& Integer'Image (Offset)));
+ ": Get_Most_Recent_Value: Offset = "
+ Integer'Image (Offset)));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Global_Data_Queue_Size = "
& Integer'Image (Global_Data_Queue_Size)));
+ ": Get_Most_Recent_Value: Global_Data_Queue_Size = "
+ Integer'Image (Global_Data_Queue_Size)));
S := Global_Data_Queue (First + Offset - 1);
......@@ -912,10 +912,10 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Most recent value for"
& " data port "
& Thread_Port_Images (P)
& " got. Immediate connection"));
+ ": Get_Most_Recent_Value: Most recent value for"
+ " data port "
+ Thread_Port_Images (P)
+ " got. Immediate connection"));
else
-- Delayed connection: The element indexed by First is
-- the oldest element and the element indexed by Last
......@@ -925,44 +925,44 @@ package body PolyORB_HI.Thread_Interrogators is
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: data port "
& Thread_Port_Images (P)
& ". Delayed connection"));
+ ": Get_Most_Recent_Value: data port "
+ Thread_Port_Images (P)
+ ". Delayed connection"));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: First = "
& Integer'Image (First)));
+ ": Get_Most_Recent_Value: First = "
+ Integer'Image (First)));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Last = "
& Integer'Image (Last)));
+ ": Get_Most_Recent_Value: Last = "
+ Integer'Image (Last)));
pragma Debug
(Put_Line
(Verbose,
" Offset = " & Integer'Image (Offset)));
" Offset = " + Integer'Image (Offset)));
pragma Debug
(Put_Line
(Verbose,
CE
& ": Get_Most_Recent_Value: Global_Data_Queue_Size = "
& Integer'Image (Global_Data_Queue_Size)));
+ ": Get_Most_Recent_Value: Global_Data_Queue_Size = "