This proves the functionality of the utility procedures supporting the
implementation of 'Value attributes.
As a side-effect of this proof, fix possible range check failures.
GNATprove is run with switch --level=3.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-valboo.adb (First_Non_Space_Ghost): Move to
utilities.
(Value_Boolean): Prefix call to First_Non_Space_Ghost.
* libgnat/s-valboo.ads (First_Non_Space_Ghost): Move to
utilities.
(Is_Boolean_Image_Ghost, Value_Boolean): Prefix call to
First_Non_Space_Ghost.
* libgnat/s-valuer.adb (Scan_Raw_Real): Adapt to change of
function Scan_Exponent to procedure.
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Adapt to change of
function Scan_Exponent to procedure.
* libgnat/s-valuti.adb (First_Non_Space_Ghost): Function moved
here.
(Last_Number_Ghost): New ghost query function.
(Scan_Exponent): Change function with side-effects into
procedure, to mark in SPARK. Prove procedure wrt contract.
Change type of local P to avoid possible range check failure (it
is not known whether this can be activated by callers).
(Scan_Plus_Sign, Scan_Sign): Change type of local P to avoid
possible range check failure. Add loop invariants and assertions
for proof.
(Scan_Trailing_Blanks): Add loop invariant.
(Scan_Underscore): Remove SPARK_Mode Off.
* libgnat/s-valuti.ads (First_Non_Space_Ghost): Function moved
here.
(Last_Number_Ghost, Only_Number_Ghost, Is_Natural_Format_Ghost,
Scan_Natural_Ghost): New ghost query functions.
(Scan_Plus_Sign, Scan_Sign, Scan_Exponent, Scan_Trailing_Blanks,
Scan_Underscore): Add functional contracts.diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb
--- a/gcc/ada/libgnat/s-valboo.adb
+++ b/gcc/ada/libgnat/s-valboo.adb
@@ -43,19 +43,6 @@ 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 --
-------------------
@@ -68,7 +55,7 @@ is
begin
Normalize_String (S, F, L);
- pragma Assert (F = First_Non_Space_Ghost (S));
+ pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S));
if S (F .. L) = "TRUE" then
return True;
diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads
--- a/gcc/ada/libgnat/s-valboo.ads
+++ b/gcc/ada/libgnat/s-valboo.ads
@@ -47,22 +47,11 @@ package System.Val_Bool
is
pragma Preelaborate;
- 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);
+ F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str);
begin
(F <= Str'Last - 3
and then Str (F) in 't' | 'T'
@@ -92,7 +81,8 @@ is
with
Pre => Is_Boolean_Image_Ghost (Str),
Post =>
- Value_Boolean'Result = (Str (First_Non_Space_Ghost (Str)) in 't' | 'T');
+ Value_Boolean'Result =
+ (Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T');
-- Computes Boolean'Value (Str)
end System.Val_Bool;
diff --git a/gcc/ada/libgnat/s-valuer.adb b/gcc/ada/libgnat/s-valuer.adb
--- a/gcc/ada/libgnat/s-valuer.adb
+++ b/gcc/ada/libgnat/s-valuer.adb
@@ -511,6 +511,8 @@ package body System.Value_R is
Value : Uns;
-- Mantissa as an Integer
+ Expon : Integer;
+
begin
-- The default base is 10
@@ -643,7 +645,8 @@ package body System.Value_R is
-- Update pointer and scan exponent
Ptr.all := Index;
- Scale := Scale + Scan_Exponent (Str, Ptr, Max, Real => True);
+ Scan_Exponent (Str, Ptr, Max, Expon, Real => True);
+ Scale := Scale + Expon;
-- Here is where we check for a bad based number
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -234,7 +234,7 @@ package body System.Value_U is
-- Come here with scanned unsigned value in Uval. The only remaining
-- required step is to deal with exponent if one is present.
- Expon := Scan_Exponent (Str, Ptr, Max);
+ Scan_Exponent (Str, Ptr, Max, Expon);
if Expon /= 0 and then Uval /= 0 then
diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb
--- a/gcc/ada/libgnat/s-valuti.adb
+++ b/gcc/ada/libgnat/s-valuti.adb
@@ -62,6 +62,41 @@ is
end if;
end Bad_Value;
+ ---------------------------
+ -- First_Non_Space_Ghost --
+ ---------------------------
+
+ 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;
+
+ -----------------------
+ -- Last_Number_Ghost --
+ -----------------------
+
+ function Last_Number_Ghost (Str : String) return Positive is
+ begin
+ for J in Str'Range loop
+ if Str (J) not in '0' .. '9' | '_' then
+ return J - 1;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Str'First .. J => Str (K) in '0' .. '9' | '_');
+ end loop;
+
+ return Str'Last;
+ end Last_Number_Ghost;
+
----------------------
-- Normalize_String --
----------------------
@@ -119,15 +154,14 @@ is
-- Scan_Exponent --
-------------------
- function Scan_Exponent
+ procedure Scan_Exponent
(Str : String;
Ptr : not null access Integer;
Max : Integer;
- Real : Boolean := False) return Integer
- with
- SPARK_Mode => Off -- Function with side-effect through Ptr
+ Exp : out Integer;
+ Real : Boolean := False)
is
- P : Natural := Ptr.all;
+ P : Integer := Ptr.all;
M : Boolean;
X : Integer;
@@ -135,7 +169,8 @@ is
if P >= Max
or else (Str (P) /= 'E' and then Str (P) /= 'e')
then
- return 0;
+ Exp := 0;
+ return;
end if;
-- We have an E/e, see if sign follows
@@ -146,7 +181,8 @@ is
P := P + 1;
if P > Max then
- return 0;
+ Exp := 0;
+ return;
else
M := False;
end if;
@@ -155,7 +191,8 @@ is
P := P + 1;
if P > Max or else not Real then
- return 0;
+ Exp := 0;
+ return;
else
M := True;
end if;
@@ -165,7 +202,8 @@ is
end if;
if Str (P) not in '0' .. '9' then
- return 0;
+ Exp := 0;
+ return;
end if;
-- Scan out the exponent value as an unsigned integer. Values larger
@@ -176,28 +214,52 @@ is
X := 0;
- loop
- if X < (Integer'Last / 10) then
- X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
- end if;
+ declare
+ Rest : constant String := Str (P .. Max) with Ghost;
+ Last : constant Natural := Last_Number_Ghost (Rest) with Ghost;
- P := P + 1;
+ begin
+ pragma Assert (Is_Natural_Format_Ghost (Rest));
- exit when P > Max;
+ loop
+ pragma Assert (Str (P) = Rest (P));
+ pragma Assert (Str (P) in '0' .. '9');
- if Str (P) = '_' then
- Scan_Underscore (Str, P, Ptr, Max, False);
- else
- exit when Str (P) not in '0' .. '9';
- end if;
- end loop;
+ if X < (Integer'Last / 10) then
+ X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
+ end if;
+
+ pragma Loop_Invariant (X >= 0);
+ pragma Loop_Invariant (P in P'Loop_Entry .. Last);
+ pragma Loop_Invariant (Str (P) in '0' .. '9');
+ pragma Loop_Invariant
+ (Scan_Natural_Ghost (Rest, P'Loop_Entry, 0)
+ = (if P = Max
+ or else Rest (P + 1) not in '0' .. '9' | '_'
+ or else X >= Integer'Last / 10
+ then
+ X
+ else
+ Scan_Natural_Ghost (Rest, P + 1, X)));
+
+ P := P + 1;
+
+ exit when P > Max;
+
+ if Str (P) = '_' then
+ Scan_Underscore (Str, P, Ptr, Max, False);
+ else
+ exit when Str (P) not in '0' .. '9';
+ end if;
+ end loop;
+ end;
if M then
X := -X;
end if;
Ptr.all := P;
- return X;
+ Exp := X;
end Scan_Exponent;
--------------------
@@ -209,10 +271,8 @@ is
Ptr : not null access Integer;
Max : Integer;
Start : out Positive)
- with
- SPARK_Mode => Off -- Not proved yet
is
- P : Natural := Ptr.all;
+ P : Integer := Ptr.all;
begin
if P > Max then
@@ -224,6 +284,12 @@ is
while Str (P) = ' ' loop
P := P + 1;
+ pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
+ pragma Loop_Invariant (P in Ptr.all .. Max);
+ pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
+ pragma Loop_Invariant
+ (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
+
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@@ -232,6 +298,8 @@ is
Start := P;
+ pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+
-- Skip past an initial plus sign
if Str (P) = '+' then
@@ -256,10 +324,8 @@ is
Max : Integer;
Minus : out Boolean;
Start : out Positive)
- with
- SPARK_Mode => Off -- Not proved yet
is
- P : Natural := Ptr.all;
+ P : Integer := Ptr.all;
begin
-- Deal with case of null string (all blanks). As per spec, we raise
@@ -274,6 +340,12 @@ is
while Str (P) = ' ' loop
P := P + 1;
+ pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
+ pragma Loop_Invariant (P in Ptr.all .. Max);
+ pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
+ pragma Loop_Invariant
+ (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
+
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@@ -282,6 +354,8 @@ is
Start := P;
+ pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+
-- Remember an initial minus sign
if Str (P) = '-' then
@@ -315,15 +389,14 @@ is
-- Scan_Trailing_Blanks --
--------------------------
- procedure Scan_Trailing_Blanks (Str : String; P : Positive)
- with
- SPARK_Mode => Off -- Not proved yet
- is
+ procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
begin
for J in P .. Str'Last loop
if Str (J) /= ' ' then
Bad_Value (Str);
end if;
+
+ pragma Loop_Invariant (for all K in P .. J => Str (K) = ' ');
end loop;
end Scan_Trailing_Blanks;
@@ -337,8 +410,6 @@ is
Ptr : not null access Integer;
Max : Integer;
Ext : Boolean)
- with
- SPARK_Mode => Off -- Not proved yet
is
C : Character;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -47,6 +47,7 @@ with System.Case_Util;
package System.Val_Util
with SPARK_Mode, Pure
is
+ pragma Unevaluated_Use_Of_Old (Allow);
procedure Bad_Value (S : String)
with
@@ -62,6 +63,17 @@ is
-- Ghost function that returns True if S has only space characters from
-- index From to index To.
+ function First_Non_Space_Ghost (S : String) return Positive
+ with
+ Ghost,
+ Pre => not 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 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.
+
procedure Normalize_String
(S : in out String;
F, L : out Integer)
@@ -96,7 +108,27 @@ is
Ptr : not null access Integer;
Max : Integer;
Minus : out Boolean;
- Start : out Positive);
+ Start : out Positive)
+ with
+ Pre =>
+ -- Ptr.all .. Max is either an empty range, or a valid range in Str
+ (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
+ and then not Only_Space_Ghost (Str, Ptr.all, Max)
+ and then
+ (declare
+ F : constant Positive :=
+ First_Non_Space_Ghost (Str (Ptr.all .. Max));
+ begin
+ (if Str (F) in '+' | '-' then
+ F <= Max - 1 and then Str (F + 1) /= ' ')),
+ Post =>
+ (declare
+ F : constant Positive :=
+ First_Non_Space_Ghost (Str (Ptr.all'Old .. Max));
+ begin
+ Minus = (Str (F) = '-')
+ and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F)
+ and then Start = F);
-- The Str, Ptr, Max parameters are as for the scan routines (Str is the
-- string to be scanned starting at Ptr.all, and Max is the index of the
-- last character in the string). Scan_Sign first scans out any initial
@@ -121,17 +153,150 @@ is
(Str : String;
Ptr : not null access Integer;
Max : Integer;
- Start : out Positive);
+ Start : out Positive)
+ with
+ Pre =>
+ -- Ptr.all .. Max is either an empty range, or a valid range in Str
+ (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
+ and then not Only_Space_Ghost (Str, Ptr.all, Max)
+ and then
+ (declare
+ F : constant Positive :=
+ First_Non_Space_Ghost (Str (Ptr.all .. Max));
+ begin
+ (if Str (F) = '+' then
+ F <= Max - 1 and then Str (F + 1) /= ' ')),
+ Post =>
+ (declare
+ F : constant Positive :=
+ First_Non_Space_Ghost (Str (Ptr.all'Old .. Max));
+ begin
+ Ptr.all = (if Str (F) = '+' then F + 1 else F)
+ and then Start = F);
-- Same as Scan_Sign, but allows only plus, not minus. This is used for
-- modular types.
- function Scan_Exponent
+ function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean
+ is
+ (for all J in From .. To => Str (J) in '0' .. '9' | '_')
+ with
+ Ghost,
+ Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+ -- Ghost function that returns True if S has only number characters from
+ -- index From to index To.
+
+ function Last_Number_Ghost (Str : String) return Positive
+ with
+ Ghost,
+ Pre => Str /= "" and then Str (Str'First) in '0' .. '9',
+ Post => Last_Number_Ghost'Result in Str'Range
+ and then (if Last_Number_Ghost'Result < Str'Last then
+ Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_')
+ and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result);
+ -- Ghost function that returns the index of the last character in S that
+ -- is either a figure or underscore, which necessarily exists given the
+ -- precondition on S.
+
+ function Is_Natural_Format_Ghost (Str : String) return Boolean is
+ (Str /= ""
+ and then Str (Str'First) in '0' .. '9'
+ and then
+ (declare
+ L : constant Positive := Last_Number_Ghost (Str);
+ begin
+ Str (L) in '0' .. '9'
+ and then (for all J in Str'First .. L =>
+ (if Str (J) = '_' then Str (J + 1) /= '_'))))
+ with
+ Ghost;
+ -- Ghost function that determines if Str has the correct format for a
+ -- natural number, consisting in a sequence of figures possibly separated
+ -- by single underscores. It may be followed by other characters.
+
+ function Scan_Natural_Ghost
+ (Str : String;
+ P : Natural;
+ Acc : Natural)
+ return Natural
+ is
+ (if Str (P) = '_' then
+ Scan_Natural_Ghost (Str, P + 1, Acc)
+ else
+ (declare
+ Shift_Acc : constant Natural :=
+ Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
+ begin
+ (if P = Str'Last
+ or else Str (P + 1) not in '0' .. '9' | '_'
+ or else Shift_Acc >= Integer'Last / 10
+ then
+ Shift_Acc
+ else
+ Scan_Natural_Ghost (Str, P + 1, Shift_Acc))))
+ with
+ Ghost,
+ Subprogram_Variant => (Increases => P),
+ Pre => Is_Natural_Format_Ghost (Str)
+ and then P in Str'First .. Last_Number_Ghost (Str)
+ and then Acc < Integer'Last / 10;
+ -- Ghost function that recursively computes the natural number in Str, up
+ -- to the first number greater or equal to Natural'Last / 10, assuming Acc
+ -- has been scanned already and scanning continues at index P.
+
+ procedure Scan_Exponent
(Str : String;
Ptr : not null access Integer;
Max : Integer;
- Real : Boolean := False) return Integer
+ Exp : out Integer;
+ Real : Boolean := False)
with
- SPARK_Mode => Off; -- Function with side-effect through Ptr
+ Pre =>
+ -- Ptr.all .. Max is either an empty range, or a valid range in Str
+ (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
+ and then
+ Max < Natural'Last
+ and then
+ (if Ptr.all < Max and then Str (Ptr.all) in 'E' | 'e' then
+ (declare
+ Plus_Sign : constant Boolean := Str (Ptr.all + 1) = '+';
+ Minus_Sign : constant Boolean := Str (Ptr.all + 1) = '-';
+ Sign : constant Boolean := Plus_Sign or Minus_Sign;
+ begin
+ (if Minus_Sign and not Real then True
+ elsif Sign
+ and then (Ptr.all > Max - 2
+ or else Str (Ptr.all + 2) not in '0' .. '9')
+ then True
+ else
+ (declare
+ Start : constant Natural :=
+ (if Sign then Ptr.all + 2 else Ptr.all + 1);
+ begin
+ Is_Natural_Format_Ghost (Str (Start .. Max)))))),
+ Post =>
+ (if Ptr.all'Old < Max and then Str (Ptr.all'Old) in 'E' | 'e' then
+ (declare
+ Plus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '+';
+ Minus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '-';
+ Sign : constant Boolean := Plus_Sign or Minus_Sign;
+ Unchanged : constant Boolean :=
+ Exp = 0 and Ptr.all = Ptr.all'Old;
+ begin
+ (if Minus_Sign and not Real then Unchanged
+ elsif Sign
+ and then (Ptr.all'Old > Max - 2
+ or else Str (Ptr.all'Old + 2) not in '0' .. '9')
+ then Unchanged
+ else
+ (declare
+ Start : constant Natural :=
+ (if Sign then Ptr.all'Old + 2 else Ptr.all'Old + 1);
+ Value : constant Natural :=
+ Scan_Natural_Ghost (Str (Start .. Max), Start, 0);
+ begin
+ Exp = (if Minus_Sign then -Value else Value))))
+ else
+ Exp = 0 and Ptr.all = Ptr.all'Old);
-- 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
@@ -146,18 +311,37 @@ is
-- This routine must not be called with Str'Last = Positive'Last. There is
-- no check for this case, the caller must ensure this condition is met.
- procedure Scan_Trailing_Blanks (Str : String; P : Positive);
+ procedure Scan_Trailing_Blanks (Str : String; P : Positive)
+ with
+ Pre => P >= Str'First
+ and then Only_Space_Ghost (Str, P, Str'Last);
-- Checks that the remainder of the field Str (P .. Str'Last) is all
-- blanks. Raises Constraint_Error if a non-blank character is found.
+ pragma Warnings
+ (GNATprove, Off, """Ptr"" is not modified",
+ Reason => "Ptr is actually modified when raising an exception");
procedure Scan_Underscore
(Str : String;
P : in out Natural;
Ptr : not null access Integer;
Max : Integer;
- Ext : Boolean);
+ Ext : Boolean)
+ with
+ Pre => P in Str'Range
+ and then Str (P) = '_'
+ and then Max in Str'Range
+ and then P < Max
+ and then
+ (if Ext then
+ Str (P + 1) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
+ else
+ Str (P + 1) in '0' .. '9'),
+ Post =>
+ P = P'Old + 1
+ and then Ptr.all = Ptr.all;
-- Called if an underscore is encountered while scanning digits. Str (P)
- -- contains the underscore. Ptr it the pointer to be returned to the
+ -- contains the underscore. Ptr is the pointer to be returned to the
-- ultimate caller of the scan routine, Max is the maximum subscript in
-- Str, and Ext indicates if extended digits are allowed. In the case
-- where the underscore is invalid, Constraint_Error is raised with Ptr
@@ -166,5 +350,6 @@ is
--
-- This routine must not be called with Str'Last = Positive'Last. There is
-- no check for this case, the caller must ensure this condition is met.
+ pragma Warnings (GNATprove, On, """Ptr"" is not modified");
end System.Val_Util;
