From: Claire Dross <dr...@adacore.com>
Introduce new ghost helper functions to facilitate proof.
gcc/ada/
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Use new helpers.
* libgnat/s-vauspe.ads (Raw_Unsigned_Starts_As_Based_Ghost,
Raw_Unsigned_Is_Based_Ghost): New ghost helper functions.
(Is_Raw_Unsigned_Format_Ghost, Scan_Split_No_Overflow_Ghost,
Scan_Split_Value_Ghost, Raw_Unsigned_Last_Ghost): Use new
helpers.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/s-valueu.adb | 10 ++----
gcc/ada/libgnat/s-vauspe.ads | 63 ++++++++++++++++++++++--------------
2 files changed, 41 insertions(+), 32 deletions(-)
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index 062ad33b1e9..9c77caa3bcb 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -140,10 +140,7 @@ package body System.Value_U is
Spec.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'
+ Spec.Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Max)
with Ghost;
Last_Num_Based : constant Integer :=
(if Starts_As_Based
@@ -151,9 +148,8 @@ package body System.Value_U is
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)
+ Spec.Raw_Unsigned_Is_Based_Ghost
+ (Str, Last_Num_Init, Last_Num_Based, Max)
with Ghost;
Based_Val : constant Spec.Uns_Option :=
(if Starts_As_Based and then not Init_Val.Overflow
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
index 117769d20cb..960ad8ec486 100644
--- a/gcc/ada/libgnat/s-vauspe.ads
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -279,24 +279,50 @@ is
Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
-- Normal case: exponentiation without overflows
+ function Raw_Unsigned_Starts_As_Based_Ghost
+ (Str : String;
+ Last_Num_Init, To : Integer)
+ return Boolean
+ is
+ (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')
+ with Ghost,
+ Pre => Last_Num_Init in Str'Range
+ and then To in Str'Range;
+ -- Return True if Str starts as a based number
+
+ function Raw_Unsigned_Is_Based_Ghost
+ (Str : String;
+ Last_Num_Init : Integer;
+ Last_Num_Based : Integer;
+ To : Integer)
+ return Boolean
+ is
+ (Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To)
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1))
+ with Ghost,
+ Pre => Last_Num_Init in Str'Range
+ and then Last_Num_Based in Last_Num_Init .. Str'Last
+ and then To in Str'Range;
+ -- Return True if Str is a based number
+
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';
+ Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Str'Last);
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);
+ Raw_Unsigned_Is_Based_Ghost
+ (Str, Last_Num_Init, Last_Num_Based, Str'Last);
First_Exp : constant Integer :=
(if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
begin
@@ -330,10 +356,7 @@ is
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';
+ Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To);
Last_Num_Based : constant Integer :=
(if Starts_As_Based
then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
@@ -378,18 +401,13 @@ is
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';
+ Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To);
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);
+ Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To);
Based_Val : constant Uns_Option :=
(if Starts_As_Based and then not Init_Val.Overflow
then Scan_Based_Number_Ghost
@@ -468,18 +486,13 @@ is
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';
+ Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To);
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);
+ Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To);
First_Exp : constant Integer :=
(if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
begin
--
2.40.0
