OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Proof of System.Val_Uns at gold level

Browse Source 
gcc/ada/

	* libgnat/a-tiinau.ads: Use a procedure for the Scan parameter
	instead of a function with side-effects.
	* libgnat/a-tiinau.adb: Idem.
	* libgnat/a-wtinau.ads: Idem.
	* libgnat/a-wtinau.adb: Idem.
	* libgnat/a-ztinau.ads: Idem.
	* libgnat/a-ztinau.adb: Idem.
	* libgnat/s-valint.ads: Change the function with side-effects
	Scan_Integer into a procedure
	* libgnat/s-vallli.ads: Idem.
	* libgnat/s-valllli.ads: Idem.
	* libgnat/s-vallllu.ads: Add SPARK_Mode and pragma to ignore
	assertions in instance.
	* libgnat/s-valllu.ads: Idem.
	* libgnat/s-valuns.ads: Idem.
	* libgnat/s-valuei.ads: Use a procedure for the
	Scan_Raw_Unsigned parameter instead of a function with
	side-effects and change the function with side-effects
	Scan_Integer into a procedure.
	* libgnat/s-valuei.adb: Idem.
	* libgnat/s-valuti.ads: Introduce a ghost function that scans an
	exponent and complete the postcondition of Scan_Exponent to also
	describe the value of Ptr after the call. Fix the postcondition
	of Scan_Underscore. Simplify the definition of
	Scan_Natural_Ghost.
	* libgnat/s-valuti.adb: Idem.
	* libgnat/s-valboo.ads, libgnat/s-valboo.adb: Update calls to
	First_Non_Space_Ghost.
	* libgnat/s-valueu.ads: Add functional contracts.
	* libgnat/s-valueu.adb: Idem.
This commit is contained in:
Claire Dross 2021-12-15 20:10:06 +01:00 committed by Pierre-Marie de Rodat
parent 371b4ad7c4
commit 649b3efae5
20 changed files with 1066 additions and 115 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
gcc/ada/libgnat/a-tiinau.adb
View File

@ -54,7 +54,7 @@ package body Ada.Text_IO.Integer_Aux is
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;
@ -71,7 +71,7 @@ package body Ada.Text_IO.Integer_Aux is
begin
String_Skip (From, Pos);
Item := Scan (From, Pos'Access, From'Last);
Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception

7
gcc/ada/libgnat/a-tiinau.ads
View File

@ -38,8 +38,11 @@
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

4
gcc/ada/libgnat/a-wtinau.adb
View File

@ -54,7 +54,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is
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;
@ -71,7 +71,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is
begin
String_Skip (From, Pos);
Item := Scan (From, Pos'Access, From'Last);
Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception

7
gcc/ada/libgnat/a-wtinau.ads
View File

@ -38,8 +38,11 @@
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

4
gcc/ada/libgnat/a-ztinau.adb
View File

@ -54,7 +54,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is
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;
@ -71,7 +71,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is
begin
String_Skip (From, Pos);
Item := Scan (From, Pos'Access, From'Last);
Scan (From, Pos'Access, From'Last, Item);
Last := Pos - 1;
exception

7
gcc/ada/libgnat/a-ztinau.ads
View File

@ -38,8 +38,11 @@
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

3
gcc/ada/libgnat/s-valboo.adb
View File

@ -55,7 +55,8 @@ is
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;

6
gcc/ada/libgnat/s-valboo.ads
View File

@ -51,7 +51,8 @@ is
(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'
@ -82,7 +83,8 @@ is
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;

5
gcc/ada/libgnat/s-valint.ads
View File

@ -43,10 +43,11 @@ package System.Val_Int is
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

5
gcc/ada/libgnat/s-vallli.ads
View File

@ -46,10 +46,11 @@ package System.Val_LLI is
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

5
gcc/ada/libgnat/s-valllli.ads
View File

@ -46,10 +46,11 @@ package System.Val_LLLI is
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

24
gcc/ada/libgnat/s-vallllu.ads
View File

@ -32,26 +32,40 @@
-- 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

24
gcc/ada/libgnat/s-valllu.ads
View File

@ -32,26 +32,40 @@
-- 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

15
gcc/ada/libgnat/s-valuei.adb
View File

@ -37,10 +37,11 @@ package body System.Value_I is
-- 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
@ -59,13 +60,13 @@ package body System.Value_I is
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;
@ -73,12 +74,12 @@ package body System.Value_I is
-- 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;
@ -106,7 +107,7 @@ package body System.Value_I is
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;

12
gcc/ada/libgnat/s-valuei.ads
View File

@ -38,19 +38,21 @@ generic
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:

436
gcc/ada/libgnat/s-valueu.adb
View File

@ -29,18 +29,220 @@
-- --
------------------------------------------------------------------------------
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
@ -63,6 +265,40 @@ package body System.Value_U is
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
@ -85,9 +321,20 @@ package body System.Value_U is
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');
@ -96,6 +343,9 @@ package body System.Value_U is
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;
@ -104,6 +354,9 @@ package body System.Value_U is
-- Accumulate result, checking for overflow
else
Old_Uval := Uval;
Old_Overflow := Overflow;
if Uval <= Umax then
Uval := 10 * Uval + Digit;
@ -118,11 +371,22 @@ package body System.Value_U is
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
@ -153,10 +417,18 @@ package body System.Value_U is
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
@ -177,9 +449,32 @@ package body System.Value_U is
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
@ -203,6 +498,10 @@ package body System.Value_U is
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
@ -219,23 +518,62 @@ package body System.Value_U is
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
@ -246,8 +584,24 @@ package body System.Value_U is
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;
@ -255,15 +609,45 @@ package body System.Value_U is
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;
@ -271,23 +655,30 @@ package body System.Value_U is
-- 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;
--------------------
@ -313,9 +704,32 @@ package body System.Value_U is
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;

462
gcc/ada/libgnat/s-valueu.ads
View File

@ -32,6 +32,22 @@
-- 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 <>;
@ -39,10 +55,314 @@ generic
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
@ -106,26 +426,158 @@ package System.Value_U is
-- 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;

24
gcc/ada/libgnat/s-valuns.ads
View File

@ -32,26 +32,40 @@
-- 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

31
gcc/ada/libgnat/s-valuti.adb
View File

@ -66,14 +66,17 @@ is
-- 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;
@ -172,6 +175,9 @@ is
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
@ -222,7 +228,6 @@ is
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
@ -230,17 +235,11 @@ is
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;
@ -252,6 +251,8 @@ is
exit when Str (P) not in '0' .. '9';
end if;
end loop;
pragma Assert (P = Last + 1);
end;
if M then
@ -298,7 +299,7 @@ is
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
@ -354,7 +355,7 @@ is
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

96
gcc/ada/libgnat/s-valuti.ads
View File

@ -41,6 +41,8 @@ pragma Assertion_Policy (Pre => Ignore,
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;
@ -59,18 +61,23 @@ is
(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.
@ -117,14 +124,14 @@ is
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)
@ -162,14 +169,14 @@ is
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);
@ -195,7 +202,7 @@ is
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 /= ""
@ -215,7 +222,7 @@ is
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'
@ -242,7 +249,7 @@ is
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
@ -265,13 +272,35 @@ is
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;
@ -286,17 +315,11 @@ is
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
@ -340,7 +363,7 @@ is
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
@ -365,19 +388,20 @@ private
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;