gcc/ada/libgnat/i-c.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                         I N T E R F A C E S . C                          --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   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 --  Ghost code, loop invariants and assertions in this unit are meant for
  33 --  analysis only, not for run-time checking, as it would be too costly
  34 --  otherwise. This is enforced by setting the assertion policy to Ignore.
  35
  36 pragma Assertion_Policy (Ghost          => Ignore,
  37                          Loop_Invariant => Ignore,
  38                          Assert         => Ignore);
  39
  40 package body Interfaces.C
  41   with SPARK_Mode
  42 is
  43
  44    --------------------
  45    -- C_Length_Ghost --
  46    --------------------
  47
  48    function C_Length_Ghost (Item : char_array) return size_t is
  49    begin
  50       for J in Item'Range loop
  51          if Item (J) = nul then
  52             return J - Item'First;
  53          end if;
  54
  55          pragma Loop_Invariant
  56            (for all K in Item'First .. J => Item (K) /= nul);
  57       end loop;
  58
  59       raise Program_Error;
  60    end C_Length_Ghost;
  61
  62    function C_Length_Ghost (Item : wchar_array) return size_t is
  63    begin
  64       for J in Item'Range loop
  65          if Item (J) = wide_nul then
  66             return J - Item'First;
  67          end if;
  68
  69          pragma Loop_Invariant
  70            (for all K in Item'First .. J => Item (K) /= wide_nul);
  71       end loop;
  72
  73       raise Program_Error;
  74    end C_Length_Ghost;
  75
  76    function C_Length_Ghost (Item : char16_array) return size_t is
  77    begin
  78       for J in Item'Range loop
  79          if Item (J) = char16_nul then
  80             return J - Item'First;
  81          end if;
  82
  83          pragma Loop_Invariant
  84            (for all K in Item'First .. J => Item (K) /= char16_nul);
  85       end loop;
  86
  87       raise Program_Error;
  88    end C_Length_Ghost;
  89
  90    function C_Length_Ghost (Item : char32_array) return size_t is
  91    begin
  92       for J in Item'Range loop
  93          if Item (J) = char32_nul then
  94             return J - Item'First;
  95          end if;
  96
  97          pragma Loop_Invariant
  98            (for all K in Item'First .. J => Item (K) /= char32_nul);
  99       end loop;
 100
 101       raise Program_Error;
 102    end C_Length_Ghost;
 103
 104    -----------------------
 105    -- Is_Nul_Terminated --
 106    -----------------------
 107
 108    --  Case of char_array
 109
 110    function Is_Nul_Terminated (Item : char_array) return Boolean is
 111    begin
 112       for J in Item'Range loop
 113          if Item (J) = nul then
 114             return True;
 115          end if;
 116
 117          pragma Loop_Invariant
 118            (for all K in Item'First .. J => Item (K) /= nul);
 119       end loop;
 120
 121       return False;
 122    end Is_Nul_Terminated;
 123
 124    --  Case of wchar_array
 125
 126    function Is_Nul_Terminated (Item : wchar_array) return Boolean is
 127    begin
 128       for J in Item'Range loop
 129          if Item (J) = wide_nul then
 130             return True;
 131          end if;
 132
 133          pragma Loop_Invariant
 134            (for all K in Item'First .. J => Item (K) /= wide_nul);
 135       end loop;
 136
 137       return False;
 138    end Is_Nul_Terminated;
 139
 140    --  Case of char16_array
 141
 142    function Is_Nul_Terminated (Item : char16_array) return Boolean is
 143    begin
 144       for J in Item'Range loop
 145          if Item (J) = char16_nul then
 146             return True;
 147          end if;
 148
 149          pragma Loop_Invariant
 150            (for all K in Item'First .. J => Item (K) /= char16_nul);
 151       end loop;
 152
 153       return False;
 154    end Is_Nul_Terminated;
 155
 156    --  Case of char32_array
 157
 158    function Is_Nul_Terminated (Item : char32_array) return Boolean is
 159    begin
 160       for J in Item'Range loop
 161          if Item (J) = char32_nul then
 162             return True;
 163          end if;
 164
 165          pragma Loop_Invariant
 166            (for all K in Item'First .. J => Item (K) /= char32_nul);
 167       end loop;
 168
 169       return False;
 170    end Is_Nul_Terminated;
 171
 172    ------------
 173    -- To_Ada --
 174    ------------
 175
 176    --  Convert char to Character
 177
 178    function To_Ada (Item : char) return Character is
 179    begin
 180       return Character'Val (char'Pos (Item));
 181    end To_Ada;
 182
 183    --  Convert char_array to String (function form)
 184
 185    function To_Ada
 186      (Item     : char_array;
 187       Trim_Nul : Boolean := True) return String
 188    is
 189       Count : Natural;
 190       From  : size_t;
 191
 192    begin
 193       if Trim_Nul then
 194          From := Item'First;
 195
 196          loop
 197             pragma Loop_Invariant (From in Item'Range);
 198             pragma Loop_Invariant
 199               (for some J in From .. Item'Last => Item (J) = nul);
 200             pragma Loop_Invariant
 201               (for all J in Item'First .. From when J /= From =>
 202                  Item (J) /= nul);
 203             pragma Loop_Variant (Increases => From);
 204
 205             if From > Item'Last then
 206                raise Terminator_Error;
 207             elsif Item (From) = nul then
 208                exit;
 209             else
 210                From := From + 1;
 211             end if;
 212          end loop;
 213
 214          pragma Assert (From = Item'First + C_Length_Ghost (Item));
 215
 216          Count := Natural (From - Item'First);
 217
 218       else
 219          Count := Item'Length;
 220       end if;
 221
 222       declare
 223          Count_Cst : constant Natural := Count;
 224          R : String (1 .. Count_Cst) with Relaxed_Initialization;
 225
 226       begin
 227          for J in R'Range loop
 228             R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
 229
 230             pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
 231             pragma Loop_Invariant
 232               (for all K in 1 .. J =>
 233                 R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
 234          end loop;
 235
 236          return R;
 237       end;
 238    end To_Ada;
 239
 240    --  Convert char_array to String (procedure form)
 241
 242    procedure To_Ada
 243      (Item     : char_array;
 244       Target   : out String;
 245       Count    : out Natural;
 246       Trim_Nul : Boolean := True)
 247    is
 248       From : size_t;
 249       To   : Integer;
 250
 251    begin
 252       if Trim_Nul then
 253          From := Item'First;
 254          loop
 255             pragma Loop_Invariant (From in Item'Range);
 256             pragma Loop_Invariant
 257               (for some J in From .. Item'Last => Item (J) = nul);
 258             pragma Loop_Invariant
 259               (for all J in Item'First .. From when J /= From =>
 260                 Item (J) /= nul);
 261             pragma Loop_Variant (Increases => From);
 262
 263             if From > Item'Last then
 264                raise Terminator_Error;
 265             elsif Item (From) = nul then
 266                exit;
 267             else
 268                From := From + 1;
 269             end if;
 270          end loop;
 271
 272          Count := Natural (From - Item'First);
 273
 274       else
 275          Count := Item'Length;
 276       end if;
 277
 278       if Count > Target'Length then
 279          raise Constraint_Error;
 280
 281       else
 282          From := Item'First;
 283          To   := Target'First;
 284
 285          for J in 1 .. Count loop
 286             Target (To) := Character (Item (From));
 287
 288             pragma Loop_Invariant (From in Item'Range);
 289             pragma Loop_Invariant (To in Target'Range);
 290             pragma Loop_Invariant (To = Target'First + (J - 1));
 291             pragma Loop_Invariant (From = Item'First + size_t (J - 1));
 292             pragma Loop_Invariant
 293               (for all J in Target'First .. To => Target (J)'Initialized);
 294             pragma Loop_Invariant
 295               (Target (Target'First .. To)'Initialized);
 296             pragma Loop_Invariant
 297               (for all K in Target'First .. To =>
 298                 Target (K) =
 299                   To_Ada (Item (size_t (K - Target'First) + Item'First)));
 300
 301             --  Avoid possible overflow when incrementing To in the last
 302             --  iteration of the loop.
 303             exit when J = Count;
 304
 305             From := From + 1;
 306             To   := To + 1;
 307          end loop;
 308       end if;
 309    end To_Ada;
 310
 311    --  Convert wchar_t to Wide_Character
 312
 313    function To_Ada (Item : wchar_t) return Wide_Character is
 314    begin
 315       return Wide_Character (Item);
 316    end To_Ada;
 317
 318    --  Convert wchar_array to Wide_String (function form)
 319
 320    function To_Ada
 321      (Item     : wchar_array;
 322       Trim_Nul : Boolean := True) return Wide_String
 323    is
 324       Count : Natural;
 325       From  : size_t;
 326
 327    begin
 328       if Trim_Nul then
 329          From := Item'First;
 330
 331          loop
 332             pragma Loop_Invariant (From in Item'Range);
 333             pragma Loop_Invariant
 334               (for some J in From .. Item'Last => Item (J) = wide_nul);
 335             pragma Loop_Invariant
 336               (for all J in Item'First .. From when J /= From =>
 337                  Item (J) /= wide_nul);
 338             pragma Loop_Variant (Increases => From);
 339
 340             if From > Item'Last then
 341                raise Terminator_Error;
 342             elsif Item (From) = wide_nul then
 343                exit;
 344             else
 345                From := From + 1;
 346             end if;
 347          end loop;
 348
 349          pragma Assert (From = Item'First + C_Length_Ghost (Item));
 350
 351          Count := Natural (From - Item'First);
 352
 353       else
 354          Count := Item'Length;
 355       end if;
 356
 357       declare
 358          Count_Cst : constant Natural := Count;
 359          R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 360
 361       begin
 362          for J in R'Range loop
 363             R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
 364
 365             pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
 366             pragma Loop_Invariant
 367               (for all K in 1 .. J =>
 368                 R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
 369          end loop;
 370
 371          return R;
 372       end;
 373    end To_Ada;
 374
 375    --  Convert wchar_array to Wide_String (procedure form)
 376
 377    procedure To_Ada
 378      (Item     : wchar_array;
 379       Target   : out Wide_String;
 380       Count    : out Natural;
 381       Trim_Nul : Boolean := True)
 382    is
 383       From : size_t;
 384       To   : Integer;
 385
 386    begin
 387       if Trim_Nul then
 388          From := Item'First;
 389          loop
 390             pragma Loop_Invariant (From in Item'Range);
 391             pragma Loop_Invariant
 392               (for some J in From .. Item'Last => Item (J) = wide_nul);
 393             pragma Loop_Invariant
 394               (for all J in Item'First .. From when J /= From =>
 395                 Item (J) /= wide_nul);
 396             pragma Loop_Variant (Increases => From);
 397
 398             if From > Item'Last then
 399                raise Terminator_Error;
 400             elsif Item (From) = wide_nul then
 401                exit;
 402             else
 403                From := From + 1;
 404             end if;
 405          end loop;
 406
 407          Count := Natural (From - Item'First);
 408
 409       else
 410          Count := Item'Length;
 411       end if;
 412
 413       if Count > Target'Length then
 414          raise Constraint_Error;
 415
 416       else
 417          From := Item'First;
 418          To   := Target'First;
 419
 420          for J in 1 .. Count loop
 421             Target (To) := To_Ada (Item (From));
 422
 423             pragma Loop_Invariant (From in Item'Range);
 424             pragma Loop_Invariant (To in Target'Range);
 425             pragma Loop_Invariant (To = Target'First + (J - 1));
 426             pragma Loop_Invariant (From = Item'First + size_t (J - 1));
 427             pragma Loop_Invariant
 428               (for all J in Target'First .. To => Target (J)'Initialized);
 429             pragma Loop_Invariant
 430               (Target (Target'First .. To)'Initialized);
 431             pragma Loop_Invariant
 432               (for all K in Target'First .. To =>
 433                 Target (K) =
 434                   To_Ada (Item (size_t (K - Target'First) + Item'First)));
 435
 436             --  Avoid possible overflow when incrementing To in the last
 437             --  iteration of the loop.
 438             exit when J = Count;
 439
 440             From := From + 1;
 441             To   := To + 1;
 442          end loop;
 443       end if;
 444    end To_Ada;
 445
 446    --  Convert char16_t to Wide_Character
 447
 448    function To_Ada (Item : char16_t) return Wide_Character is
 449    begin
 450       return Wide_Character'Val (char16_t'Pos (Item));
 451    end To_Ada;
 452
 453    --  Convert char16_array to Wide_String (function form)
 454
 455    function To_Ada
 456      (Item     : char16_array;
 457       Trim_Nul : Boolean := True) return Wide_String
 458    is
 459       Count : Natural;
 460       From  : size_t;
 461
 462    begin
 463       if Trim_Nul then
 464          From := Item'First;
 465
 466          loop
 467             pragma Loop_Invariant (From in Item'Range);
 468             pragma Loop_Invariant
 469               (for some J in From .. Item'Last => Item (J) = char16_nul);
 470             pragma Loop_Invariant
 471               (for all J in Item'First .. From when J /= From =>
 472                  Item (J) /= char16_nul);
 473             pragma Loop_Variant (Increases => From);
 474
 475             if From > Item'Last then
 476                raise Terminator_Error;
 477             elsif Item (From) = char16_nul then
 478                exit;
 479             else
 480                From := From + 1;
 481             end if;
 482          end loop;
 483
 484          pragma Assert (From = Item'First + C_Length_Ghost (Item));
 485
 486          Count := Natural (From - Item'First);
 487
 488       else
 489          Count := Item'Length;
 490       end if;
 491
 492       declare
 493          Count_Cst : constant Natural := Count;
 494          R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 495
 496       begin
 497          for J in R'Range loop
 498             R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
 499
 500             pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
 501             pragma Loop_Invariant
 502               (for all K in 1 .. J =>
 503                 R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
 504          end loop;
 505
 506          return R;
 507       end;
 508    end To_Ada;
 509
 510    --  Convert char16_array to Wide_String (procedure form)
 511
 512    procedure To_Ada
 513      (Item     : char16_array;
 514       Target   : out Wide_String;
 515       Count    : out Natural;
 516       Trim_Nul : Boolean := True)
 517    is
 518       From : size_t;
 519       To   : Integer;
 520
 521    begin
 522       if Trim_Nul then
 523          From := Item'First;
 524          loop
 525             pragma Loop_Invariant (From in Item'Range);
 526             pragma Loop_Invariant
 527               (for some J in From .. Item'Last => Item (J) = char16_nul);
 528             pragma Loop_Invariant
 529               (for all J in Item'First .. From when J /= From =>
 530                 Item (J) /= char16_nul);
 531             pragma Loop_Variant (Increases => From);
 532
 533             if From > Item'Last then
 534                raise Terminator_Error;
 535             elsif Item (From) = char16_nul then
 536                exit;
 537             else
 538                From := From + 1;
 539             end if;
 540          end loop;
 541
 542          Count := Natural (From - Item'First);
 543
 544       else
 545          Count := Item'Length;
 546       end if;
 547
 548       if Count > Target'Length then
 549          raise Constraint_Error;
 550
 551       else
 552          From := Item'First;
 553          To   := Target'First;
 554
 555          for J in 1 .. Count loop
 556             Target (To) := To_Ada (Item (From));
 557
 558             pragma Loop_Invariant (From in Item'Range);
 559             pragma Loop_Invariant (To in Target'Range);
 560             pragma Loop_Invariant (To = Target'First + (J - 1));
 561             pragma Loop_Invariant (From = Item'First + size_t (J - 1));
 562             pragma Loop_Invariant
 563               (for all J in Target'First .. To => Target (J)'Initialized);
 564             pragma Loop_Invariant
 565               (Target (Target'First .. To)'Initialized);
 566             pragma Loop_Invariant
 567               (for all K in Target'First .. To =>
 568                 Target (K) =
 569                   To_Ada (Item (size_t (K - Target'First) + Item'First)));
 570
 571             --  Avoid possible overflow when incrementing To in the last
 572             --  iteration of the loop.
 573             exit when J = Count;
 574
 575             From := From + 1;
 576             To   := To + 1;
 577          end loop;
 578       end if;
 579    end To_Ada;
 580
 581    --  Convert char32_t to Wide_Wide_Character
 582
 583    function To_Ada (Item : char32_t) return Wide_Wide_Character is
 584    begin
 585       return Wide_Wide_Character'Val (char32_t'Pos (Item));
 586    end To_Ada;
 587
 588    --  Convert char32_array to Wide_Wide_String (function form)
 589
 590    function To_Ada
 591      (Item     : char32_array;
 592       Trim_Nul : Boolean := True) return Wide_Wide_String
 593    is
 594       Count : Natural;
 595       From  : size_t;
 596
 597    begin
 598       if Trim_Nul then
 599          From := Item'First;
 600
 601          loop
 602             pragma Loop_Invariant (From in Item'Range);
 603             pragma Loop_Invariant
 604               (for some J in From .. Item'Last => Item (J) = char32_nul);
 605             pragma Loop_Invariant
 606               (for all J in Item'First .. From when J /= From =>
 607                  Item (J) /= char32_nul);
 608             pragma Loop_Invariant (From <= Item'First + C_Length_Ghost (Item));
 609             pragma Loop_Variant (Increases => From);
 610
 611             if From > Item'Last then
 612                raise Terminator_Error;
 613             elsif Item (From) = char32_nul then
 614                exit;
 615             else
 616                From := From + 1;
 617             end if;
 618          end loop;
 619
 620          pragma Assert (From = Item'First + C_Length_Ghost (Item));
 621
 622          Count := Natural (From - Item'First);
 623
 624       else
 625          Count := Item'Length;
 626       end if;
 627
 628       declare
 629          Count_Cst : constant Natural := Count;
 630          R : Wide_Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 631
 632       begin
 633          for J in R'Range loop
 634             R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
 635
 636             pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
 637             pragma Loop_Invariant
 638               (for all K in 1 .. J =>
 639                 R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
 640          end loop;
 641
 642          return R;
 643       end;
 644    end To_Ada;
 645
 646    --  Convert char32_array to Wide_Wide_String (procedure form)
 647
 648    procedure To_Ada
 649      (Item     : char32_array;
 650       Target   : out Wide_Wide_String;
 651       Count    : out Natural;
 652       Trim_Nul : Boolean := True)
 653    is
 654       From : size_t;
 655       To   : Integer;
 656
 657    begin
 658       if Trim_Nul then
 659          From := Item'First;
 660          loop
 661             pragma Loop_Invariant (From in Item'Range);
 662             pragma Loop_Invariant
 663               (for some J in From .. Item'Last => Item (J) = char32_nul);
 664             pragma Loop_Invariant
 665               (for all J in Item'First .. From when J /= From =>
 666                 Item (J) /= char32_nul);
 667             pragma Loop_Variant (Increases => From);
 668
 669             if From > Item'Last then
 670                raise Terminator_Error;
 671             elsif Item (From) = char32_nul then
 672                exit;
 673             else
 674                From := From + 1;
 675             end if;
 676          end loop;
 677
 678          Count := Natural (From - Item'First);
 679
 680       else
 681          Count := Item'Length;
 682       end if;
 683
 684       if Count > Target'Length then
 685          raise Constraint_Error;
 686
 687       else
 688          From := Item'First;
 689          To   := Target'First;
 690
 691          for J in 1 .. Count loop
 692             Target (To) := To_Ada (Item (From));
 693
 694             pragma Loop_Invariant (From in Item'Range);
 695             pragma Loop_Invariant (To in Target'Range);
 696             pragma Loop_Invariant (To = Target'First + (J - 1));
 697             pragma Loop_Invariant (From = Item'First + size_t (J - 1));
 698             pragma Loop_Invariant
 699               (for all J in Target'First .. To => Target (J)'Initialized);
 700             pragma Loop_Invariant
 701               (Target (Target'First .. To)'Initialized);
 702             pragma Loop_Invariant
 703               (for all K in Target'First .. To =>
 704                 Target (K) =
 705                   To_Ada (Item (size_t (K - Target'First) + Item'First)));
 706
 707             --  Avoid possible overflow when incrementing To in the last
 708             --  iteration of the loop.
 709             exit when J = Count;
 710
 711             From := From + 1;
 712             To   := To + 1;
 713          end loop;
 714       end if;
 715    end To_Ada;
 716
 717    ----------
 718    -- To_C --
 719    ----------
 720
 721    --  Convert Character to char
 722
 723    function To_C (Item : Character) return char is
 724    begin
 725       return char'Val (Character'Pos (Item));
 726    end To_C;
 727
 728    --  Convert String to char_array (function form)
 729
 730    function To_C
 731      (Item       : String;
 732       Append_Nul : Boolean := True) return char_array
 733    is
 734    begin
 735       if Append_Nul then
 736          declare
 737             R : char_array (0 .. Item'Length) with Relaxed_Initialization;
 738
 739          begin
 740             for J in Item'Range loop
 741                R (size_t (J - Item'First)) := To_C (Item (J));
 742
 743                pragma Loop_Invariant
 744                  (for all K in 0 .. size_t (J - Item'First) =>
 745                     R (K)'Initialized);
 746                pragma Loop_Invariant
 747                  (for all K in Item'First .. J =>
 748                     R (size_t (K - Item'First)) = To_C (Item (K)));
 749             end loop;
 750
 751             R (R'Last) := nul;
 752
 753             pragma Assert
 754               (for all J in Item'Range =>
 755                  R (size_t (J - Item'First)) = To_C (Item (J)));
 756
 757             return R;
 758          end;
 759
 760       --  Append_Nul False
 761
 762       else
 763          --  A nasty case, if the string is null, we must return a null
 764          --  char_array. The lower bound of this array is required to be zero
 765          --  (RM B.3(50)) but that is of course impossible given that size_t
 766          --  is unsigned. According to Ada 2005 AI-258, the result is to raise
 767          --  Constraint_Error. This is also the appropriate behavior in Ada 95,
 768          --  since nothing else makes sense.
 769
 770          if Item'Length = 0 then
 771             raise Constraint_Error;
 772
 773          --  Normal case
 774
 775          else
 776             declare
 777                R : char_array (0 .. Item'Length - 1)
 778                  with Relaxed_Initialization;
 779
 780             begin
 781                for J in Item'Range loop
 782                   R (size_t (J - Item'First)) := To_C (Item (J));
 783
 784                   pragma Loop_Invariant
 785                     (for all K in 0 .. size_t (J - Item'First) =>
 786                        R (K)'Initialized);
 787                   pragma Loop_Invariant
 788                     (for all K in Item'First .. J =>
 789                        R (size_t (K - Item'First)) = To_C (Item (K)));
 790                end loop;
 791
 792                return R;
 793             end;
 794          end if;
 795       end if;
 796    end To_C;
 797
 798    --  Convert String to char_array (procedure form)
 799
 800    procedure To_C
 801      (Item       : String;
 802       Target     : out char_array;
 803       Count      : out size_t;
 804       Append_Nul : Boolean := True)
 805    is
 806       To : size_t;
 807
 808    begin
 809       if Target'Length < Item'Length then
 810          raise Constraint_Error;
 811
 812       else
 813          To := Target'First;
 814          for From in Item'Range loop
 815             Target (To) := char (Item (From));
 816
 817             pragma Loop_Invariant (To in Target'Range);
 818             pragma Loop_Invariant
 819               (To - Target'First = size_t (From - Item'First));
 820             pragma Loop_Invariant
 821               (for all J in Target'First .. To => Target (J)'Initialized);
 822             pragma Loop_Invariant
 823               (Target (Target'First .. To)'Initialized);
 824             pragma Loop_Invariant
 825               (for all J in Item'First .. From =>
 826                  Target (Target'First + size_t (J - Item'First)) =
 827                    To_C (Item (J)));
 828
 829             To := To + 1;
 830          end loop;
 831
 832          if Append_Nul then
 833             if To > Target'Last then
 834                raise Constraint_Error;
 835             else
 836                Target (To) := nul;
 837                Count := Item'Length + 1;
 838             end if;
 839
 840          else
 841             Count := Item'Length;
 842          end if;
 843       end if;
 844    end To_C;
 845
 846    --  Convert Wide_Character to wchar_t
 847
 848    function To_C (Item : Wide_Character) return wchar_t is
 849    begin
 850       return wchar_t (Item);
 851    end To_C;
 852
 853    --  Convert Wide_String to wchar_array (function form)
 854
 855    function To_C
 856      (Item       : Wide_String;
 857       Append_Nul : Boolean := True) return wchar_array
 858    is
 859    begin
 860       if Append_Nul then
 861          declare
 862             R : wchar_array (0 .. Item'Length) with Relaxed_Initialization;
 863
 864          begin
 865             for J in Item'Range loop
 866                R (size_t (J - Item'First)) := To_C (Item (J));
 867
 868                pragma Loop_Invariant
 869                  (for all K in 0 .. size_t (J - Item'First) =>
 870                     R (K)'Initialized);
 871                pragma Loop_Invariant
 872                  (for all K in Item'First .. J =>
 873                     R (size_t (K - Item'First)) = To_C (Item (K)));
 874             end loop;
 875
 876             R (R'Last) := wide_nul;
 877
 878             pragma Assert
 879               (for all J in Item'Range =>
 880                  R (size_t (J - Item'First)) = To_C (Item (J)));
 881
 882             return R;
 883          end;
 884
 885       else
 886          --  A nasty case, if the string is null, we must return a null
 887          --  wchar_array. The lower bound of this array is required to be zero
 888          --  (RM B.3(50)) but that is of course impossible given that size_t
 889          --  is unsigned. According to Ada 2005 AI-258, the result is to raise
 890          --  Constraint_Error. This is also the appropriate behavior in Ada 95,
 891          --  since nothing else makes sense.
 892
 893          if Item'Length = 0 then
 894             raise Constraint_Error;
 895
 896          else
 897             declare
 898                R : wchar_array (0 .. Item'Length - 1)
 899                  with Relaxed_Initialization;
 900
 901             begin
 902                for J in Item'Range loop
 903                   R (size_t (J - Item'First)) := To_C (Item (J));
 904
 905                   pragma Loop_Invariant
 906                     (for all K in 0 .. size_t (J - Item'First) =>
 907                        R (K)'Initialized);
 908                   pragma Loop_Invariant
 909                     (for all K in Item'First .. J =>
 910                        R (size_t (K - Item'First)) = To_C (Item (K)));
 911                end loop;
 912
 913                return R;
 914             end;
 915          end if;
 916       end if;
 917    end To_C;
 918
 919    --  Convert Wide_String to wchar_array (procedure form)
 920
 921    procedure To_C
 922      (Item       : Wide_String;
 923       Target     : out wchar_array;
 924       Count      : out size_t;
 925       Append_Nul : Boolean := True)
 926    is
 927       To : size_t;
 928
 929    begin
 930       if Target'Length < Item'Length then
 931          raise Constraint_Error;
 932
 933       else
 934          To := Target'First;
 935          for From in Item'Range loop
 936             Target (To) := To_C (Item (From));
 937
 938             pragma Loop_Invariant (To in Target'Range);
 939             pragma Loop_Invariant
 940               (To - Target'First = size_t (From - Item'First));
 941             pragma Loop_Invariant
 942               (for all J in Target'First .. To => Target (J)'Initialized);
 943             pragma Loop_Invariant
 944               (Target (Target'First .. To)'Initialized);
 945             pragma Loop_Invariant
 946               (for all J in Item'First .. From =>
 947                 Target (Target'First + size_t (J - Item'First)) =
 948                   To_C (Item (J)));
 949
 950             To := To + 1;
 951          end loop;
 952
 953          pragma Assert
 954            (for all J in Item'Range =>
 955              Target (Target'First + size_t (J - Item'First)) =
 956                To_C (Item (J)));
 957          pragma Assert
 958            (if Item'Length /= 0 then
 959              Target (Target'First ..
 960                      Target'First + (Item'Length - 1))'Initialized);
 961
 962          if Append_Nul then
 963             if To > Target'Last then
 964                raise Constraint_Error;
 965             else
 966                Target (To) := wide_nul;
 967                Count := Item'Length + 1;
 968             end if;
 969
 970          else
 971             Count := Item'Length;
 972          end if;
 973       end if;
 974    end To_C;
 975
 976    --  Convert Wide_Character to char16_t
 977
 978    function To_C (Item : Wide_Character) return char16_t is
 979    begin
 980       return char16_t'Val (Wide_Character'Pos (Item));
 981    end To_C;
 982
 983    --  Convert Wide_String to char16_array (function form)
 984
 985    function To_C
 986      (Item       : Wide_String;
 987       Append_Nul : Boolean := True) return char16_array
 988    is
 989    begin
 990       if Append_Nul then
 991          declare
 992             R : char16_array (0 .. Item'Length) with Relaxed_Initialization;
 993
 994          begin
 995             for J in Item'Range loop
 996                R (size_t (J - Item'First)) := To_C (Item (J));
 997
 998                pragma Loop_Invariant
 999                  (for all K in 0 .. size_t (J - Item'First) =>
1000                     R (K)'Initialized);
1001                pragma Loop_Invariant
1002                  (for all K in Item'First .. J =>
1003                     R (size_t (K - Item'First)) = To_C (Item (K)));
1004             end loop;
1005
1006             R (R'Last) := char16_nul;
1007
1008             pragma Assert
1009               (for all J in Item'Range =>
1010                  R (size_t (J - Item'First)) = To_C (Item (J)));
1011
1012             return R;
1013          end;
1014
1015       else
1016          --  A nasty case, if the string is null, we must return a null
1017          --  char16_array. The lower bound of this array is required to be zero
1018          --  (RM B.3(50)) but that is of course impossible given that size_t
1019          --  is unsigned. According to Ada 2005 AI-258, the result is to raise
1020          --  Constraint_Error. This is also the appropriate behavior in Ada 95,
1021          --  since nothing else makes sense.
1022
1023          if Item'Length = 0 then
1024             raise Constraint_Error;
1025
1026          else
1027             declare
1028                R : char16_array (0 .. Item'Length - 1)
1029                  with Relaxed_Initialization;
1030
1031             begin
1032                for J in Item'Range loop
1033                   R (size_t (J - Item'First)) := To_C (Item (J));
1034
1035                   pragma Loop_Invariant
1036                     (for all K in 0 .. size_t (J - Item'First) =>
1037                        R (K)'Initialized);
1038                   pragma Loop_Invariant
1039                     (for all K in Item'First .. J =>
1040                        R (size_t (K - Item'First)) = To_C (Item (K)));
1041                end loop;
1042
1043                return R;
1044             end;
1045          end if;
1046       end if;
1047    end To_C;
1048
1049    --  Convert Wide_String to char16_array (procedure form)
1050
1051    procedure To_C
1052      (Item       : Wide_String;
1053       Target     : out char16_array;
1054       Count      : out size_t;
1055       Append_Nul : Boolean := True)
1056    is
1057       To : size_t;
1058
1059    begin
1060       if Target'Length < Item'Length then
1061          raise Constraint_Error;
1062
1063       else
1064          To := Target'First;
1065          for From in Item'Range loop
1066             Target (To) := To_C (Item (From));
1067
1068             pragma Loop_Invariant (To in Target'Range);
1069             pragma Loop_Invariant
1070               (To - Target'First = size_t (From - Item'First));
1071             pragma Loop_Invariant
1072               (for all J in Target'First .. To => Target (J)'Initialized);
1073             pragma Loop_Invariant
1074               (Target (Target'First .. To)'Initialized);
1075             pragma Loop_Invariant
1076               (for all J in Item'First .. From =>
1077                 Target (Target'First + size_t (J - Item'First)) =
1078                   To_C (Item (J)));
1079
1080             To := To + 1;
1081          end loop;
1082
1083          pragma Assert
1084            (for all J in Item'Range =>
1085              Target (Target'First + size_t (J - Item'First)) =
1086                To_C (Item (J)));
1087          pragma Assert
1088            (if Item'Length /= 0 then
1089              Target (Target'First ..
1090                      Target'First + (Item'Length - 1))'Initialized);
1091
1092          if Append_Nul then
1093             if To > Target'Last then
1094                raise Constraint_Error;
1095             else
1096                Target (To) := char16_nul;
1097                Count := Item'Length + 1;
1098             end if;
1099
1100          else
1101             Count := Item'Length;
1102          end if;
1103       end if;
1104    end To_C;
1105
1106    --  Convert Wide_Character to char32_t
1107
1108    function To_C (Item : Wide_Wide_Character) return char32_t is
1109    begin
1110       return char32_t'Val (Wide_Wide_Character'Pos (Item));
1111    end To_C;
1112
1113    --  Convert Wide_Wide_String to char32_array (function form)
1114
1115    function To_C
1116      (Item       : Wide_Wide_String;
1117       Append_Nul : Boolean := True) return char32_array
1118    is
1119    begin
1120       if Append_Nul then
1121          declare
1122             R : char32_array (0 .. Item'Length) with Relaxed_Initialization;
1123
1124          begin
1125             for J in Item'Range loop
1126                R (size_t (J - Item'First)) := To_C (Item (J));
1127
1128                pragma Loop_Invariant
1129                  (for all K in 0 .. size_t (J - Item'First) =>
1130                     R (K)'Initialized);
1131                pragma Loop_Invariant
1132                  (for all K in Item'First .. J =>
1133                     R (size_t (K - Item'First)) = To_C (Item (K)));
1134             end loop;
1135
1136             R (R'Last) := char32_nul;
1137
1138             pragma Assert
1139               (for all J in Item'Range =>
1140                  R (size_t (J - Item'First)) = To_C (Item (J)));
1141
1142             return R;
1143          end;
1144
1145       else
1146          --  A nasty case, if the string is null, we must return a null
1147          --  char32_array. The lower bound of this array is required to be zero
1148          --  (RM B.3(50)) but that is of course impossible given that size_t
1149          --  is unsigned. According to Ada 2005 AI-258, the result is to raise
1150          --  Constraint_Error.
1151
1152          if Item'Length = 0 then
1153             raise Constraint_Error;
1154
1155          else
1156             declare
1157                R : char32_array (0 .. Item'Length - 1)
1158                  with Relaxed_Initialization;
1159
1160             begin
1161                for J in Item'Range loop
1162                   R (size_t (J - Item'First)) := To_C (Item (J));
1163
1164                   pragma Loop_Invariant
1165                     (for all K in 0 .. size_t (J - Item'First) =>
1166                        R (K)'Initialized);
1167                   pragma Loop_Invariant
1168                     (for all K in Item'First .. J =>
1169                        R (size_t (K - Item'First)) = To_C (Item (K)));
1170                end loop;
1171
1172                return R;
1173             end;
1174          end if;
1175       end if;
1176    end To_C;
1177
1178    --  Convert Wide_Wide_String to char32_array (procedure form)
1179
1180    procedure To_C
1181      (Item       : Wide_Wide_String;
1182       Target     : out char32_array;
1183       Count      : out size_t;
1184       Append_Nul : Boolean := True)
1185    is
1186       To : size_t;
1187
1188    begin
1189       if Target'Length < Item'Length + (if Append_Nul then 1 else 0) then
1190          raise Constraint_Error;
1191
1192       else
1193          To := Target'First;
1194          for From in Item'Range loop
1195             Target (To) := To_C (Item (From));
1196
1197             pragma Loop_Invariant (To in Target'Range);
1198             pragma Loop_Invariant
1199               (To - Target'First = size_t (From - Item'First));
1200             pragma Loop_Invariant
1201               (for all J in Target'First .. To => Target (J)'Initialized);
1202             pragma Loop_Invariant
1203               (Target (Target'First .. To)'Initialized);
1204             pragma Loop_Invariant
1205               (for all J in Item'First .. From =>
1206                 Target (Target'First + size_t (J - Item'First)) =
1207                   To_C (Item (J)));
1208
1209             To := To + 1;
1210          end loop;
1211
1212          pragma Assert
1213            (for all J in Item'Range =>
1214              Target (Target'First + size_t (J - Item'First)) =
1215                To_C (Item (J)));
1216          pragma Assert
1217            (if Item'Length /= 0 then
1218              Target (Target'First ..
1219                      Target'First + (Item'Length - 1))'Initialized);
1220
1221          if Append_Nul then
1222             Target (To) := char32_nul;
1223             Count := Item'Length + 1;
1224          else
1225             Count := Item'Length;
1226          end if;
1227       end if;
1228    end To_C;
1229    pragma Annotate (CodePeer, False_Positive, "validity check",
1230      "Count is only uninitialized on abnormal return.");
1231
1232 end Interfaces.C;