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