diff options
Diffstat (limited to 'gcc/ada/libgnat/s-valuei.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-valuei.ads | 64 |
1 files changed, 2 insertions, 62 deletions
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index 531eae1..08619c8 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -32,16 +32,6 @@ -- This package contains routines for scanning signed integer values for use -- in Text_IO.Integer_IO, and the Value attribute. -pragma Assertion_Policy (Pre => Ignore, - Post => Ignore, - Contract_Cases => Ignore, - Ghost => Ignore, - Subprogram_Variant => Ignore); - -with System.Val_Spec; use System.Val_Spec; -with System.Value_I_Spec; -with System.Value_U_Spec; - generic type Int is range <>; @@ -54,13 +44,6 @@ generic Max : Integer; Res : out Uns); - -- Additional parameters for ghost subprograms used inside contracts - - with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; - with package Spec is new System.Value_I_Spec - (Int => Int, Uns => Uns, U_Spec => U_Spec) - with Ghost; - package System.Value_I is pragma Preelaborate; @@ -68,43 +51,7 @@ package System.Value_I is (Str : String; Ptr : not null access Integer; Max : Integer; - Res : out Int) - with - 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)) - 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) in '+' | '-' then Non_Blank + 1 - else Non_Blank); - begin - U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max)) - and then U_Spec.Raw_Unsigned_No_Overflow_Ghost - (Str, Fst_Num, Max) - and then Spec.Uns_Is_Valid_Int - (Minus => Str (Non_Blank) = '-', - Uval => U_Spec.Scan_Raw_Unsigned_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) in '+' | '-' then Non_Blank + 1 - else Non_Blank); - Uval : constant Uns := - U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max); - begin - Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', - Uval => Uval, - Val => Res) - and then Ptr.all = U_Spec.Raw_Unsigned_Last_Ghost - (Str, Fst_Num, Max)); + 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 @@ -130,14 +77,7 @@ package System.Value_I is -- special case of an all-blank string, and Ptr is unchanged, and hence -- is greater than Max as required in this case. - 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 Spec.Is_Integer_Ghost (Spec.Slide_If_Necessary (Str)), - Post => Spec.Is_Value_Integer_Ghost - (Spec.Slide_If_Necessary (Str), Value_Integer'Result), - Subprogram_Variant => (Decreases => Str'First); + function Value_Integer (Str : String) return Int; -- 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 -- argument of the attribute. Constraint_Error is raised if the string is |