gcc/ada/libgnat/s-imageu.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                       S Y S T E M . I M A G E _ U                        --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2024, 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 routines for supporting the Image attribute for
  33 --  modular integer types, and also for conversion operations required in
  34 --  Text_IO.Modular_IO for such types.
  35
  36 --  Preconditions in this unit are meant for analysis only, not for run-time
  37 --  checking, so that the expected exceptions are raised. This is enforced by
  38 --  setting the corresponding assertion policy to Ignore. Postconditions and
  39 --  contract cases should not be executed at runtime as well, in order not to
  40 --  slow down the execution of these functions.
  41
  42 pragma Assertion_Policy (Pre                => Ignore,
  43                          Post               => Ignore,
  44                          Contract_Cases     => Ignore,
  45                          Ghost              => Ignore,
  46                          Subprogram_Variant => Ignore);
  47
  48 with System.Value_U_Spec;
  49
  50 generic
  51
  52    type Uns is mod <>;
  53
  54    --  Additional parameters for ghost subprograms used inside contracts
  55
  56    with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
  57
  58 package System.Image_U is
  59    use all type U_Spec.Uns_Option;
  60
  61    Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost;
  62
  63    procedure Image_Unsigned
  64      (V : Uns;
  65       S : in out String;
  66       P : out Natural)
  67    with
  68      Pre  => S'First = 1
  69        and then S'Last < Integer'Last
  70        and then S'Last >= Unsigned_Width_Ghost,
  71      Post => P in S'Range
  72        and then U_Spec.Is_Value_Unsigned_Ghost (S (1 .. P), V);
  73    pragma Inline (Image_Unsigned);
  74    --  Computes Uns'Image (V) and stores the result in S (1 .. P) setting
  75    --  the resulting value of P. The caller guarantees that S is long enough to
  76    --  hold the result, and that S'First is 1.
  77
  78    procedure Set_Image_Unsigned
  79      (V : Uns;
  80       S : in out String;
  81       P : in out Natural)
  82    with
  83      Pre  => P < Integer'Last
  84        and then S'Last < Integer'Last
  85        and then S'First <= P + 1
  86        and then S'First <= S'Last
  87        and then P <= S'Last - Unsigned_Width_Ghost + 1,
  88      Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
  89        and then P in P'Old + 1 .. S'Last
  90        and then U_Spec.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
  91        and then U_Spec.Scan_Based_Number_Ghost
  92          (S, From => P'Old + 1, To => P)
  93          = U_Spec.Wrap_Option (V);
  94    --  Stores the image of V in S starting at S (P + 1), P is updated to point
  95    --  to the last character stored. The value stored is identical to the value
  96    --  of Uns'Image (V) except that no leading space is stored. The caller
  97    --  guarantees that S is long enough to hold the result. S need not have a
  98    --  lower bound of 1.
  99
 100 end System.Image_U;