| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT COMPILER COMPONENTS -- |
| -- -- |
| -- S Y S T E M . V A L U E _ U _ S P E C -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 2022-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| -- This package contains the specification entities using for the formal |
| -- verification of the routines for scanning modular Unsigned values. |
| |
| -- 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.Val_Util; use System.Val_Util; |
| |
| generic |
| |
| type Uns is mod <>; |
| |
| package System.Value_U_Spec with |
| Ghost, |
| SPARK_Mode, |
| Annotate => (GNATprove, Always_Return) |
| is |
| pragma Preelaborate; |
| |
| type Uns_Option (Overflow : Boolean := False) is record |
| case Overflow is |
| when True => |
| null; |
| when False => |
| Value : Uns := 0; |
| end case; |
| end record; |
| |
| function Wrap_Option (Value : Uns) return Uns_Option is |
| (Overflow => False, Value => Value); |
| |
| function Only_Decimal_Ghost |
| (Str : String; |
| From, To : Integer) |
| return Boolean |
| is |
| (for all J in From .. To => Str (J) in '0' .. '9') |
| with |
| Pre => From > To or else (From >= Str'First and then To <= Str'Last); |
| -- Ghost function that returns True if S has only decimal characters |
| -- from index From to index To. |
| |
| 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 |
| 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 |
| 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) /= '_')))); |
| -- 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 |
| 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); |
| -- 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 |
| 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. |
| |
| -- Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost |
| |
| procedure Lemma_Scan_Based_Number_Ghost_Base |
| (Str : String; |
| From, To : Integer; |
| Base : Uns := 10; |
| Acc : Uns := 0) |
| with |
| Global => null, |
| 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), |
| Post => |
| (if From > To |
| then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = |
| (Overflow => False, Value => Acc)); |
| -- Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To |
| |
| procedure Lemma_Scan_Based_Number_Ghost_Underscore |
| (Str : String; |
| From, To : Integer; |
| Base : Uns := 10; |
| Acc : Uns := 0) |
| with |
| Global => null, |
| 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), |
| Post => |
| (if From <= To and then Str (From) = '_' |
| then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = |
| Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)); |
| -- Underscore case: underscores are ignored while scanning |
| |
| procedure Lemma_Scan_Based_Number_Ghost_Overflow |
| (Str : String; |
| From, To : Integer; |
| Base : Uns := 10; |
| Acc : Uns := 0) |
| with |
| Global => null, |
| 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), |
| Post => |
| (if From <= To |
| and then Str (From) /= '_' |
| and then Scan_Overflows_Ghost |
| (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) |
| then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = |
| (Overflow => True)); |
| -- Overflow case: scanning a digit which causes an overflow |
| |
| procedure Lemma_Scan_Based_Number_Ghost_Step |
| (Str : String; |
| From, To : Integer; |
| Base : Uns := 10; |
| Acc : Uns := 0) |
| with |
| Global => null, |
| 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), |
| Post => |
| (if From <= To |
| and then Str (From) /= '_' |
| and then not Scan_Overflows_Ghost |
| (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) |
| then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = |
| Scan_Based_Number_Ghost |
| (Str, From + 1, To, Base, |
| Base * Acc + Hexa_To_Unsigned_Ghost (Str (From)))); |
| -- Normal case: scanning a digit without overflows |
| |
| function Exponent_Unsigned_Ghost |
| (Value : Uns; |
| Exp : Natural; |
| Base : Uns := 10) return Uns_Option |
| with |
| Subprogram_Variant => (Decreases => Exp); |
| -- Ghost function that recursively computes Value * Base ** Exp |
| |
| -- Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost |
| |
| procedure Lemma_Exponent_Unsigned_Ghost_Base |
| (Value : Uns; |
| Exp : Natural; |
| Base : Uns := 10) |
| with |
| Post => |
| (if Exp = 0 or Value = 0 |
| then Exponent_Unsigned_Ghost (Value, Exp, Base) = |
| (Overflow => False, Value => Value)); |
| -- Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0 |
| |
| procedure Lemma_Exponent_Unsigned_Ghost_Overflow |
| (Value : Uns; |
| Exp : Natural; |
| Base : Uns := 10) |
| with |
| Post => |
| (if Exp /= 0 |
| and then Value /= 0 |
| and then Scan_Overflows_Ghost (0, Base, Value) |
| then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True)); |
| -- Overflow case: the next multiplication overflows |
| |
| procedure Lemma_Exponent_Unsigned_Ghost_Step |
| (Value : Uns; |
| Exp : Natural; |
| Base : Uns := 10) |
| with |
| Post => |
| (if Exp /= 0 |
| and then Value /= 0 |
| and then not Scan_Overflows_Ghost (0, Base, Value) |
| then Exponent_Unsigned_Ghost (Value, Exp, Base) = |
| Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); |
| -- Normal case: exponentiation without overflows |
| |
| 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 |
| Pre => Str'Last /= Positive'Last; |
| -- 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. |
| |
| type Split_Value_Ghost is record |
| Value : Uns; |
| Base : Uns; |
| Expon : Natural; |
| end record; |
| |
| function Scan_Split_No_Overflow_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); |
| 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); |
| begin |
| not Init_Val.Overflow |
| and then |
| (Last_Num_Init >= To - 1 |
| or else Str (Last_Num_Init + 1) not in '#' | ':' |
| or else Init_Val.Value in 2 .. 16) |
| and then |
| (not Starts_As_Based |
| or else not Based_Val.Overflow)) |
| with |
| 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'; |
| -- Ghost function that determines if an overflow might occur while scanning |
| -- the representation of an unsigned number. 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, |
| -- or |
| -- * The computation of the based part overflows. |
| |
| pragma Warnings (Off, "constant * is not referenced"); |
| function Scan_Split_Value_Ghost |
| (Str : String; |
| From, To : Integer) |
| return Split_Value_Ghost |
| 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 |
| (Value => Value, Base => Base, Expon => Expon)) |
| with |
| 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 Scan_Split_No_Overflow_Ghost (Str, From, To); |
| -- Ghost function that scans an unsigned number without a sign character |
| -- and return a record containing the values scanned for its value, its |
| -- base, and its exponent. |
| pragma Warnings (On, "constant * is not referenced"); |
| |
| function Raw_Unsigned_No_Overflow_Ghost |
| (Str : String; |
| From, To : Integer) |
| return Boolean |
| is |
| (Scan_Split_No_Overflow_Ghost (Str, From, To) |
| and then |
| (declare |
| Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost |
| (Str, From, To); |
| begin |
| not Exponent_Unsigned_Ghost |
| (Val.Value, Val.Expon, Val.Base).Overflow)) |
| with |
| 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'; |
| -- Ghost function that determines if the computation of the unsigned number |
| -- represented by Str will overflow. The computation overflows if either: |
| -- * The scan of the string overflows, or |
| -- * The computation of the exponentiation overflows. |
| |
| function Scan_Raw_Unsigned_Ghost |
| (Str : String; |
| From, To : Integer) |
| return Uns |
| is |
| (declare |
| Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost |
| (Str, From, To); |
| begin |
| Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value) |
| with |
| 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 Raw_Unsigned_No_Overflow_Ghost (Str, From, To); |
| -- 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 |
| 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'; |
| -- Ghost function that returns the position of the cursor once an unsigned |
| -- number has been seen. |
| |
| function Slide_To_1 (Str : String) return String |
| with |
| 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); |
| -- 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 Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last) |
| and then Only_Space_Ghost |
| (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) |
| with |
| Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) |
| and then Str'Last /= Positive'Last; |
| -- 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 |
| Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) |
| and then Str'Last /= Positive'Last |
| and then Is_Unsigned_Ghost (Str); |
| -- Ghost function that returns True if Val is the value corresponding to |
| -- the unsigned number represented by Str. |
| |
| procedure Prove_Scan_Based_Number_Ghost_Eq |
| (Str1, Str2 : String; |
| From, To : Integer; |
| Base : Uns := 10; |
| Acc : Uns := 0) |
| with |
| Subprogram_Variant => (Increases => From), |
| Pre => Str1'Last /= Positive'Last |
| and then Str2'Last /= Positive'Last |
| and then |
| (From > To or else (From >= Str1'First and then To <= Str1'Last)) |
| and then |
| (From > To or else (From >= Str2'First and then To <= Str2'Last)) |
| and then Only_Hexa_Ghost (Str1, From, To) |
| and then (for all J in From .. To => Str1 (J) = Str2 (J)), |
| Post => |
| Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) |
| = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); |
| -- Scan_Based_Number_Ghost returns the same value on two slices which are |
| -- equal. |
| |
| procedure Prove_Scan_Only_Decimal_Ghost |
| (Str : String; |
| Val : Uns) |
| with |
| Pre => Str'Last /= Positive'Last |
| and then Str'Length >= 2 |
| and then Str (Str'First) = ' ' |
| and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) |
| and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) |
| = Wrap_Option (Val), |
| Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str)) |
| and then |
| Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val); |
| -- Ghost lemma used in the proof of 'Image implementation, to prove that |
| -- the result of Value_Unsigned on a decimal string is the same as the |
| -- result of Scan_Based_Number_Ghost. |
| |
| -- Bundle Uns type with other types, constants and subprograms used in |
| -- ghost code, so that this package can be instantiated once and used |
| -- multiple times as generic formal for a given Int type. |
| |
| package Uns_Params is new System.Val_Util.Uns_Params |
| (Uns => Uns, |
| P_Uns_Option => Uns_Option, |
| P_Wrap_Option => Wrap_Option, |
| P_Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost, |
| P_Scan_Overflows_Ghost => Scan_Overflows_Ghost, |
| P_Is_Raw_Unsigned_Format_Ghost => |
| Is_Raw_Unsigned_Format_Ghost, |
| P_Scan_Split_No_Overflow_Ghost => |
| Scan_Split_No_Overflow_Ghost, |
| P_Raw_Unsigned_No_Overflow_Ghost => |
| Raw_Unsigned_No_Overflow_Ghost, |
| P_Exponent_Unsigned_Ghost => Exponent_Unsigned_Ghost, |
| P_Lemma_Exponent_Unsigned_Ghost_Base => |
| Lemma_Exponent_Unsigned_Ghost_Base, |
| P_Lemma_Exponent_Unsigned_Ghost_Overflow => |
| Lemma_Exponent_Unsigned_Ghost_Overflow, |
| P_Lemma_Exponent_Unsigned_Ghost_Step => |
| Lemma_Exponent_Unsigned_Ghost_Step, |
| P_Scan_Raw_Unsigned_Ghost => Scan_Raw_Unsigned_Ghost, |
| P_Lemma_Scan_Based_Number_Ghost_Base => |
| Lemma_Scan_Based_Number_Ghost_Base, |
| P_Lemma_Scan_Based_Number_Ghost_Underscore => |
| Lemma_Scan_Based_Number_Ghost_Underscore, |
| P_Lemma_Scan_Based_Number_Ghost_Overflow => |
| Lemma_Scan_Based_Number_Ghost_Overflow, |
| P_Lemma_Scan_Based_Number_Ghost_Step => |
| Lemma_Scan_Based_Number_Ghost_Step, |
| P_Raw_Unsigned_Last_Ghost => Raw_Unsigned_Last_Ghost, |
| P_Only_Decimal_Ghost => Only_Decimal_Ghost, |
| P_Scan_Based_Number_Ghost => Scan_Based_Number_Ghost, |
| P_Is_Unsigned_Ghost => |
| Is_Unsigned_Ghost, |
| P_Is_Value_Unsigned_Ghost => |
| Is_Value_Unsigned_Ghost, |
| P_Prove_Scan_Only_Decimal_Ghost => |
| Prove_Scan_Only_Decimal_Ghost, |
| P_Prove_Scan_Based_Number_Ghost_Eq => |
| Prove_Scan_Based_Number_Ghost_Eq); |
| |
| private |
| |
| ---------------- |
| -- 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_Spec; |
