------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S Y S T E M . V A L U E _ U _ S P E C --
-- --
-- B o d y --
-- --
-- Copyright (C) 2022-2023, 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. --
-- --
------------------------------------------------------------------------------
pragma Assertion_Policy (Pre => Ignore,
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore,
Subprogram_Variant => Ignore);
package body System.Value_U_Spec with SPARK_Mode is
-----------------------------
-- 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));
---------------------
-- 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;
-----------------------------
-- Lemmas with null bodies --
-----------------------------
procedure Lemma_Scan_Based_Number_Ghost_Base
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is null;
procedure Lemma_Scan_Based_Number_Ghost_Underscore
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is null;
procedure Lemma_Scan_Based_Number_Ghost_Overflow
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is null;
procedure Lemma_Scan_Based_Number_Ghost_Step
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is null;
procedure Lemma_Exponent_Unsigned_Ghost_Base
(Value : Uns;
Exp : Natural;
Base : Uns := 10)
is null;
procedure Lemma_Exponent_Unsigned_Ghost_Overflow
(Value : Uns;
Exp : Natural;
Base : Uns := 10)
is null;
procedure Lemma_Exponent_Unsigned_Ghost_Step
(Value : Uns;
Exp : Natural;
Base : Uns := 10)
is null;
--------------------------------------
-- Prove_Scan_Based_Number_Ghost_Eq --
--------------------------------------
procedure Prove_Scan_Based_Number_Ghost_Eq
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is
begin
if From > To then
null;
elsif Str1 (From) = '_' then
Prove_Scan_Based_Number_Ghost_Eq
(Str1, Str2, From + 1, To, Base, Acc);
elsif Scan_Overflows_Ghost
(Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
then
null;
else
Prove_Scan_Based_Number_Ghost_Eq
(Str1, Str2, From + 1, To, Base,
Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
end if;
end Prove_Scan_Based_Number_Ghost_Eq;
-----------------------------------
-- Prove_Scan_Only_Decimal_Ghost --
-----------------------------------
procedure Prove_Scan_Only_Decimal_Ghost
(Str : String;
Val : Uns)
is
pragma Assert (Str (Str'First + 1) /= ' ');
Non_Blank : constant Positive := First_Non_Space_Ghost
(Str, Str'First, Str'Last);
pragma Assert (Non_Blank = Str'First + 1);
Fst_Num : constant Positive :=
(if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
pragma Assert (Fst_Num = Str'First + 1);
begin
pragma Assert
(Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
pragma Assert
(Scan_Split_No_Overflow_Ghost (Str, Str'First + 1, Str'Last));
pragma Assert
((Val, 10, 0) = Scan_Split_Value_Ghost (Str, Str'First + 1, Str'Last));
pragma Assert
(Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
pragma Assert (Is_Unsigned_Ghost (Str));
pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
end Prove_Scan_Only_Decimal_Ghost;
-----------------------------
-- 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))));
end System.Value_U_Spec;