gcc/ada/libgnat/i-c.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                         I N T E R F A C E S . C                          --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 -- This specification is derived from the Ada Reference Manual for use with --
  10 -- GNAT.  In accordance with the copyright of that document, you can freely --
  11 -- copy and modify this specification,  provided that if you redistribute a --
  12 -- modified version,  any changes that you have made are clearly indicated. --
  13 --                                                                          --
  14 ------------------------------------------------------------------------------
  15
  16 --  Preconditions in this unit are meant for analysis only, not for run-time
  17 --  checking, so that the expected exceptions are raised. This is enforced by
  18 --  setting the corresponding assertion policy to Ignore. Postconditions and
  19 --  contract cases should not be executed at runtime as well, in order not to
  20 --  slow down the execution of these functions.
  21
  22 pragma Assertion_Policy (Pre            => Ignore,
  23                          Post           => Ignore,
  24                          Contract_Cases => Ignore,
  25                          Ghost          => Ignore);
  26
  27 --  Pre/postconditions use a fully qualified name for the standard "+" operator
  28 --  in order to work around an internal limitation of the compiler.
  29
  30 with System;
  31 with System.Parameters;
  32
  33 package Interfaces.C with
  34   SPARK_Mode,
  35   Pure,
  36   Always_Terminates
  37 is
  38
  39    --  Each of the types declared in Interfaces.C is C-compatible.
  40
  41    --  The types int, short, long, unsigned, ptrdiff_t, size_t, double,
  42    --  char, wchar_t, char16_t, and char32_t correspond respectively to the
  43    --  C types having the same names. The types signed_char, unsigned_short,
  44    --  unsigned_long, unsigned_char, C_bool, C_float, and long_double
  45    --  correspond respectively to the C types signed char, unsigned
  46    --  short, unsigned long, unsigned char, bool, float, and long double.
  47
  48    --  Declaration's based on C's <limits.h>
  49
  50    CHAR_BIT  : constant := 8;
  51    SCHAR_MIN : constant := -128;
  52    SCHAR_MAX : constant := 127;
  53    UCHAR_MAX : constant := 255;
  54
  55    --  Signed and Unsigned Integers. Note that in GNAT, we have ensured that
  56    --  the standard predefined Ada types correspond to the standard C types
  57
  58    --  Note: the Integer qualifications used in the declaration of type long
  59    --  avoid ambiguities when compiling in the presence of s-auxdec.ads and
  60    --  a non-private system.address type.
  61
  62    type int   is new Integer;
  63    type short is new Short_Integer;
  64    type long  is range -(2 ** (System.Parameters.long_bits - Integer'(1)))
  65      .. +(2 ** (System.Parameters.long_bits - Integer'(1))) - 1;
  66    type long_long is new Long_Long_Integer;
  67
  68    type signed_char is range SCHAR_MIN .. SCHAR_MAX;
  69    for signed_char'Size use CHAR_BIT;
  70
  71    type unsigned           is mod 2 ** int'Size;
  72    type unsigned_short     is mod 2 ** short'Size;
  73    type unsigned_long      is mod 2 ** long'Size;
  74    type unsigned_long_long is mod 2 ** long_long'Size;
  75
  76    type unsigned_char is mod (UCHAR_MAX + 1);
  77    for unsigned_char'Size use CHAR_BIT;
  78
  79    --  Note: Ada RM states that the type of the subtype plain_char is either
  80    --  signed_char or unsigned_char, depending on the C implementation. GNAT
  81    --  instead choses unsigned_char always.
  82
  83    subtype plain_char is unsigned_char;
  84
  85    --  Note: the Integer qualifications used in the declaration of ptrdiff_t
  86    --  avoid ambiguities when compiling in the presence of s-auxdec.ads and
  87    --  a non-private system.address type.
  88
  89    type ptrdiff_t is
  90      range -System.Memory_Size / 2 .. System.Memory_Size / 2 - 1;
  91
  92    type size_t is mod System.Memory_Size;
  93
  94    --  Boolean type
  95
  96    type C_bool is new Boolean;
  97    pragma Convention (C, C_bool);
  98
  99    --  Floating-Point
 100
 101    type C_float     is new Float;
 102    type double      is new Standard.Long_Float;
 103    type long_double is new Standard.Long_Long_Float;
 104
 105    ----------------------------
 106    -- Characters and Strings --
 107    ----------------------------
 108
 109    type char is new Character;
 110
 111    nul : constant char := char'First;
 112
 113    --  The functions To_C and To_Ada map between the Ada type Character and the
 114    --  C type char.
 115
 116    function To_C (Item : Character) return char
 117    with
 118      Post => To_C'Result = char'Val (Character'Pos (Item));
 119
 120    function To_Ada (Item : char) return Character
 121    with
 122      Post => To_Ada'Result = Character'Val (char'Pos (Item));
 123
 124    type char_array is array (size_t range <>) of aliased char;
 125    for char_array'Component_Size use CHAR_BIT;
 126
 127    function Is_Nul_Terminated (Item : char_array) return Boolean
 128    with
 129      Post => Is_Nul_Terminated'Result = (for some C of Item => C = nul);
 130    --  The result of Is_Nul_Terminated is True if Item contains nul, and is
 131    --  False otherwise.
 132
 133    function C_Length_Ghost (Item : char_array) return size_t
 134    with
 135      Ghost,
 136      Pre  => Is_Nul_Terminated (Item),
 137      Post => C_Length_Ghost'Result <= Item'Last - Item'First
 138        and then Item (Item'First + C_Length_Ghost'Result) = nul
 139        and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
 140                    when J /= Item'First + C_Length_Ghost'Result =>
 141                      Item (J) /= nul);
 142    --  Ghost function to compute the length of a char_array up to the first nul
 143    --  character.
 144
 145    function To_C
 146      (Item       : String;
 147       Append_Nul : Boolean := True) return char_array
 148    with
 149      Pre  => not (Append_Nul = False and then Item'Length = 0),
 150      Post => To_C'Result'First = 0
 151        and then To_C'Result'Length =
 152          (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length)
 153        and then (for all J in Item'Range =>
 154                    To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
 155        and then (if Append_Nul then To_C'Result (To_C'Result'Last) = nul);
 156    --  The result of To_C is a char_array value of length Item'Length (if
 157    --  Append_Nul is False) or Item'Length+1 (if Append_Nul is True). The lower
 158    --  bound is 0. For each component Item(I), the corresponding component
 159    --  in the result is To_C applied to Item(I). The value nul is appended if
 160    --  Append_Nul is True. If Append_Nul is False and Item'Length is 0, then
 161    --  To_C propagates Constraint_Error.
 162
 163    function To_Ada
 164      (Item     : char_array;
 165       Trim_Nul : Boolean := True) return String
 166    with
 167      Pre  => (if Trim_Nul then
 168                 Is_Nul_Terminated (Item)
 169                   and then C_Length_Ghost (Item) <= size_t (Natural'Last)
 170               else
 171                 Item'Last - Item'First < size_t (Natural'Last)),
 172      Post => To_Ada'Result'First = 1
 173        and then To_Ada'Result'Length =
 174          (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
 175        and then (for all J in To_Ada'Result'Range =>
 176                    To_Ada'Result (J) =
 177                      To_Ada (Item (size_t (J) - 1 + Item'First)));
 178    --  The result of To_Ada is a String whose length is Item'Length (if
 179    --  Trim_Nul is False) or the length of the slice of Item preceding the
 180    --  first nul (if Trim_Nul is True). The lower bound of the result is 1.
 181    --  If Trim_Nul is False, then for each component Item(I) the corresponding
 182    --  component in the result is To_Ada applied to Item(I). If Trim_Nul
 183    --  is True, then for each component Item(I) before the first nul the
 184    --  corresponding component in the result is To_Ada applied to Item(I). The
 185    --  function propagates Terminator_Error if Trim_Nul is True and Item does
 186    --  not contain nul.
 187
 188    procedure To_C
 189      (Item       : String;
 190       Target     : out char_array;
 191       Count      : out size_t;
 192       Append_Nul : Boolean := True)
 193    with
 194      Relaxed_Initialization => Target,
 195      Pre  => Target'Length >=
 196        (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length),
 197      Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
 198        and then
 199          (if Count /= 0 then
 200            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 201        and then
 202          (for all J in Item'Range =>
 203            Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
 204        and then
 205          (if Append_Nul then Target (Target'First + (Count - 1)) = nul);
 206    --  For procedure To_C, each element of Item is converted (via the To_C
 207    --  function) to a char, which is assigned to the corresponding element of
 208    --  Target. If Append_Nul is True, nul is then assigned to the next element
 209    --  of Target. In either case, Count is set to the number of Target elements
 210    --  assigned. If Target is not long enough, Constraint_Error is propagated.
 211
 212    procedure To_Ada
 213      (Item     : char_array;
 214       Target   : out String;
 215       Count    : out Natural;
 216       Trim_Nul : Boolean := True)
 217    with
 218      Relaxed_Initialization => Target,
 219      Pre  => (if Trim_Nul then
 220                 Is_Nul_Terminated (Item)
 221                   and then C_Length_Ghost (Item) <= size_t (Target'Length)
 222               else
 223                 Item'Last - Item'First < size_t (Target'Length)),
 224      Post => Count =
 225          (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
 226        and then
 227          (if Count /= 0 then
 228            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 229        and then
 230          (for all J in Target'First .. Target'First + (Count - 1) =>
 231            Target (J) =
 232              To_Ada (Item (size_t (J - Target'First) + Item'First)));
 233    --  For procedure To_Ada, each element of Item (if Trim_Nul is False) or
 234    --  each element of Item preceding the first nul (if Trim_Nul is True) is
 235    --  converted (via the To_Ada function) to a Character, which is assigned
 236    --  to the corresponding element of Target. Count is set to the number of
 237    --  Target elements assigned. If Target is not long enough, Constraint_Error
 238    --  is propagated. If Trim_Nul is True and Item does not contain nul, then
 239    --  Terminator_Error is propagated.
 240
 241    ------------------------------------
 242    -- Wide Character and Wide String --
 243    ------------------------------------
 244
 245    type wchar_t is new Wide_Character;
 246    for wchar_t'Size use Standard'Wchar_T_Size;
 247
 248    wide_nul : constant wchar_t := wchar_t'First;
 249
 250    --  To_C and To_Ada provide the mappings between the Ada and C wide
 251    --  character types.
 252
 253    function To_C (Item : Wide_Character) return wchar_t
 254    with
 255      Post => To_C'Result = wchar_t (Item);
 256
 257    function To_Ada (Item : wchar_t) return Wide_Character
 258    with
 259      Post => To_Ada'Result = Wide_Character (Item);
 260
 261    type wchar_array is array (size_t range <>) of aliased wchar_t;
 262
 263    function Is_Nul_Terminated (Item : wchar_array) return Boolean
 264    with
 265      Post => Is_Nul_Terminated'Result = (for some C of Item => C = wide_nul);
 266    --  The result of Is_Nul_Terminated is True if Item contains wide_nul, and
 267    --  is False otherwise.
 268
 269    --  The To_C and To_Ada subprograms that convert between Wide_String and
 270    --  wchar_array have analogous effects to the To_C and To_Ada subprograms
 271    --  that convert between String and char_array, except that wide_nul is
 272    --  used instead of nul.
 273
 274    function C_Length_Ghost (Item : wchar_array) return size_t
 275    with
 276      Ghost,
 277      Pre  => Is_Nul_Terminated (Item),
 278      Post => C_Length_Ghost'Result <= Item'Last - Item'First
 279        and then Item (Item'First + C_Length_Ghost'Result) = wide_nul
 280        and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
 281                    when J /= Item'First + C_Length_Ghost'Result =>
 282                      Item (J) /= wide_nul);
 283    --  Ghost function to compute the length of a wchar_array up to the first
 284    --  wide_nul character.
 285
 286    function To_C
 287      (Item       : Wide_String;
 288       Append_Nul : Boolean := True) return wchar_array
 289    with
 290      Pre  => not (Append_Nul = False and then Item'Length = 0),
 291      Post => To_C'Result'First = 0
 292        and then To_C'Result'Length =
 293          (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length)
 294        and then (for all J in Item'Range =>
 295                    To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
 296        and then (if Append_Nul then To_C'Result (To_C'Result'Last) = wide_nul);
 297
 298    function To_Ada
 299      (Item     : wchar_array;
 300       Trim_Nul : Boolean := True) return Wide_String
 301    with
 302      Pre  => (if Trim_Nul then
 303                 Is_Nul_Terminated (Item)
 304                   and then C_Length_Ghost (Item) <= size_t (Natural'Last)
 305               else
 306                 Item'Last - Item'First < size_t (Natural'Last)),
 307      Post => To_Ada'Result'First = 1
 308        and then To_Ada'Result'Length =
 309          (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
 310        and then (for all J in To_Ada'Result'Range =>
 311                    To_Ada'Result (J) =
 312                      To_Ada (Item (size_t (J) - 1 + Item'First)));
 313
 314    procedure To_C
 315      (Item       : Wide_String;
 316       Target     : out wchar_array;
 317       Count      : out size_t;
 318       Append_Nul : Boolean := True)
 319    with
 320      Relaxed_Initialization => Target,
 321      Pre  => Target'Length >=
 322        (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length),
 323      Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
 324        and then
 325          (if Count /= 0 then
 326            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 327        and then
 328          (for all J in Item'Range =>
 329            Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
 330        and then
 331          (if Append_Nul then Target (Target'First + (Count - 1)) = wide_nul);
 332
 333    procedure To_Ada
 334      (Item     : wchar_array;
 335       Target   : out Wide_String;
 336       Count    : out Natural;
 337       Trim_Nul : Boolean := True)
 338    with
 339      Relaxed_Initialization => Target,
 340      Pre  => (if Trim_Nul then
 341                 Is_Nul_Terminated (Item)
 342                   and then C_Length_Ghost (Item) <= size_t (Target'Length)
 343               else
 344                 Item'Last - Item'First < size_t (Target'Length)),
 345      Post => Count =
 346          (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
 347        and then
 348          (if Count /= 0 then
 349            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 350        and then
 351          (for all J in Target'First .. Target'First + (Count - 1) =>
 352            Target (J) =
 353              To_Ada (Item (size_t (J - Target'First) + Item'First)));
 354
 355    Terminator_Error : exception;
 356
 357    --  The remaining declarations are for Ada 2005 (AI-285)
 358
 359    --  ISO/IEC 10646:2003 compatible types defined by SC22/WG14 document N1010
 360
 361    type char16_t is new Wide_Character;
 362    pragma Ada_05 (char16_t);
 363
 364    char16_nul : constant char16_t := char16_t'Val (0);
 365    pragma Ada_05 (char16_nul);
 366
 367    --  To_C and To_Ada provide mappings between the Ada and C 16-bit character
 368    --  types.
 369
 370    function To_C (Item : Wide_Character) return char16_t
 371    with
 372      Post => To_C'Result = char16_t (Item);
 373    pragma Ada_05 (To_C);
 374
 375    function To_Ada (Item : char16_t) return Wide_Character
 376    with
 377      Post => To_Ada'Result = Wide_Character (Item);
 378    pragma Ada_05 (To_Ada);
 379
 380    type char16_array is array (size_t range <>) of aliased char16_t;
 381    pragma Ada_05 (char16_array);
 382
 383    function Is_Nul_Terminated (Item : char16_array) return Boolean
 384    with
 385      Post => Is_Nul_Terminated'Result = (for some C of Item => C = char16_nul);
 386    pragma Ada_05 (Is_Nul_Terminated);
 387    --  The result of Is_Nul_Terminated is True if Item contains char16_nul, and
 388    --  is False otherwise.
 389
 390    --  The To_C and To_Ada subprograms that convert between Wide_String and
 391    --  char16_array have analogous effects to the To_C and To_Ada subprograms
 392    --  that convert between String and char_array, except that char16_nul is
 393    --  used instead of nul.
 394
 395    function C_Length_Ghost (Item : char16_array) return size_t
 396    with
 397      Ghost,
 398      Pre  => Is_Nul_Terminated (Item),
 399      Post => C_Length_Ghost'Result <= Item'Last - Item'First
 400        and then Item (Item'First + C_Length_Ghost'Result) = char16_nul
 401        and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
 402                    when J /= Item'First + C_Length_Ghost'Result =>
 403                      Item (J) /= char16_nul);
 404    --  Ghost function to compute the length of a char16_array up to the first
 405    --  char16_nul character.
 406
 407    function To_C
 408      (Item       : Wide_String;
 409       Append_Nul : Boolean := True) return char16_array
 410    with
 411      Pre  => not (Append_Nul = False and then Item'Length = 0),
 412      Post => To_C'Result'First = 0
 413        and then To_C'Result'Length =
 414          (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length)
 415        and then (for all J in Item'Range =>
 416                    To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
 417        and then
 418          (if Append_Nul then To_C'Result (To_C'Result'Last) = char16_nul);
 419    pragma Ada_05 (To_C);
 420
 421    function To_Ada
 422      (Item     : char16_array;
 423       Trim_Nul : Boolean := True) return Wide_String
 424    with
 425      Pre  => (if Trim_Nul then
 426                 Is_Nul_Terminated (Item)
 427                   and then C_Length_Ghost (Item) <= size_t (Natural'Last)
 428               else
 429                 Item'Last - Item'First < size_t (Natural'Last)),
 430      Post => To_Ada'Result'First = 1
 431        and then To_Ada'Result'Length =
 432          (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
 433        and then (for all J in To_Ada'Result'Range =>
 434                    To_Ada'Result (J) =
 435                      To_Ada (Item (size_t (J) - 1 + Item'First)));
 436    pragma Ada_05 (To_Ada);
 437
 438    procedure To_C
 439      (Item       : Wide_String;
 440       Target     : out char16_array;
 441       Count      : out size_t;
 442       Append_Nul : Boolean := True)
 443    with
 444      Relaxed_Initialization => Target,
 445      Pre  => Target'Length >=
 446        (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length),
 447      Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
 448        and then
 449          (if Count /= 0 then
 450            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 451        and then
 452          (for all J in Item'Range =>
 453            Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
 454        and then
 455          (if Append_Nul then Target (Target'First + (Count - 1)) = char16_nul);
 456    pragma Ada_05 (To_C);
 457
 458    procedure To_Ada
 459      (Item     : char16_array;
 460       Target   : out Wide_String;
 461       Count    : out Natural;
 462       Trim_Nul : Boolean := True)
 463    with
 464      Relaxed_Initialization => Target,
 465      Pre  => (if Trim_Nul then
 466                 Is_Nul_Terminated (Item)
 467                   and then C_Length_Ghost (Item) <= size_t (Target'Length)
 468               else
 469                 Item'Last - Item'First < size_t (Target'Length)),
 470      Post => Count =
 471          (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
 472        and then
 473          (if Count /= 0 then
 474            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 475        and then
 476          (for all J in Target'First .. Target'First + (Count - 1) =>
 477            Target (J) =
 478              To_Ada (Item (size_t (J - Target'First) + Item'First)));
 479    pragma Ada_05 (To_Ada);
 480
 481    type char32_t is new Wide_Wide_Character;
 482    pragma Ada_05 (char32_t);
 483
 484    char32_nul : constant char32_t := char32_t'Val (0);
 485    pragma Ada_05 (char32_nul);
 486
 487    --  To_C and To_Ada provide mappings between the Ada and C 32-bit character
 488    --  types.
 489
 490    function To_C (Item : Wide_Wide_Character) return char32_t
 491    with
 492      Post => To_C'Result = char32_t (Item);
 493    pragma Ada_05 (To_C);
 494
 495    function To_Ada (Item : char32_t) return Wide_Wide_Character
 496    with
 497      Post => To_Ada'Result = Wide_Wide_Character (Item);
 498    pragma Ada_05 (To_Ada);
 499
 500    type char32_array is array (size_t range <>) of aliased char32_t;
 501    pragma Ada_05 (char32_array);
 502
 503    function Is_Nul_Terminated (Item : char32_array) return Boolean
 504    with
 505      Post => Is_Nul_Terminated'Result = (for some C of Item => C = char32_nul);
 506    pragma Ada_05 (Is_Nul_Terminated);
 507    --  The result of Is_Nul_Terminated is True if Item contains char32_nul, and
 508    --  is False otherwise.
 509
 510    function C_Length_Ghost (Item : char32_array) return size_t
 511    with
 512      Ghost,
 513      Pre  => Is_Nul_Terminated (Item),
 514      Post => C_Length_Ghost'Result <= Item'Last - Item'First
 515        and then Item (Item'First + C_Length_Ghost'Result) = char32_nul
 516        and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
 517                    when J /= Item'First + C_Length_Ghost'Result =>
 518                      Item (J) /= char32_nul);
 519    --  Ghost function to compute the length of a char32_array up to the first
 520    --  char32_nul character.
 521
 522    --  The To_C and To_Ada subprograms that convert between Wide_Wide_String
 523    --  and char32_array have analogous effects to the To_C and To_Ada
 524    --  subprograms that convert between String and char_array, except
 525    --  that char32_nul is used instead of nul.
 526
 527    function To_C
 528      (Item       : Wide_Wide_String;
 529       Append_Nul : Boolean := True) return char32_array
 530    with
 531      Pre  => not (Append_Nul = False and then Item'Length = 0),
 532      Post => To_C'Result'First = 0
 533        and then To_C'Result'Length =
 534          (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length)
 535        and then (for all J in Item'Range =>
 536                    To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
 537        and then
 538          (if Append_Nul then To_C'Result (To_C'Result'Last) = char32_nul);
 539    pragma Ada_05 (To_C);
 540
 541    function To_Ada
 542      (Item     : char32_array;
 543       Trim_Nul : Boolean := True) return Wide_Wide_String
 544    with
 545      Pre  => (if Trim_Nul then
 546                 Is_Nul_Terminated (Item)
 547                   and then C_Length_Ghost (Item) <= size_t (Natural'Last)
 548               else
 549                 Item'Last - Item'First < size_t (Natural'Last)),
 550      Post => To_Ada'Result'First = 1
 551        and then To_Ada'Result'Length =
 552          (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
 553        and then (for all J in To_Ada'Result'Range =>
 554                    To_Ada'Result (J) =
 555                      To_Ada (Item (size_t (J) - 1 + Item'First)));
 556    pragma Ada_05 (To_Ada);
 557
 558    procedure To_C
 559      (Item       : Wide_Wide_String;
 560       Target     : out char32_array;
 561       Count      : out size_t;
 562       Append_Nul : Boolean := True)
 563    with
 564      Relaxed_Initialization => Target,
 565      Pre  => Target'Length >=
 566        (if Append_Nul then Standard."+" (Item'Length, 1) else Item'Length),
 567      Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
 568        and then
 569          (if Count /= 0 then
 570            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 571        and then
 572          (for all J in Item'Range =>
 573            Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
 574        and then
 575          (if Append_Nul then Target (Target'First + (Count - 1)) = char32_nul);
 576    pragma Ada_05 (To_C);
 577
 578    procedure To_Ada
 579      (Item     : char32_array;
 580       Target   : out Wide_Wide_String;
 581       Count    : out Natural;
 582       Trim_Nul : Boolean := True)
 583    with
 584      Relaxed_Initialization => Target,
 585      Pre  => (if Trim_Nul then
 586                 Is_Nul_Terminated (Item)
 587                   and then C_Length_Ghost (Item) <= size_t (Target'Length)
 588               else
 589                 Item'Last - Item'First < size_t (Target'Length)),
 590      Post => Count =
 591          (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
 592        and then
 593          (if Count /= 0 then
 594            Target (Target'First .. Target'First + (Count - 1))'Initialized)
 595        and then
 596          (for all J in Target'First .. Target'First + (Count - 1) =>
 597            Target (J) =
 598              To_Ada (Item (size_t (J - Target'First) + Item'First)));
 599    pragma Ada_05 (To_Ada);
 600
 601 end Interfaces.C;