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 --
----------------------
-- 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;
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
P := P + 1;
if P > Max then
- return 0;
+ Exp := 0;
+ return;
else
M := False;
end if;
P := P + 1;
if P > Max or else not Real then
- return 0;
+ Exp := 0;
+ return;
else
M := True;
end if;
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
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;
--------------------
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
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);
Start := P;
+ pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+
-- Skip past an initial plus sign
if Str (P) = '+' then
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
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);
Start := P;
+ pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+
-- Remember an initial minus sign
if Str (P) = '-' then
-- 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;
Ptr : not null access Integer;
Max : Integer;
Ext : Boolean)
- with
- SPARK_Mode => Off -- Not proved yet
is
C : Character;
package System.Val_Util
with SPARK_Mode, Pure
is
+ pragma Unevaluated_Use_Of_Old (Allow);
procedure Bad_Value (S : String)
with
-- 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)
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
(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
-- 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
--
-- 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;
projects / thirdparty / gcc.git / commitdiff
