Commit a8e3071f authored by yoogx's avatar yoogx

* Partial proofs using GNATProve GPL2014

parent 64c0b127
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- PolyORB HI is free software; you can redistribute it and/or modify it --
-- under terms of the GNU General Public License as published by the Free --
......@@ -37,6 +37,7 @@ with Ada.Real_Time;
with System;
package body PolyORB_HI.Output is
use Ada.Real_Time;
procedure Unprotected_Put_Line (Text : in String);
......@@ -45,11 +46,23 @@ package body PolyORB_HI.Output is
procedure Unprotected_Put (Text : in String);
-- Not thread-safe Put function
----------
-- Lock --
----------
-- This package encapsulates specific elements to protect against
-- race condition on the output buffer. It is in a package to
-- abide with SPARK restrictions.
package Output_Lock is
procedure Put_Line (Text : in String);
-- As above but always displays the message
procedure Put (Text : in String);
protected Lock 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
-- display
......@@ -57,30 +70,42 @@ package body PolyORB_HI.Output is
procedure Put_Line (Text : in String);
private
pragma Priority (System.Priority'Last);
end Lock;
private
pragma Priority (System.Priority'Last);
end Lock;
protected body Lock is
--------------
-- Put_Line --
--------------
protected body Lock is
procedure Put_Line (Text : in String) is
begin
Unprotected_Put_Line (Text);
end Put_Line;
--------------
-- Put_Line --
--------------
---------
-- Put --
---------
procedure Put (Text : in String) is
begin
Unprotected_Put (Text);
end Put;
end Lock;
procedure Put_Line (Text : in String) is
begin
Unprotected_Put_Line (Text);
Lock.Put_Line (Text);
end Put_Line;
---------
-- Put --
---------
procedure Put (Text : in String) is
begin
Unprotected_Put (Text);
Lock.Put (Text);
end Put;
end Lock;
end Output_Lock;
--------------
-- Put_Line --
......@@ -101,7 +126,7 @@ package body PolyORB_HI.Output is
procedure Put_Line (Text : in String) is
begin
Lock.Put_Line (Text);
Output_Lock.Put_Line (Text);
end Put_Line;
---------
......@@ -123,7 +148,7 @@ package body PolyORB_HI.Output is
procedure Put (Text : in String) is
begin
Lock.Put (Text);
Output_Lock.Put (Text);
end Put;
--------------------------
......@@ -165,7 +190,7 @@ package body PolyORB_HI.Output is
subtype Output_Line is String (Output_Position);
Hex : constant String := "0123456789ABCDEF";
Hex : constant array (0 .. 15) of Character := "0123456789ABCDEF";
Nil : constant Output_Line := (Output_Line'Range => ' ');
procedure Dump
......@@ -178,8 +203,8 @@ package body PolyORB_HI.Output is
for J in Stream'Range loop
if Index + 3 <= Output'Last then
Output (Index) := ' ';
Output (Index + 1) := Hex (Natural (Stream (J) / 16) + 1);
Output (Index + 2) := Hex (Natural (Stream (J) mod 16) + 1);
Output (Index + 1) := Hex (Natural (Stream (J) / 16));
Output (Index + 2) := Hex (Natural (Stream (J) mod 16));
Index := Index + 3;
else
Put_Line (Mode, Output);
......@@ -196,7 +221,7 @@ package body PolyORB_HI.Output is
---------
function "+" (S1 : String; S2 : String) return String is
S : String (1 .. S1'Length + S2'Length);
S : String (1 .. S1'Length + S2'Length) := (others => ' ');
begin
S (1 .. S1'Length) := S1 (S1'First .. S1'Last);
S (S1'Length + 1 .. S'Last) := S2 (S2'First .. S2'Last);
......
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