gcc/ada/libgnat/s-vaispe.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                   S Y S T E M . V A L U E _ I _ S P E C                  --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2022-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  This package contains the specification entities using for the formal
  33 --  verification of the routines for scanning signed integer values.
  34
  35 --  Preconditions in this unit are meant for analysis only, not for run-time
  36 --  checking, so that the expected exceptions are raised. This is enforced by
  37 --  setting the corresponding assertion policy to Ignore. Postconditions and
  38 --  contract cases should not be executed at runtime as well, in order not to
  39 --  slow down the execution of these functions.
  40
  41 pragma Assertion_Policy (Pre                => Ignore,
  42                          Post               => Ignore,
  43                          Contract_Cases     => Ignore,
  44                          Ghost              => Ignore,
  45                          Subprogram_Variant => Ignore);
  46
  47 with System.Value_U_Spec;
  48 with System.Val_Spec; use System.Val_Spec;
  49
  50 generic
  51
  52    type Int is range <>;
  53
  54    type Uns is mod <>;
  55
  56    --  Additional parameters for ghost subprograms used inside contracts
  57
  58    with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
  59
  60 package System.Value_I_Spec with
  61    Ghost,
  62    SPARK_Mode,
  63    Always_Terminates
  64 is
  65    pragma Preelaborate;
  66    use all type U_Spec.Uns_Option;
  67
  68    function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
  69      (if Minus then Uval <= Uns (Int'Last) + 1
  70       else Uval <= Uns (Int'Last))
  71    with Post => True;
  72    --  Return True if Uval (or -Uval when Minus is True) is a valid number of
  73    --  type Int.
  74
  75    function Is_Int_Of_Uns
  76      (Minus : Boolean;
  77       Uval  : Uns;
  78       Val   : Int)
  79       return Boolean
  80    is
  81      (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
  82       elsif Minus then Val = -(Int (Uval))
  83       else Val = Int (Uval))
  84    with
  85      Pre  => Uns_Is_Valid_Int (Minus, Uval),
  86      Post => True;
  87    --  Return True if Uval (or -Uval when Minus is True) is equal to Val
  88
  89    function Abs_Uns_Of_Int (Val : Int) return Uns is
  90      (if Val = Int'First then Uns (Int'Last) + 1
  91       elsif Val < 0 then Uns (-Val)
  92       else Uns (Val));
  93    --  Return the unsigned absolute value of Val
  94
  95    function Slide_To_1 (Str : String) return String
  96    with
  97      Post =>
  98        Only_Space_Ghost (Str, Str'First, Str'Last) =
  99          (for all J in Str'First .. Str'Last =>
 100             Slide_To_1'Result (J - Str'First + 1) = ' ');
 101    --  Slides Str so that it starts at 1
 102
 103    function Slide_If_Necessary (Str : String) return String is
 104      (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
 105    --  If Str'Last = Positive'Last then slides Str so that it starts at 1
 106
 107    function Is_Integer_Ghost (Str : String) return Boolean is
 108      (declare
 109         Non_Blank : constant Positive := First_Non_Space_Ghost
 110           (Str, Str'First, Str'Last);
 111         Fst_Num   : constant Positive :=
 112           (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
 113       begin
 114         U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
 115           and then U_Spec.Raw_Unsigned_No_Overflow_Ghost
 116              (Str, Fst_Num, Str'Last)
 117           and then
 118             Uns_Is_Valid_Int
 119               (Minus => Str (Non_Blank) = '-',
 120                Uval  => U_Spec.Scan_Raw_Unsigned_Ghost
 121                  (Str, Fst_Num, Str'Last))
 122           and then Only_Space_Ghost
 123             (Str, U_Spec.Raw_Unsigned_Last_Ghost
 124              (Str, Fst_Num, Str'Last), Str'Last))
 125    with
 126      Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
 127        and then Str'Last /= Positive'Last,
 128      Post => True;
 129    --  Ghost function that determines if Str has the correct format for a
 130    --  signed number, consisting in some blank characters, an optional
 131    --  sign, a raw unsigned number which does not overflow and then some
 132    --  more blank characters.
 133
 134    function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
 135      (declare
 136         Non_Blank : constant Positive := First_Non_Space_Ghost
 137           (Str, Str'First, Str'Last);
 138         Fst_Num   : constant Positive :=
 139           (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
 140         Uval      : constant Uns :=
 141           U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
 142       begin
 143         Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
 144                        Uval  => Uval,
 145                        Val   => Val))
 146    with
 147      Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
 148        and then Str'Last /= Positive'Last
 149        and then Is_Integer_Ghost (Str),
 150      Post => True;
 151    --  Ghost function that returns True if Val is the value corresponding to
 152    --  the signed number represented by Str.
 153
 154    procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
 155    with
 156      Ghost,
 157      Pre  => Str'Last /= Positive'Last
 158        and then Str'Length >= 2
 159        and then Str (Str'First) in ' ' | '-'
 160        and then (Str (Str'First) = '-') = (Val < 0)
 161        and then U_Spec.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
 162        and then U_Spec.Scan_Based_Number_Ghost
 163          (Str, Str'First + 1, Str'Last)
 164          = U_Spec.Wrap_Option (Abs_Uns_Of_Int (Val)),
 165      Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
 166        and then Is_Value_Integer_Ghost (Str, Val);
 167    --  Ghost lemma used in the proof of 'Image implementation, to prove that
 168    --  the result of Value_Integer on a decimal string is the same as the
 169    --  signing the result of Scan_Based_Number_Ghost.
 170
 171 private
 172
 173    ----------------
 174    -- Slide_To_1 --
 175    ----------------
 176
 177    function Slide_To_1 (Str : String) return String is
 178      (declare
 179         Res : constant String (1 .. Str'Length) := Str;
 180       begin
 181         Res);
 182
 183 end System.Value_I_Spec;