Load_Integer (File, Buf, Stop);
end if;
- Item := Scan (Buf, Ptr'Access, Stop);
+ Scan (Buf, Ptr'Access, Stop, Item);
Check_End_Of_Field (Buf, Stop, Ptr, Width);
end Get;
begin
String_Skip (From, Pos);
- Item := Scan (From, Pos'Access, From'Last);
+ Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception
private generic
type Num is (<>);
- with function Scan
- (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+ with procedure Scan
+ (Str : String;
+ Ptr : not null access Integer;
+ Max : Integer;
+ Res : out Num);
with procedure Set_Image
(V : Num; S : in out String; P : in out Natural);
with procedure Set_Image_Width
Load_Integer (File, Buf, Stop);
end if;
- Item := Scan (Buf, Ptr'Access, Stop);
+ Scan (Buf, Ptr'Access, Stop, Item);
Check_End_Of_Field (Buf, Stop, Ptr, Width);
end Get;
begin
String_Skip (From, Pos);
- Item := Scan (From, Pos'Access, From'Last);
+ Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception
private generic
type Num is (<>);
- with function Scan
- (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+ with procedure Scan
+ (Str : String;
+ Ptr : not null access Integer;
+ Max : Integer;
+ Res : out Num);
with procedure Set_Image
(V : Num; S : in out String; P : in out Natural);
with procedure Set_Image_Width
Load_Integer (File, Buf, Stop);
end if;
- Item := Scan (Buf, Ptr'Access, Stop);
+ Scan (Buf, Ptr'Access, Stop, Item);
Check_End_Of_Field (Buf, Stop, Ptr, Width);
end Get;
begin
String_Skip (From, Pos);
- Item := Scan (From, Pos'Access, From'Last);
+ Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception
private generic
type Num is (<>);
- with function Scan
- (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+ with procedure Scan
+ (Str : String;
+ Ptr : not null access Integer;
+ Max : Integer;
+ Res : out Num);
with procedure Set_Image
(V : Num; S : in out String; P : in out Natural);
with procedure Set_Image_Width
begin
Normalize_String (S, F, L);
- pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S));
+ pragma Assert (F = System.Val_Util.First_Non_Space_Ghost
+ (S, Str'First, Str'Last));
if S (F .. L) = "TRUE" then
return True;
(not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
and then
(declare
- F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str);
+ F : constant Positive := System.Val_Util.First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
begin
(F <= Str'Last - 3
and then Str (F) in 't' | 'T'
Pre => Is_Boolean_Image_Ghost (Str),
Post =>
Value_Boolean'Result =
- (Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T');
+ (Str (System.Val_Util.First_Non_Space_Ghost
+ (Str, Str'First, Str'Last)) in 't' | 'T');
-- Computes Boolean'Value (Str)
end System.Val_Bool;
package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned);
- function Scan_Integer
+ procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Integer
+ Max : Integer;
+ Res : out Integer)
renames Impl.Scan_Integer;
function Value_Integer (Str : String) return Integer
Long_Long_Unsigned,
Val_LLU.Scan_Raw_Long_Long_Unsigned);
- function Scan_Long_Long_Integer
+ procedure Scan_Long_Long_Integer
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Integer
+ Max : Integer;
+ Res : out Long_Long_Integer)
renames Impl.Scan_Integer;
function Value_Long_Long_Integer (Str : String) return Long_Long_Integer
Long_Long_Long_Unsigned,
Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned);
- function Scan_Long_Long_Long_Integer
+ procedure Scan_Long_Long_Long_Integer
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Long_Integer
+ Max : Integer;
+ Res : out Long_Long_Long_Integer)
renames Impl.Scan_Integer;
function Value_Long_Long_Long_Integer
-- This package contains routines for scanning modular Long_Long_Unsigned
-- values for use in Text_IO.Modular_IO, and the Value attribute.
+-- 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,
+ Subprogram_Variant => Ignore);
+
with System.Unsigned_Types;
with System.Value_U;
-package System.Val_LLLU is
+package System.Val_LLLU with SPARK_Mode is
pragma Preelaborate;
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
package Impl is new Value_U (Long_Long_Long_Unsigned);
- function Scan_Raw_Long_Long_Long_Unsigned
+ procedure Scan_Raw_Long_Long_Long_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Long_Unsigned
+ Max : Integer;
+ Res : out Long_Long_Long_Unsigned)
renames Impl.Scan_Raw_Unsigned;
- function Scan_Long_Long_Long_Unsigned
+ procedure Scan_Long_Long_Long_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Long_Unsigned
+ Max : Integer;
+ Res : out Long_Long_Long_Unsigned)
renames Impl.Scan_Unsigned;
function Value_Long_Long_Long_Unsigned
-- This package contains routines for scanning modular Long_Long_Unsigned
-- values for use in Text_IO.Modular_IO, and the Value attribute.
+-- 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,
+ Subprogram_Variant => Ignore);
+
with System.Unsigned_Types;
with System.Value_U;
-package System.Val_LLU is
+package System.Val_LLU with SPARK_Mode is
pragma Preelaborate;
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
package Impl is new Value_U (Long_Long_Unsigned);
- function Scan_Raw_Long_Long_Unsigned
+ procedure Scan_Raw_Long_Long_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Unsigned
+ Max : Integer;
+ Res : out Long_Long_Unsigned)
renames Impl.Scan_Raw_Unsigned;
- function Scan_Long_Long_Unsigned
+ procedure Scan_Long_Long_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Long_Long_Unsigned
+ Max : Integer;
+ Res : out Long_Long_Unsigned)
renames Impl.Scan_Unsigned;
function Value_Long_Long_Unsigned
-- Scan_Integer --
------------------
- function Scan_Integer
+ procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Int
+ Max : Integer;
+ Res : out Int)
is
Uval : Uns;
-- Unsigned result
Bad_Value (Str);
end if;
- Uval := Scan_Raw_Unsigned (Str, Ptr, Max);
+ Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
-- Deal with overflow cases, and also with largest negative number
if Uval > Uns (Int'Last) then
if Minus and then Uval = Uns (-(Int'First)) then
- return Int'First;
+ Res := Int'First;
else
Bad_Value (Str);
end if;
-- Negative values
elsif Minus then
- return -(Int (Uval));
+ Res := -(Int (Uval));
-- Positive values
else
- return Int (Uval);
+ Res := Int (Uval);
end if;
end Scan_Integer;
V : Int;
P : aliased Integer := Str'First;
begin
- V := Scan_Integer (Str, P'Access, Str'Last);
+ Scan_Integer (Str, P'Access, Str'Last, V);
Scan_Trailing_Blanks (Str, P);
return V;
end;
type Uns is mod <>;
- with function Scan_Raw_Unsigned
+ with procedure Scan_Raw_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Uns;
+ Max : Integer;
+ Res : out Uns);
package System.Value_I is
pragma Preelaborate;
- function Scan_Integer
+ procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Int;
- -- This function scans the string starting at Str (Ptr.all) for a valid
+ Max : Integer;
+ Res : out Int);
+ -- This procedure scans the string starting at Str (Ptr.all) for a valid
-- integer according to the syntax described in (RM 3.5(43)). The substring
-- scanned extends no further than Str (Max). There are three cases for the
-- return:
-- --
------------------------------------------------------------------------------
-with System.Val_Util; use System.Val_Util;
-
package body System.Value_U 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,
+ Assert_And_Cut => Ignore,
+ Subprogram_Variant => Ignore);
+
+ -- Local lemmas
+
+ procedure Lemma_Digit_Is_Before_Last
+ (Str : String;
+ P : Integer;
+ From : Integer;
+ To : Integer)
+ with Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then P in From .. To
+ and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+ Post => P /= Last_Hexa_Ghost (Str (From .. To)) + 1;
+ -- If the character at position P is a digit, P cannot be the position of
+ -- of the first non-digit in Str.
+
+ procedure Lemma_End_Of_Scan
+ (Str : String;
+ From : Integer;
+ To : Integer;
+ Base : Uns;
+ Acc : Uns)
+ with Ghost,
+ Pre => Str'Last /= Positive'Last and then From > To,
+ Post => Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+ (False, Acc);
+ -- Unfold the definition of Scan_Based_Number_Ghost on an empty string
+
+ procedure Lemma_Scan_Digit
+ (Str : String;
+ P : Integer;
+ Lst : Integer;
+ Digit : Uns;
+ Base : Uns;
+ Old_Acc : Uns;
+ Acc : Uns;
+ Scan_Val : Uns_Option;
+ Old_Overflow : Boolean;
+ Overflow : Boolean)
+ with Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then Lst in Str'Range
+ and then P in Str'First .. Lst
+ and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then Digit = Hexa_To_Unsigned_Ghost (Str (P))
+ and then Only_Hexa_Ghost (Str, P, Lst)
+ and then Base in 2 .. 16
+ and then (if Digit < Base and then Old_Acc <= Uns'Last / Base
+ then Acc = Base * Old_Acc + Digit)
+ and then (if Digit >= Base
+ or else Old_Acc > Uns'Last / Base
+ or else (Old_Acc > (Uns'Last - Base + 1) / Base
+ and then Acc < Uns'Last / Base)
+ then Overflow
+ else Overflow = Old_Overflow)
+ and then
+ (if not Old_Overflow then
+ Scan_Val = Scan_Based_Number_Ghost
+ (Str, P, Lst, Base, Old_Acc)),
+ Post =>
+ (if not Overflow then
+ Scan_Val = Scan_Based_Number_Ghost
+ (Str, P + 1, Lst, Base, Acc))
+ and then
+ (if Overflow then Old_Overflow or else Scan_Val.Overflow);
+ -- Unfold the definition of Scan_Based_Number_Ghost when the string starts
+ -- with a digit.
+
+ procedure Lemma_Scan_Underscore
+ (Str : String;
+ P : Integer;
+ From : Integer;
+ To : Integer;
+ Lst : Integer;
+ Base : Uns;
+ Acc : Uns;
+ Scan_Val : Uns_Option;
+ Overflow : Boolean;
+ Ext : Boolean)
+ with Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Lst <= To
+ and then P in From .. Lst + 1
+ and then P <= To
+ and then
+ (if Ext then
+ Is_Based_Format_Ghost (Str (From .. To))
+ and then Lst = Last_Hexa_Ghost (Str (From .. To))
+ else Is_Natural_Format_Ghost (Str (From .. To))
+ and then Lst = Last_Number_Ghost (Str (From .. To)))
+ and then Str (P) = '_'
+ and then
+ (if not Overflow then
+ Scan_Val = Scan_Based_Number_Ghost (Str, P, Lst, Base, Acc)),
+ Post => P + 1 <= Lst
+ and then
+ (if Ext then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ else Str (P + 1) in '0' .. '9')
+ and then
+ (if not Overflow then
+ Scan_Val = Scan_Based_Number_Ghost (Str, P + 1, Lst, Base, Acc));
+ -- Unfold the definition of Scan_Based_Number_Ghost when the string starts
+ -- with an underscore.
+
+ -----------------------------
+ -- Local lemma null bodies --
+ -----------------------------
+
+ procedure Lemma_Digit_Is_Before_Last
+ (Str : String;
+ P : Integer;
+ From : Integer;
+ To : Integer)
+ is null;
+
+ procedure Lemma_End_Of_Scan
+ (Str : String;
+ From : Integer;
+ To : Integer;
+ Base : Uns;
+ Acc : Uns)
+ is null;
+
+ procedure Lemma_Scan_Underscore
+ (Str : String;
+ P : Integer;
+ From : Integer;
+ To : Integer;
+ Lst : Integer;
+ Base : Uns;
+ Acc : Uns;
+ Scan_Val : Uns_Option;
+ Overflow : Boolean;
+ Ext : Boolean)
+ is null;
+
+ ---------------------
+ -- Last_Hexa_Ghost --
+ ---------------------
+
+ function Last_Hexa_Ghost (Str : String) return Positive is
+ begin
+ for J in Str'Range loop
+ if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
+ return J - 1;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Str'First .. J =>
+ Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
+ end loop;
+
+ return Str'Last;
+ end Last_Hexa_Ghost;
+
+ ----------------------
+ -- Lemma_Scan_Digit --
+ ----------------------
+
+ procedure Lemma_Scan_Digit
+ (Str : String;
+ P : Integer;
+ Lst : Integer;
+ Digit : Uns;
+ Base : Uns;
+ Old_Acc : Uns;
+ Acc : Uns;
+ Scan_Val : Uns_Option;
+ Old_Overflow : Boolean;
+ Overflow : Boolean)
+ is
+ pragma Unreferenced (Str, P, Lst, Scan_Val, Overflow, Old_Overflow);
+ begin
+ if Digit >= Base then
+ null;
+
+ elsif Old_Acc <= (Uns'Last - Base + 1) / Base then
+ pragma Assert (not Scan_Overflows_Ghost (Digit, Base, Old_Acc));
+
+ elsif Old_Acc > Uns'Last / Base then
+ null;
+
+ else
+ pragma Assert
+ ((Acc < Uns'Last / Base) =
+ Scan_Overflows_Ghost (Digit, Base, Old_Acc));
+ end if;
+ end Lemma_Scan_Digit;
+
-----------------------
-- Scan_Raw_Unsigned --
-----------------------
- function Scan_Raw_Unsigned
+ procedure Scan_Raw_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Uns
+ Max : Integer;
+ Res : out Uns)
is
P : Integer;
-- Local copy of the pointer
Digit : Uns;
-- Digit value
+ Ptr_Old : constant Integer := Ptr.all
+ with Ghost;
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (Ptr.all .. Max))
+ with Ghost;
+ Init_Val : constant Uns_Option :=
+ Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
+ with Ghost;
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < Max - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ with Ghost;
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
+ else Last_Num_Init)
+ with Ghost;
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < Max
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)
+ with Ghost;
+ Based_Val : constant Uns_Option :=
+ (if Starts_As_Based and then not Init_Val.Overflow
+ then Scan_Based_Number_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+ else Init_Val)
+ with Ghost;
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1)
+ with Ghost;
+
begin
-- We do not tolerate strings with Str'Last = Positive'Last
Umax10 : constant Uns := Uns'Last / 10;
-- Numbers bigger than Umax10 overflow if multiplied by 10
+ Old_Uval : Uns with Ghost;
+ Old_Overflow : Boolean with Ghost;
+
begin
-- Loop through decimal digits
loop
+ pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Init + 1);
+ pragma Loop_Invariant
+ (if Overflow then Init_Val.Overflow);
+ pragma Loop_Invariant
+ (if not Overflow
+ then Init_Val = Scan_Based_Number_Ghost
+ (Str, P, Last_Num_Init, Acc => Uval));
+
exit when P > Max;
Digit := Character'Pos (Str (P)) - Character'Pos ('0');
if Digit > 9 then
if Str (P) = '_' then
+ Lemma_Scan_Underscore
+ (Str, P, Ptr_Old, Max, Last_Num_Init, 10, Uval,
+ Init_Val, Overflow, False);
Scan_Underscore (Str, P, Ptr, Max, False);
else
exit;
-- Accumulate result, checking for overflow
else
+ Old_Uval := Uval;
+ Old_Overflow := Overflow;
+
if Uval <= Umax then
Uval := 10 * Uval + Digit;
end if;
end if;
+ Lemma_Scan_Digit
+ (Str, P, Last_Num_Init, Digit, 10, Old_Uval, Uval, Init_Val,
+ Old_Overflow, Overflow);
+
P := P + 1;
end if;
end loop;
+ pragma Assert (P = Last_Num_Init + 1);
+ pragma Assert (Init_Val.Overflow = Overflow);
end;
+ pragma Assert_And_Cut
+ (P = Last_Num_Init + 1
+ and then Overflow = Init_Val.Overflow
+ and then (if not Overflow then Init_Val.Value = Uval));
+
Ptr.all := P;
-- Deal with based case. We recognize either the standard '#' or the
UmaxB : constant Uns := Uns'Last / Base;
-- Numbers bigger than UmaxB overflow if multiplied by base
+ Old_Uval : Uns with Ghost;
+ Old_Overflow : Boolean with Ghost;
+
begin
+ pragma Assert
+ (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
+ then Is_Based_Format_Ghost (Str (P .. Max)));
+
-- Loop to scan out based integer value
loop
+
-- We require a digit at this stage
if Str (P) in '0' .. '9' then
else
Uval := Base;
+ Base := 10;
+ pragma Assert (Ptr.all = Last_Num_Init + 1);
+ pragma Assert (if not Overflow then Uval = Init_Val.Value);
exit;
end if;
+ Lemma_Digit_Is_Before_Last (Str, P, Last_Num_Init + 2, Max);
+
+ pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based);
+ pragma Loop_Invariant
+ (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then Digit = Hexa_To_Unsigned_Ghost (Str (P)));
+ pragma Loop_Invariant
+ (if Overflow'Loop_Entry then Overflow);
+ pragma Loop_Invariant
+ (if Overflow then
+ Overflow'Loop_Entry or else Based_Val.Overflow);
+ pragma Loop_Invariant
+ (if not Overflow
+ then Based_Val = Scan_Based_Number_Ghost
+ (Str, P, Last_Num_Based, Base, Uval));
+ pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1);
+
+ Old_Uval := Uval;
+ Old_Overflow := Overflow;
+
-- If digit is too large, just signal overflow and continue.
-- The idea here is to keep scanning as long as the input is
-- syntactically valid, even if we have detected overflow
end if;
end if;
+ Lemma_Scan_Digit
+ (Str, P, Last_Num_Based, Digit, Base, Old_Uval, Uval,
+ Based_Val, Old_Overflow, Overflow);
+
-- If at end of string with no base char, not a based number
-- but we signal Constraint_Error and set the pointer past
-- the end of the field, since this is what the ACVC tests
if Str (P) = Base_Char then
Ptr.all := P + 1;
+ pragma Assert (Ptr.all = Last_Num_Based + 2);
+ Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
+ pragma Assert (if not Overflow then Uval = Based_Val.Value);
exit;
-- Deal with underscore
elsif Str (P) = '_' then
+ Lemma_Scan_Underscore
+ (Str, P, Last_Num_Init + 2, Max, Last_Num_Based, Base,
+ Uval, Based_Val, Overflow, True);
Scan_Underscore (Str, P, Ptr, Max, True);
+ pragma Assert
+ (if not Overflow
+ then Based_Val = Scan_Based_Number_Ghost
+ (Str, P, Last_Num_Based, Base, Uval));
end if;
-
end loop;
end;
+ pragma Assert
+ (if Starts_As_Based then P = Last_Num_Based + 1
+ else P = Last_Num_Init + 2);
+ pragma Assert
+ (Overflow =
+ (Init_Val.Overflow
+ or else Init_Val.Value not in 2 .. 16
+ or else (Starts_As_Based and then Based_Val.Overflow)));
end if;
+ pragma Assert_And_Cut
+ (Overflow =
+ (Init_Val.Overflow
+ or else
+ (Last_Num_Init < Max - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Init_Val.Value not in 2 .. 16)
+ or else (Starts_As_Based and then Based_Val.Overflow))
+ and then
+ (if not Overflow then
+ (if Is_Based then Uval = Based_Val.Value
+ else Uval = Init_Val.Value))
+ and then Ptr.all = First_Exp
+ and then Base in 2 .. 16
+ and then
+ (if not Overflow then
+ (if Is_Based then Base = Init_Val.Value else Base = 10)));
+
-- Come here with scanned unsigned value in Uval. The only remaining
-- required step is to deal with exponent if one is present.
Scan_Exponent (Str, Ptr, Max, Expon);
+ pragma Assert
+ (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
+ then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max)));
+
if Expon /= 0 and then Uval /= 0 then
-- For non-zero value, scale by exponent value. No need to do this
UmaxB : constant Uns := Uns'Last / Base;
-- Numbers bigger than UmaxB overflow if multiplied by base
+ Res_Val : constant Uns_Option :=
+ Exponent_Unsigned_Ghost (Uval, Expon, Base)
+ with Ghost;
begin
for J in 1 .. Expon loop
+ pragma Loop_Invariant
+ (if Overflow'Loop_Entry then Overflow);
+ pragma Loop_Invariant
+ (if Overflow
+ then Overflow'Loop_Entry or else Res_Val.Overflow);
+ pragma Loop_Invariant
+ (if not Overflow
+ then Res_Val = Exponent_Unsigned_Ghost
+ (Uval, Expon - J + 1, Base));
+
+ pragma Assert
+ ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval));
+
if Uval > UmaxB then
Overflow := True;
exit;
Uval := Uval * Base;
end loop;
+ pragma Assert
+ (Overflow = (Init_Val.Overflow
+ or else
+ (Last_Num_Init < Max - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Init_Val.Value not in 2 .. 16)
+ or else (Starts_As_Based and then Based_Val.Overflow)
+ or else Res_Val.Overflow));
+ pragma Assert
+ (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+ pragma Assert
+ (Exponent_Unsigned_Ghost (Uval, 0, Base) = (False, Uval));
+ pragma Assert
+ (if not Overflow then Uval = Res_Val.Value);
+ pragma Assert
+ (if not Overflow then
+ Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
end;
end if;
+ pragma Assert
+ (if Expon = 0 or else Uval = 0 then
+ Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
+ pragma Assert
+ (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+ pragma Assert
+ (if not Overflow then
+ Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
- -- Return result, dealing with sign and overflow
+ -- Return result, dealing with overflow
if Overflow then
Bad_Value (Str);
+ pragma Annotate
+ (GNATprove, Intentional,
+ "call to nonreturning subprogram might be executed",
+ "it is expected that Constraint_Error is raised in case of"
+ & " overflow");
else
- return Uval;
+ Res := Uval;
end if;
end Scan_Raw_Unsigned;
-- Scan_Unsigned --
-------------------
- function Scan_Unsigned
+ procedure Scan_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Uns
+ Max : Integer;
+ Res : out Uns)
is
Start : Positive;
-- Save location of first non-blank character
begin
+ pragma Warnings
+ (Off,
+ """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
Scan_Plus_Sign (Str, Ptr, Max, Start);
+ pragma Warnings
+ (On,
+ """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
if Str (Ptr.all) not in '0' .. '9' then
Ptr.all := Start;
Bad_Value (Str);
end if;
- return Scan_Raw_Unsigned (Str, Ptr, Max);
+ Scan_Raw_Unsigned (Str, Ptr, Max, Res);
end Scan_Unsigned;
--------------------
declare
V : Uns;
P : aliased Integer := Str'First;
+
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last)
+ with Ghost;
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank)
+ with Ghost;
begin
- V := Scan_Unsigned (Str, P'Access, Str'Last);
+ pragma Assert
+ (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+
+ declare
+ P_Acc : constant not null access Integer := P'Access;
+ begin
+ Scan_Unsigned (Str, P_Acc, Str'Last, V);
+ end;
+
+ pragma Assert
+ (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+ pragma Assert
+ (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
+
Scan_Trailing_Blanks (Str, P);
+
+ pragma Assert
+ (Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), V));
return V;
end;
end if;
-- This package contains routines for scanning modular Unsigned
-- values for use in Text_IO.Modular_IO, and the Value attribute.
+-- 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,
+ Subprogram_Variant => Ignore);
+pragma Warnings (Off, "postcondition does not mention function result");
+-- True postconditions are used to avoid inlining for GNATprove
+
+with System.Val_Util; use System.Val_Util;
+
generic
type Uns is mod <>;
package System.Value_U is
pragma Preelaborate;
- function Scan_Raw_Unsigned
+ type Uns_Option (Overflow : Boolean := False) is record
+ case Overflow is
+ when True =>
+ null;
+ when False =>
+ Value : Uns := 0;
+ end case;
+ end record with Ghost;
+
+ function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
+ is
+ (for all J in From .. To =>
+ Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+ with
+ Ghost,
+ Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+ -- Ghost function that returns True if S has only hexadecimal characters
+ -- from index From to index To.
+
+ function Last_Hexa_Ghost (Str : String) return Positive
+ with
+ Ghost,
+ Pre => Str /= ""
+ and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+ Post => Last_Hexa_Ghost'Result in Str'Range
+ and then (if Last_Hexa_Ghost'Result < Str'Last then
+ Str (Last_Hexa_Ghost'Result + 1) not in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+ and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
+ -- Ghost function that returns the index of the last character in S that
+ -- is either an hexadecimal digit or an underscore, which necessarily
+ -- exists given the precondition on Str.
+
+ function Is_Based_Format_Ghost (Str : String) return Boolean
+ is
+ (Str /= ""
+ and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then
+ (declare
+ L : constant Positive := Last_Hexa_Ghost (Str);
+ begin
+ Str (L) /= '_'
+ 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
+ -- based number, consisting in a sequence of hexadecimal digits possibly
+ -- separated by single underscores. It may be followed by other characters.
+
+ function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
+ (case X is
+ when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
+ when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
+ when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
+ when others => raise Program_Error)
+ with
+ Ghost,
+ Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ -- Ghost function that computes the value corresponding to an hexadecimal
+ -- digit.
+
+ function Scan_Overflows_Ghost
+ (Digit : Uns;
+ Base : Uns;
+ Acc : Uns) return Boolean
+ is
+ (Digit >= Base
+ or else Acc > Uns'Last / Base
+ or else Uns'Last - Digit < Base * Acc)
+ with Ghost;
+ -- Ghost function which returns True if Digit + Base * Acc overflows or
+ -- Digit is greater than Base, as this is used by the algorithm for the
+ -- test of overflow.
+
+ function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0) return Uns_Option
+ with
+ Ghost,
+ Subprogram_Variant => (Increases => From),
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To);
+ -- Ghost function that recursively computes the based number in Str,
+ -- assuming Acc has been scanned already and scanning continues at index
+ -- From.
+
+ function Exponent_Unsigned_Ghost
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10) return Uns_Option
+ with
+ Ghost,
+ Subprogram_Variant => (Decreases => Exp);
+ -- Ghost function that recursively computes Value * Base ** Exp
+
+ function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
+ (Is_Natural_Format_Ghost (Str)
+ and then
+ (declare
+ Last_Num_Init : constant Integer := Last_Number_Ghost (Str);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < Str'Last - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < Str'Last
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ begin
+ (if Starts_As_Based then
+ Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+ and then Last_Num_Based < Str'Last)
+ and then Is_Opt_Exponent_Format_Ghost
+ (Str (First_Exp .. Str'Last))))
+ with
+ Ghost,
+ Pre => Str'Last /= Positive'Last,
+ Post => True;
+ -- Ghost function that determines if Str has the correct format for an
+ -- unsigned number without a sign character.
+ -- It is a natural number in base 10, optionally followed by a based
+ -- number surrounded by delimiters # or :, optionally followed by an
+ -- exponent part.
+
+ function Raw_Unsigned_Overflows_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Init_Val : constant Uns_Option :=
+ Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ Based_Val : constant Uns_Option :=
+ (if Starts_As_Based and then not Init_Val.Overflow
+ then Scan_Based_Number_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+ else Init_Val);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ Expon : constant Natural :=
+ (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ then Scan_Exponent_Ghost (Str (First_Exp .. To))
+ else 0);
+ begin
+ Init_Val.Overflow
+ or else
+ (Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Init_Val.Value not in 2 .. 16)
+ or else
+ (Starts_As_Based
+ and then Based_Val.Overflow)
+ or else
+ (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ and then
+ (declare
+ Base : constant Uns :=
+ (if Is_Based then Init_Val.Value else 10);
+ Value : constant Uns :=
+ (if Is_Based then Based_Val.Value else Init_Val.Value);
+ begin
+ Exponent_Unsigned_Ghost
+ (Value, Expon, Base).Overflow)))
+ with
+ Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9',
+ Post => True;
+ -- Ghost function that determines if the computation of the unsigned number
+ -- represented by Str will overflow. The computation overflows if either:
+ -- * The computation of the decimal part overflows,
+ -- * The decimal part is followed by a valid delimiter for a based
+ -- part, and the number corresponding to the base is not a valid base,
+ -- * The computation of the based part overflows, or
+ -- * There is an exponent and the computation of the exponentiation
+ -- overflows.
+
+ function Scan_Raw_Unsigned_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Uns
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Init_Val : constant Uns_Option :=
+ Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ Based_Val : constant Uns_Option :=
+ (if Starts_As_Based and then not Init_Val.Overflow
+ then Scan_Based_Number_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+ else Init_Val);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ Expon : constant Natural :=
+ (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ then Scan_Exponent_Ghost (Str (First_Exp .. To))
+ else 0);
+ Base : constant Uns :=
+ (if Is_Based then Init_Val.Value else 10);
+ Value : constant Uns :=
+ (if Is_Based then Based_Val.Value else Init_Val.Value);
+ begin
+ Exponent_Unsigned_Ghost (Value, Expon, Base).Value)
+ with
+ Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9'
+ and then not Raw_Unsigned_Overflows_Ghost (Str, From, To),
+ Post => True;
+ -- Ghost function that scans an unsigned number without a sign character
+
+ function Raw_Unsigned_Last_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Positive
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ begin
+ (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ then First_Exp
+ elsif Str (First_Exp + 1) in '-' | '+' then
+ Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
+ else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
+ with
+ Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9',
+ Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1;
+ -- Ghost function that returns the position of the cursor once an unsigned
+ -- number has been seen.
+
+ procedure Scan_Raw_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Uns;
+ Max : Integer;
+ Res : out Uns)
+ with Pre => Str'Last /= Positive'Last
+ and then Ptr.all in Str'Range
+ and then Max in Ptr.all .. Str'Last
+ and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
+ Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max)
+ and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
+ and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
+
-- This function scans the string starting at Str (Ptr.all) for a valid
-- integer according to the syntax described in (RM 3.5(43)). The substring
-- scanned extends no further than Str (Max). Note: this does not scan
-- Note: if Str is empty, i.e. if Max is less than Ptr, then this is a
-- special case of an all-blank string, and Ptr is unchanged, and hence
-- is greater than Max as required in this case.
+ -- ??? This is not the case. We will read Str (Ptr.all) without checking
+ -- and increase Ptr.all by one.
--
-- Note: this routine should not be called with Str'Last = Positive'Last.
-- If this occurs Program_Error is raised with a message noting that this
-- case is not supported. Most such cases are eliminated by the caller.
- function Scan_Unsigned
+ procedure Scan_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Uns;
+ Max : Integer;
+ Res : out Uns)
+ with Pre => Str'Last /= Positive'Last
+ and then Ptr.all in Str'Range
+ and then Max in Ptr.all .. Str'Last
+ and then not Only_Space_Ghost (Str, Ptr.all, Max)
+ and then
+ (declare
+ Non_Blank : constant Positive :=
+ First_Non_Space_Ghost (Str, Ptr.all, Max);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
+ Post =>
+ (declare
+ Non_Blank : constant Positive :=
+ First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
+ and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
+ and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+
-- Same as Scan_Raw_Unsigned, except scans optional leading
-- blanks, and an optional leading plus sign.
--
-- Note: if a minus sign is present, Constraint_Error will be raised.
-- Note: trailing blanks are not scanned.
+ function Slide_To_1 (Str : String) return String
+ with Ghost,
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ (for all J in Str'First .. Str'Last =>
+ Slide_To_1'Result (J - Str'First + 1) = ' ');
+ -- Slides Str so that it starts at 1
+
+ function Slide_If_Necessary (Str : String) return String is
+ (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
+ with Ghost,
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ Only_Space_Ghost (Slide_If_Necessary'Result,
+ Slide_If_Necessary'Result'First,
+ Slide_If_Necessary'Result'Last);
+ -- If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+ function Is_Unsigned_Ghost (Str : String) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+ and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
+ and then Only_Space_Ghost
+ (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+ with Ghost,
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last,
+ Post => True;
+ -- Ghost function that determines if Str has the correct format for an
+ -- unsigned number, consisting in some blank characters, an optional
+ -- + sign, a raw unsigned number which does not overflow and then some
+ -- more blank characters.
+
+ function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+ with Ghost,
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last
+ and then Is_Unsigned_Ghost (Str),
+ Post => True;
+ -- Ghost function that returns True if Val is the value corresponding to
+ -- the unsigned number represented by Str.
+
function Value_Unsigned
- (Str : String) return Uns;
+ (Str : String) return Uns
+ with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Length /= Positive'Last
+ and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)),
+ Post =>
+ Is_Value_Unsigned_Ghost
+ (Slide_If_Necessary (Str), Value_Unsigned'Result),
+ Subprogram_Variant => (Decreases => Str'First);
-- Used in computing X'Value (Str) where X is a modular integer type whose
-- modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str
-- is the string argument of the attribute. Constraint_Error is raised if
-- the string is malformed, or if the value is out of range.
+private
+
+ -----------------------------
+ -- Exponent_Unsigned_Ghost --
+ -----------------------------
+
+ function Exponent_Unsigned_Ghost
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10) return Uns_Option
+ is
+ (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
+ elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
+ else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+
+ -----------------------------
+ -- Scan_Based_Number_Ghost --
+ -----------------------------
+
+ function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0) return Uns_Option
+ is
+ (if From > To then (Overflow => False, Value => Acc)
+ elsif Str (From) = '_'
+ then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
+ elsif Scan_Overflows_Ghost
+ (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+ then (Overflow => True)
+ else Scan_Based_Number_Ghost
+ (Str, From + 1, To, Base,
+ Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+
+ ----------------
+ -- Slide_To_1 --
+ ----------------
+
+ function Slide_To_1 (Str : String) return String is
+ (declare
+ Res : constant String (1 .. Str'Length) := Str;
+ begin
+ Res);
+
end System.Value_U;
-- This package contains routines for scanning modular Unsigned
-- values for use in Text_IO.Modular_IO, and the Value attribute.
+-- 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,
+ Subprogram_Variant => Ignore);
+
with System.Unsigned_Types;
with System.Value_U;
-package System.Val_Uns is
+package System.Val_Uns with SPARK_Mode is
pragma Preelaborate;
subtype Unsigned is Unsigned_Types.Unsigned;
package Impl is new Value_U (Unsigned);
- function Scan_Raw_Unsigned
+ procedure Scan_Raw_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Unsigned
+ Max : Integer;
+ Res : out Unsigned)
renames Impl.Scan_Raw_Unsigned;
- function Scan_Unsigned
+ procedure Scan_Unsigned
(Str : String;
Ptr : not null access Integer;
- Max : Integer) return Unsigned
+ Max : Integer;
+ Res : out Unsigned)
renames Impl.Scan_Unsigned;
function Value_Unsigned
-- First_Non_Space_Ghost --
---------------------------
- function First_Non_Space_Ghost (S : String) return Positive is
+ function First_Non_Space_Ghost
+ (S : String;
+ From, To : Integer) return Positive
+ is
begin
- for J in S'Range loop
+ for J in From .. To loop
if S (J) /= ' ' then
return J;
end if;
- pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
+ pragma Loop_Invariant (for all K in From .. J => S (K) = ' ');
end loop;
raise Program_Error;
Exp := 0;
return;
end if;
+ pragma Annotate
+ (CodePeer, False_Positive, "test always false",
+ "the slice might be empty or not start with an 'e'");
-- We have an E/e, see if sign follows
pragma Assert (Is_Natural_Format_Ghost (Rest));
loop
- pragma Assert (Str (P) = Rest (P));
pragma Assert (Str (P) in '0' .. '9');
if X < (Integer'Last / 10) then
end if;
pragma Loop_Invariant (X >= 0);
- pragma Loop_Invariant (P in P'Loop_Entry .. Last);
+ pragma Loop_Invariant (P in Rest'First .. 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)));
+ (Scan_Natural_Ghost (Rest, Rest'First, 0)
+ = Scan_Natural_Ghost (Rest, P + 1, X));
P := P + 1;
exit when Str (P) not in '0' .. '9';
end if;
end loop;
+
+ pragma Assert (P = Last + 1);
end;
if M then
Start := P;
- pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+ pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
-- Skip past an initial plus sign
Start := P;
- pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+ pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
-- Remember an initial minus sign
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
+pragma Warnings (Off, "postcondition does not mention function result");
+-- True postconditions are used to avoid inlining for GNATprove
with System.Case_Util;
(for all J in From .. To => S (J) = ' ')
with
Ghost,
- Pre => From > To or else (From >= S'First and then To <= S'Last);
+ Pre => From > To or else (From >= S'First and then To <= S'Last),
+ Post => True;
-- 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
+ function First_Non_Space_Ghost
+ (S : String;
+ From, To : Integer) return Positive
with
Ghost,
- Pre => not Only_Space_Ghost (S, S'First, S'Last),
- Post => First_Non_Space_Ghost'Result in S'Range
+ Pre => From in S'Range
+ and then To in S'Range
+ and then not Only_Space_Ghost (S, From, To),
+ Post => First_Non_Space_Ghost'Result in From .. To
and then S (First_Non_Space_Ghost'Result) /= ' '
and then Only_Space_Ghost
- (S, S'First, First_Non_Space_Ghost'Result - 1);
+ (S, From, 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.
and then
(declare
F : constant Positive :=
- First_Non_Space_Ghost (Str (Ptr.all .. Max));
+ 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));
+ 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
(declare
F : constant Positive :=
- First_Non_Space_Ghost (Str (Ptr.all .. Max));
+ 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));
+ First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
begin
Ptr.all = (if Str (F) = '+' then F + 1 else F)
and then Start = F);
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.
+ -- precondition on Str.
function Is_Natural_Format_Ghost (Str : String) return Boolean is
(Str /= ""
function Starts_As_Exponent_Format_Ghost
(Str : String;
- Real : Boolean) return Boolean
+ Real : Boolean := False) return Boolean
is
(Str'Length > 1
and then Str (Str'First) in 'E' | 'e'
function Is_Opt_Exponent_Format_Ghost
(Str : String;
- Real : Boolean) return Boolean
+ Real : Boolean := False) return Boolean
is
(not Starts_As_Exponent_Format_Ghost (Str, Real)
or else
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;
+ Pre => Str /= "" and then Str (Str'First) in '0' .. '9'
+ and then Str'Last < Natural'Last
+ and then P in Str'First .. Last_Number_Ghost (Str) + 1;
-- 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.
+ function Scan_Exponent_Ghost
+ (Str : String;
+ Real : Boolean := False)
+ return Integer
+ is
+ (declare
+ Plus_Sign : constant Boolean := Str (Str'First + 1) = '+';
+ Minus_Sign : constant Boolean := Str (Str'First + 1) = '-';
+ Sign : constant Boolean := Plus_Sign or Minus_Sign;
+ Start : constant Natural :=
+ (if Sign then Str'First + 2 else Str'First + 1);
+ Value : constant Natural :=
+ Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0);
+ begin
+ (if Minus_Sign then -Value else Value))
+ with
+ Ghost,
+ Pre => Str'Last < Natural'Last
+ and then Starts_As_Exponent_Format_Ghost (Str, Real),
+ Post => (if not Real then Scan_Exponent_Ghost'Result >= 0);
+ -- Ghost function that scans an exponent
+
procedure Scan_Exponent
(Str : String;
Ptr : not null access Integer;
and then Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real),
Post =>
(if Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real)
- 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;
- 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))
+ then Exp = Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real)
+ and then
+ (if Str (Ptr.all'Old + 1) in '-' | '+' then
+ Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1
+ else Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1)
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
Str (P + 1) in '0' .. '9'),
Post =>
P = P'Old + 1
- and then Ptr.all = Ptr.all;
+ and then Ptr.all'Old = Ptr.all;
-- Called if an underscore is encountered while scanning digits. Str (P)
-- contains the underscore. Ptr is the pointer to be returned to the
-- ultimate caller of the scan routine, Max is the maximum subscript in
Acc : Natural)
return Natural
is
- (if Str (P) = '_' then
+ (if P > Str'Last
+ or else Str (P) not in '0' .. '9' | '_'
+ or else Acc >= Integer'Last / 10
+ then
+ Acc
+ elsif 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'));
+ Acc * 10 +
+ (Integer'(Character'Pos (Str (P))) -
+ Integer'(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))));
+ Scan_Natural_Ghost (Str, P + 1, Shift_Acc)));
end System.Val_Util;
projects / thirdparty / gcc.git / commitdiff
