@@ -29,7 +29,17 @@
-- --
------------------------------------------------------------------------------
-package body System.Img_Bool is
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
+package body System.Img_Bool
+ with SPARK_Mode
+is
-------------------
-- Image_Boolean --
@@ -31,13 +31,33 @@
-- Boolean'Image
-package System.Img_Bool is
- pragma Pure;
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
+with System.Val_Bool;
+
+package System.Img_Bool
+ with SPARK_Mode, Preelaborate
+is
procedure Image_Boolean
(V : Boolean;
S : in out String;
- P : out Natural);
+ P : out Natural)
+ with
+ Pre => S'First = 1
+ and then (if V then S'Length >= 4 else S'Length >= 5),
+ Post => (if V then P = 4 else P = 5)
+ and then System.Val_Bool.Is_Boolean_Image_Ghost (S (1 .. P))
+ and then System.Val_Bool.Value_Boolean (S (1 .. P)) = V;
-- Computes Boolean'Image (V) and stores the result in S (1 .. P)
-- setting the resulting value of P. The caller guarantees that S
-- is long enough to hold the result, and that S'First is 1.
@@ -29,22 +29,47 @@
-- --
------------------------------------------------------------------------------
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with System.Val_Util; use System.Val_Util;
-package body System.Val_Bool is
+package body System.Val_Bool
+ with SPARK_Mode
+is
+
+ function First_Non_Space_Ghost (S : String) return Positive is
+ begin
+ for J in S'Range loop
+ if S (J) /= ' ' then
+ return J;
+ end if;
+
+ pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
+ end loop;
+
+ raise Program_Error;
+ end First_Non_Space_Ghost;
-------------------
-- Value_Boolean --
-------------------
function Value_Boolean (Str : String) return Boolean is
- F : Natural;
- L : Natural;
+ F : Integer;
+ L : Integer;
S : String (Str'Range) := Str;
begin
Normalize_String (S, F, L);
+ pragma Assert (F = First_Non_Space_Ghost (S));
+
if S (F .. L) = "TRUE" then
return True;
@@ -29,10 +29,70 @@
-- --
------------------------------------------------------------------------------
-package System.Val_Bool is
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
+with System.Val_Util;
+
+package System.Val_Bool
+ with SPARK_Mode
+is
pragma Preelaborate;
- function Value_Boolean (Str : String) return Boolean;
+ function First_Non_Space_Ghost (S : String) return Positive
+ with
+ Ghost,
+ Pre => not System.Val_Util.Only_Space_Ghost (S, S'First, S'Last),
+ Post => First_Non_Space_Ghost'Result in S'Range
+ and then S (First_Non_Space_Ghost'Result) /= ' '
+ and then System.Val_Util.Only_Space_Ghost
+ (S, S'First, First_Non_Space_Ghost'Result - 1);
+ -- Ghost function that returns the index of the first non-space character
+ -- in S, which necessarily exists given the precondition on S.
+
+ function Is_Boolean_Image_Ghost (Str : String) return Boolean is
+ (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then
+ (declare
+ F : constant Positive := First_Non_Space_Ghost (Str);
+ begin
+ (F <= Str'Last - 3
+ and then Str (F) in 't' | 'T'
+ and then Str (F + 1) in 'r' | 'R'
+ and then Str (F + 2) in 'u' | 'U'
+ and then Str (F + 3) in 'e' | 'E'
+ and then
+ (if F + 3 < Str'Last then
+ System.Val_Util.Only_Space_Ghost (Str, F + 4, Str'Last)))
+ or else
+ (F <= Str'Last - 4
+ and then Str (F) in 'f' | 'F'
+ and then Str (F + 1) in 'a' | 'A'
+ and then Str (F + 2) in 'l' | 'L'
+ and then Str (F + 3) in 's' | 'S'
+ and then Str (F + 4) in 'e' | 'E'
+ and then
+ (if F + 4 < Str'Last then
+ System.Val_Util.Only_Space_Ghost (Str, F + 5, Str'Last)))))
+ with
+ Ghost;
+ -- Ghost function that returns True iff Str is the image of a boolean, that
+ -- is "true" or "false" in any capitalization, possibly surounded by space
+ -- characters.
+
+ function Value_Boolean (Str : String) return Boolean
+ with
+ Pre => Is_Boolean_Image_Ghost (Str),
+ Post =>
+ Value_Boolean'Result = (Str (First_Non_Space_Ghost (Str)) in 't' | 'T');
-- Computes Boolean'Value (Str)
end System.Val_Bool;
@@ -29,15 +29,27 @@
-- --
------------------------------------------------------------------------------
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with System.Case_Util; use System.Case_Util;
-package body System.Val_Util is
+package body System.Val_Util
+ with SPARK_Mode
+is
---------------
-- Bad_Value --
---------------
procedure Bad_Value (S : String) is
+ pragma Annotate (GNATprove, Intentional, "exception might be raised",
+ "Intentional exception from Bad_Value");
begin
-- Bad_Value might be called with very long strings allocated on the
-- heap. Limit the size of the message so that we avoid creating a
@@ -62,21 +74,33 @@ package body System.Val_Util is
F := S'First;
L := S'Last;
+ -- Case of empty string
+
+ if F > L then
+ return;
+ end if;
+
-- Scan for leading spaces
- while F <= L and then S (F) = ' ' loop
+ while F < L and then S (F) = ' ' loop
+ pragma Loop_Invariant (F in S'First .. L - 1);
+ pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' ');
F := F + 1;
end loop;
- -- Case of no nonspace characters found
+ -- Case of no nonspace characters found. Decrease L to ensure L < F
+ -- without risking an overflow if F is Integer'Last.
- if F > L then
+ if S (F) = ' ' then
+ L := L - 1;
return;
end if;
-- Scan for trailing spaces
while S (L) = ' ' loop
+ pragma Loop_Invariant (L in F + 1 .. S'Last);
+ pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' ');
L := L - 1;
end loop;
@@ -85,6 +109,8 @@ package body System.Val_Util is
if S (F) /= ''' then
for J in F .. L loop
S (J) := To_Upper (S (J));
+ pragma Loop_Invariant
+ (for all K in F .. J => S (K) = To_Upper (S'Loop_Entry (K)));
end loop;
end if;
end Normalize_String;
@@ -98,6 +124,8 @@ package body System.Val_Util is
Ptr : not null access Integer;
Max : Integer;
Real : Boolean := False) return Integer
+ with
+ SPARK_Mode => Off -- Function with side-effect through Ptr
is
P : Natural := Ptr.all;
M : Boolean;
@@ -181,6 +209,8 @@ package body System.Val_Util is
Ptr : not null access Integer;
Max : Integer;
Start : out Positive)
+ with
+ SPARK_Mode => Off -- Not proved yet
is
P : Natural := Ptr.all;
@@ -226,6 +256,8 @@ package body System.Val_Util is
Max : Integer;
Minus : out Boolean;
Start : out Positive)
+ with
+ SPARK_Mode => Off -- Not proved yet
is
P : Natural := Ptr.all;
@@ -283,7 +315,10 @@ package body System.Val_Util is
-- Scan_Trailing_Blanks --
--------------------------
- procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
+ procedure Scan_Trailing_Blanks (Str : String; P : Positive)
+ with
+ SPARK_Mode => Off -- Not proved yet
+ is
begin
for J in P .. Str'Last loop
if Str (J) /= ' ' then
@@ -302,6 +337,8 @@ package body System.Val_Util is
Ptr : not null access Integer;
Max : Integer;
Ext : Boolean)
+ with
+ SPARK_Mode => Off -- Not proved yet
is
C : Character;
@@ -31,16 +31,60 @@
-- This package provides some common utilities used by the s-valxxx files
-package System.Val_Util is
- pragma Pure;
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
- procedure Bad_Value (S : String);
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
+with System.Case_Util;
+
+package System.Val_Util
+ with SPARK_Mode, Pure
+is
+
+ procedure Bad_Value (S : String)
+ with
+ Depends => (null => S);
pragma No_Return (Bad_Value);
-- Raises constraint error with message: bad input for 'Value: "xxx"
+ function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is
+ (for all J in From .. To => S (J) = ' ')
+ with
+ Ghost,
+ Pre => From > To or else (From >= S'First and then To <= S'Last);
+ -- Ghost function that returns True if S has only space characters from
+ -- index From to index To.
+
procedure Normalize_String
(S : in out String;
- F, L : out Integer);
+ F, L : out Integer)
+ with
+ Post => (if Only_Space_Ghost (S'Old, S'First, S'Last) then
+ F > L
+ else
+ F >= S'First
+ and then L <= S'Last
+ and then F <= L
+ and then Only_Space_Ghost (S'Old, S'First, F - 1)
+ and then S'Old (F) /= ' '
+ and then S'Old (L) /= ' '
+ and then
+ (if L < S'Last then
+ Only_Space_Ghost (S'Old, L + 1, S'Last))
+ and then
+ (if S'Old (F) /= ''' then
+ (for all J in S'Range =>
+ (if J in F .. L then
+ S (J) = System.Case_Util.To_Upper (S'Old (J))
+ else
+ S (J) = S'Old (J)))));
-- This procedure scans the string S setting F to be the index of the first
-- non-blank character of S and L to be the index of the last non-blank
-- character of S. Any lower case characters present in S will be folded to
@@ -85,7 +129,9 @@ package System.Val_Util is
(Str : String;
Ptr : not null access Integer;
Max : Integer;
- Real : Boolean := False) return Integer;
+ Real : Boolean := False) return Integer
+ with
+ SPARK_Mode => Off; -- Function with side-effect through Ptr
-- Called to scan a possible exponent. Str, Ptr, Max are as described above
-- for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an
-- exponent is scanned out, with the exponent value returned in Exp, and