aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2022-01-25 14:32:38 +0100
committerPierre-Marie de Rodat <derodat@adacore.com>2022-05-10 08:19:24 +0000
commitcfcc53801bd0f95d6f7160a06faa909a360317d6 (patch)
tree4d867a1c0f6af2531cb45d0232cbe893c69c1aea
parentd89d9ecceb541ca824f7fb5f57f747a31c7ce9a5 (diff)
downloadgcc-cfcc53801bd0f95d6f7160a06faa909a360317d6.zip
gcc-cfcc53801bd0f95d6f7160a06faa909a360317d6.tar.gz
gcc-cfcc53801bd0f95d6f7160a06faa909a360317d6.tar.bz2
[Ada] Fix indentation to follow uniform style across runtime units
gcc/ada/ * libgnat/s-valuei.adb: Fix indentation. * libgnat/s-valuei.ads: Same.
-rw-r--r--gcc/ada/libgnat/s-valuei.adb4
-rw-r--r--gcc/ada/libgnat/s-valuei.ads96
2 files changed, 53 insertions, 47 deletions
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index faf5791..68d8984 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -63,6 +63,7 @@ package body System.Value_I is
Non_Blank : constant Positive :=
First_Non_Space_Ghost (Str, Ptr.all, Max)
with Ghost;
+
Fst_Num : constant Positive :=
(if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
else Non_Blank)
@@ -127,10 +128,11 @@ package body System.Value_I is
Non_Blank : constant Positive := First_Non_Space_Ghost
(Str, Str'First, Str'Last)
with Ghost;
+
Fst_Num : constant Positive :=
(if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
else Non_Blank)
- with Ghost;
+ with Ghost;
begin
pragma Assert
(Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index d6a78fd..a7e20ab 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -90,7 +90,8 @@ package System.Value_I is
(if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
elsif Minus then Val = -(Int (Uval))
else Val = Int (Uval))
- with Ghost,
+ with
+ Ghost,
Pre => Uns_Is_Valid_Int (Minus, Uval),
Post => True;
-- Return True if Uval (or -Uval when Minus is True) is equal to Val
@@ -101,8 +102,7 @@ package System.Value_I is
Max : Integer;
Res : out Int)
with
- Pre =>
- Str'Last /= Positive'Last
+ Pre => Str'Last /= Positive'Last
-- Ptr.all .. Max is either an empty range, or a valid range in Str
and then (Ptr.all > Max
or else (Ptr.all >= Str'First and then Max <= Str'Last))
@@ -116,10 +116,10 @@ package System.Value_I is
else Non_Blank);
begin
Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
- and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
- and then Uns_Is_Valid_Int
- (Minus => Str (Non_Blank) = '-',
- Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
+ and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
+ and then Uns_Is_Valid_Int
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
Post =>
(declare
Non_Blank : constant Positive := First_Non_Space_Ghost
@@ -130,10 +130,10 @@ package System.Value_I is
Uval : constant Uns :=
Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
begin
- Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
- Uval => Uval,
- Val => Res)
- and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+ Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Res)
+ and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
-- 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
@@ -160,21 +160,23 @@ package System.Value_I is
-- is greater than Max as required in this case.
function Slide_To_1 (Str : String) return String
- with Ghost,
- Post =>
- Only_Space_Ghost (Str, Str'First, Str'Last) =
+ 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);
+ 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_Integer_Ghost (Str : String) return Boolean is
@@ -185,17 +187,18 @@ package System.Value_I is
(if Str (Non_Blank) in '+' | '-' 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
- Uns_Is_Valid_Int
- (Minus => Str (Non_Blank) = '-',
- Uval => Scan_Raw_Unsigned_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;
+ and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
+ and then
+ Uns_Is_Valid_Int
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Scan_Raw_Unsigned_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 a
-- signed number, consisting in some blank characters, an optional
-- sign, a raw unsigned number which does not overflow and then some
@@ -213,21 +216,22 @@ package System.Value_I is
Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
Uval => Uval,
Val => Val))
- with Ghost,
- Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Last /= Positive'Last
- and then Is_Integer_Ghost (Str),
- Post => True;
+ with
+ Ghost,
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last
+ and then Is_Integer_Ghost (Str),
+ Post => True;
-- Ghost function that returns True if Val is the value corresponding to
-- the signed number represented by Str.
function Value_Integer (Str : String) return Int
- with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Length /= Positive'Last
- and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
- Post =>
- Is_Value_Integer_Ghost
- (Slide_If_Necessary (Str), Value_Integer'Result),
+ with
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Length /= Positive'Last
+ and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
+ Post => Is_Value_Integer_Ghost
+ (Slide_If_Necessary (Str), Value_Integer'Result),
Subprogram_Variant => (Decreases => Str'First);
-- Used in computing X'Value (Str) where X is a signed integer type whose
-- base range does not exceed the base range of Integer. Str is the string
@@ -241,9 +245,9 @@ private
----------------
function Slide_To_1 (Str : String) return String is
- (declare
- Res : constant String (1 .. Str'Length) := Str;
- begin
- Res);
+ (declare
+ Res : constant String (1 .. Str'Length) := Str;
+ begin
+ Res);
end System.Value_I;