Commit 8337f4ef authored by yoogx's avatar yoogx

* Complete proof using GNATProve GPL2014

parent dd9f14c9
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 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 --
......@@ -40,19 +40,30 @@ package body PolyORB_HI.Utils is
function To_HI_String (S : String) return HI_String is
R : String (1 .. HI_String_Size) := (others => ' ');
begin
R (1 .. S'Length) := S;
return HI_String'(S => R,
L => S'Length);
end To_HI_String;
if S'Length < 1 then
return HI_String'(S => R,
L => 0);
---------------
-- To_String --
---------------
elsif S'Length <= HI_String_Size then
for J in 1 .. S'Length loop
R (J) := S (S'First + (J - 1));
function To_String (H : HI_String) return String is
begin
return H.S (1 .. H.L);
end To_String;
end loop;
-- XXX GNATProve GPL2014 cannot prove the code below, which
-- appears equivalent, TBI
-- R (1 .. S'Length) := S (S'First .. S'Last);
return HI_String'(S => R,
L => S'Length);
else
R (1 .. HI_String_Size) := S (S'First .. S'First + HI_String_Size - 1);
return HI_String'(S => R,
L => HI_String_Size);
end if;
end To_HI_String;
----------------
-- Swap_Bytes --
......@@ -110,21 +121,12 @@ package body PolyORB_HI.Utils is
function Parse_String (S : String; First : Integer; Delimiter : Character)
return Integer
is
Local_First : Integer;
Last : Integer;
Last : Integer := S'Last;
begin
if First < S'First then
Local_First := S'First;
else
Local_First := First;
end if;
for J in Local_First .. S'Last loop
for J in First .. S'Last loop
if S (J) = Delimiter then
Last := J - 1;
exit;
elsif J = S'Last then
Last := J;
end if;
end loop;
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2007-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 2007-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 --
......@@ -85,17 +85,28 @@ package PolyORB_HI.Utils is
HI_String_Size : constant := 80;
type HI_String is record
S : String (1 ..HI_String_Size);
L : Natural;
end record;
type HI_String is private;
function To_Hi_String (S : String) return HI_String;
function To_String (H : HI_String) return String;
function To_Hi_String (S : String) return HI_String
with Post => (Valid (To_Hi_String'Result));
function To_String (H : HI_String) return String
with Pre => (Valid (H));
function Length (H : HI_String) return Natural
with Pre => (Valid (H));
function Valid (H : HI_String) return Boolean;
function Parse_String (S : String; First : Integer; Delimiter : Character)
return Integer;
-- XXX
return Integer
with Pre => (First >= S'First and First <= S'Last);
-- XXX GNATProve GPL2014 cannot prove this, TBI
-- Post => ((Parse_String'Result = S'Last)
-- or (Parse_String'Result in S'Range
-- and then Parse_String'Result > S'First
-- and then S (Parse_String'Result - 1) = Delimiter));
-- Return index of the character just before Delimiter, or return S'last
------------------
-- Naming Table --
......@@ -110,4 +121,22 @@ package PolyORB_HI.Utils is
type Naming_Table_Type is array (Node_Type'Range)
of PolyORB_HI.Utils.Naming_Entry;
private
type HI_String is record
S : String (1 ..HI_String_Size);
L : Natural;
-- It is exepected L <= HI_String_Size
-- XXX Todo add a type invariant
end record;
function Length (H : HI_String) return Natural is
(H.L);
function Valid (H : HI_String) return Boolean is
(H.L <= HI_String_Size);
function To_String (H : HI_String) return String is
(H.S (1 .. H.L));
end PolyORB_HI.Utils;
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