User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | systemc/token_ring.07.BUG.cil.c |
Line in file: | 8 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
1/* Generated by CIL v. 1.3.6 */ 2/* print_CIL_Input is true */ 3 4void error(void) 5{ 6 7 { 8 ERROR: ; 9 goto ERROR; 10 return; 11} 12} 13int m_pc = 0; 14int t1_pc = 0; 15int t2_pc = 0; 16int t3_pc = 0; 17int t4_pc = 0; 18int t5_pc = 0; 19int t6_pc = 0; 20int t7_pc = 0; 21int m_st ; 22int t1_st ; 23int t2_st ; 24int t3_st ; 25int t4_st ; 26int t5_st ; 27int t6_st ; 28int t7_st ; 29int m_i ; 30int t1_i ; 31int t2_i ; 32int t3_i ; 33int t4_i ; 34int t5_i ; 35int t6_i ; 36int t7_i ; 37int M_E = 2; 38int T1_E = 2; 39int T2_E = 2; 40int T3_E = 2; 41int T4_E = 2; 42int T5_E = 2; 43int T6_E = 2; 44int T7_E = 2; 45int E_M = 2; 46int E_1 = 2; 47int E_2 = 2; 48int E_3 = 2; 49int E_4 = 2; 50int E_5 = 2; 51int E_6 = 2; 52int E_7 = 2; 53int is_master_triggered(void) ; 54int is_transmit1_triggered(void) ; 55int is_transmit2_triggered(void) ; 56int is_transmit3_triggered(void) ; 57int is_transmit4_triggered(void) ; 58int is_transmit5_triggered(void) ; 59int is_transmit6_triggered(void) ; 60int is_transmit7_triggered(void) ; 61void immediate_notify(void) ; 62int token ; 63int __VERIFIER_nondet_int() ; 64int local ; 65void master(void) 66{ 67int tmp_var ; 68 { 69 if (m_pc == 0) { 70 goto M_ENTRY; 71 } else { 72 if (m_pc == 1) { 73 goto M_WAIT; 74 } else { 75 76 } 77 } 78 M_ENTRY: ; 79 { 80 while (1) { 81 while_0_continue: /* CIL Label */ ; 82 { 83 token = __VERIFIER_nondet_int(); 84 local = token; 85 E_1 = 1; 86 immediate_notify(); 87 E_1 = 2; 88 m_pc = 1; 89 m_st = 2; 90 } 91 92 goto return_label; 93 M_WAIT: ; 94 if (token != local + 7) { 95 { 96 error(); 97 } 98 } else { 99 if(tmp_var <= 5){ 100 if(tmp_var >= 5){ 101 102 } 103 } 104 105 if(tmp_var <= 5){ 106 if(tmp_var >= 5){ 107 if(tmp_var == 5){ 108 error(); 109 } 110 } 111 } 112 } 113 } 114 while_0_break: /* CIL Label */ ; 115 } 116 117 return_label: /* CIL Label */ 118 return; 119} 120} 121void transmit1(void) 122{ 123 124 { 125 if (t1_pc == 0) { 126 goto T1_ENTRY; 127 } else { 128 if (t1_pc == 1) { 129 goto T1_WAIT; 130 } else { 131 132 } 133 } 134 T1_ENTRY: ; 135 { 136 while (1) { 137 while_1_continue: /* CIL Label */ ; 138 t1_pc = 1; 139 t1_st = 2; 140 141 goto return_label; 142 T1_WAIT: 143 { 144 token += 1; 145 E_2 = 1; 146 immediate_notify(); 147 E_2 = 2; 148 } 149 } 150 while_1_break: /* CIL Label */ ; 151 } 152 153 return_label: /* CIL Label */ 154 return; 155} 156} 157void transmit2(void) 158{ 159 160 { 161 if (t2_pc == 0) { 162 goto T2_ENTRY; 163 } else { 164 if (t2_pc == 1) { 165 goto T2_WAIT; 166 } else { 167 168 } 169 } 170 T2_ENTRY: ; 171 { 172 while (1) { 173 while_2_continue: /* CIL Label */ ; 174 t2_pc = 1; 175 t2_st = 2; 176 177 goto return_label; 178 T2_WAIT: 179 { 180 token += 1; 181 E_3 = 1; 182 immediate_notify(); 183 E_3 = 2; 184 } 185 } 186 while_2_break: /* CIL Label */ ; 187 } 188 189 return_label: /* CIL Label */ 190 return; 191} 192} 193void transmit3(void) 194{ 195 196 { 197 if (t3_pc == 0) { 198 goto T3_ENTRY; 199 } else { 200 if (t3_pc == 1) { 201 goto T3_WAIT; 202 } else { 203 204 } 205 } 206 T3_ENTRY: ; 207 { 208 while (1) { 209 while_3_continue: /* CIL Label */ ; 210 t3_pc = 1; 211 t3_st = 2; 212 213 goto return_label; 214 T3_WAIT: 215 { 216 token += 1; 217 E_4 = 1; 218 immediate_notify(); 219 E_4 = 2; 220 } 221 } 222 while_3_break: /* CIL Label */ ; 223 } 224 225 return_label: /* CIL Label */ 226 return; 227} 228} 229void transmit4(void) 230{ 231 232 { 233 if (t4_pc == 0) { 234 goto T4_ENTRY; 235 } else { 236 if (t4_pc == 1) { 237 goto T4_WAIT; 238 } else { 239 240 } 241 } 242 T4_ENTRY: ; 243 { 244 while (1) { 245 while_4_continue: /* CIL Label */ ; 246 t4_pc = 1; 247 t4_st = 2; 248 249 goto return_label; 250 T4_WAIT: 251 { 252 token += 1; 253 E_5 = 1; 254 immediate_notify(); 255 E_5 = 2; 256 } 257 } 258 while_4_break: /* CIL Label */ ; 259 } 260 261 return_label: /* CIL Label */ 262 return; 263} 264} 265void transmit5(void) 266{ 267 268 { 269 if (t5_pc == 0) { 270 goto T5_ENTRY; 271 } else { 272 if (t5_pc == 1) { 273 goto T5_WAIT; 274 } else { 275 276 } 277 } 278 T5_ENTRY: ; 279 { 280 while (1) { 281 while_5_continue: /* CIL Label */ ; 282 t5_pc = 1; 283 t5_st = 2; 284 285 goto return_label; 286 T5_WAIT: 287 { 288 token += 1; 289 E_6 = 1; 290 immediate_notify(); 291 E_6 = 2; 292 } 293 } 294 while_5_break: /* CIL Label */ ; 295 } 296 297 return_label: /* CIL Label */ 298 return; 299} 300} 301void transmit6(void) 302{ 303 304 { 305 if (t6_pc == 0) { 306 goto T6_ENTRY; 307 } else { 308 if (t6_pc == 1) { 309 goto T6_WAIT; 310 } else { 311 312 } 313 } 314 T6_ENTRY: ; 315 { 316 while (1) { 317 while_6_continue: /* CIL Label */ ; 318 t6_pc = 1; 319 t6_st = 2; 320 321 goto return_label; 322 T6_WAIT: 323 { 324 token += 1; 325 E_7 = 1; 326 immediate_notify(); 327 E_7 = 2; 328 } 329 } 330 while_6_break: /* CIL Label */ ; 331 } 332 333 return_label: /* CIL Label */ 334 return; 335} 336} 337void transmit7(void) 338{ 339 340 { 341 if (t7_pc == 0) { 342 goto T7_ENTRY; 343 } else { 344 if (t7_pc == 1) { 345 goto T7_WAIT; 346 } else { 347 348 } 349 } 350 T7_ENTRY: ; 351 { 352 while (1) { 353 while_7_continue: /* CIL Label */ ; 354 t7_pc = 1; 355 t7_st = 2; 356 357 goto return_label; 358 T7_WAIT: 359 { 360 token += 1; 361 E_M = 1; 362 immediate_notify(); 363 E_M = 2; 364 } 365 } 366 while_7_break: /* CIL Label */ ; 367 } 368 369 return_label: /* CIL Label */ 370 return; 371} 372} 373int is_master_triggered(void) 374{ int __retres1 ; 375 376 { 377 if (m_pc == 1) { 378 if (E_M == 1) { 379 __retres1 = 1; 380 goto return_label; 381 } else { 382 383 } 384 } else { 385 386 } 387 __retres1 = 0; 388 return_label: /* CIL Label */ 389 return (__retres1); 390} 391} 392int is_transmit1_triggered(void) 393{ int __retres1 ; 394 395 { 396 if (t1_pc == 1) { 397 if (E_1 == 1) { 398 __retres1 = 1; 399 goto return_label; 400 } else { 401 402 } 403 } else { 404 405 } 406 __retres1 = 0; 407 return_label: /* CIL Label */ 408 return (__retres1); 409} 410} 411int is_transmit2_triggered(void) 412{ int __retres1 ; 413 414 { 415 if (t2_pc == 1) { 416 if (E_2 == 1) { 417 __retres1 = 1; 418 goto return_label; 419 } else { 420 421 } 422 } else { 423 424 } 425 __retres1 = 0; 426 return_label: /* CIL Label */ 427 return (__retres1); 428} 429} 430int is_transmit3_triggered(void) 431{ int __retres1 ; 432 433 { 434 if (t3_pc == 1) { 435 if (E_3 == 1) { 436 __retres1 = 1; 437 goto return_label; 438 } else { 439 440 } 441 } else { 442 443 } 444 __retres1 = 0; 445 return_label: /* CIL Label */ 446 return (__retres1); 447} 448} 449int is_transmit4_triggered(void) 450{ int __retres1 ; 451 452 { 453 if (t4_pc == 1) { 454 if (E_4 == 1) { 455 __retres1 = 1; 456 goto return_label; 457 } else { 458 459 } 460 } else { 461 462 } 463 __retres1 = 0; 464 return_label: /* CIL Label */ 465 return (__retres1); 466} 467} 468int is_transmit5_triggered(void) 469{ int __retres1 ; 470 471 { 472 if (t5_pc == 1) { 473 if (E_5 == 1) { 474 __retres1 = 1; 475 goto return_label; 476 } else { 477 478 } 479 } else { 480 481 } 482 __retres1 = 0; 483 return_label: /* CIL Label */ 484 return (__retres1); 485} 486} 487int is_transmit6_triggered(void) 488{ int __retres1 ; 489 490 { 491 if (t6_pc == 1) { 492 if (E_6 == 1) { 493 __retres1 = 1; 494 goto return_label; 495 } else { 496 497 } 498 } else { 499 500 } 501 __retres1 = 0; 502 return_label: /* CIL Label */ 503 return (__retres1); 504} 505} 506int is_transmit7_triggered(void) 507{ int __retres1 ; 508 509 { 510 if (t7_pc == 1) { 511 if (E_7 == 1) { 512 __retres1 = 1; 513 goto return_label; 514 } else { 515 516 } 517 } else { 518 519 } 520 __retres1 = 0; 521 return_label: /* CIL Label */ 522 return (__retres1); 523} 524} 525void update_channels(void) 526{ 527 528 { 529 530 return; 531} 532} 533void init_threads(void) 534{ 535 536 { 537 if (m_i == 1) { 538 m_st = 0; 539 } else { 540 m_st = 2; 541 } 542 if (t1_i == 1) { 543 t1_st = 0; 544 } else { 545 t1_st = 2; 546 } 547 if (t2_i == 1) { 548 t2_st = 0; 549 } else { 550 t2_st = 2; 551 } 552 if (t3_i == 1) { 553 t3_st = 0; 554 } else { 555 t3_st = 2; 556 } 557 if (t4_i == 1) { 558 t4_st = 0; 559 } else { 560 t4_st = 2; 561 } 562 if (t5_i == 1) { 563 t5_st = 0; 564 } else { 565 t5_st = 2; 566 } 567 if (t6_i == 1) { 568 t6_st = 0; 569 } else { 570 t6_st = 2; 571 } 572 if (t7_i == 1) { 573 t7_st = 0; 574 } else { 575 t7_st = 2; 576 } 577 578 return; 579} 580} 581int exists_runnable_thread(void) 582{ int __retres1 ; 583 584 { 585 if (m_st == 0) { 586 __retres1 = 1; 587 goto return_label; 588 } else { 589 if (t1_st == 0) { 590 __retres1 = 1; 591 goto return_label; 592 } else { 593 if (t2_st == 0) { 594 __retres1 = 1; 595 goto return_label; 596 } else { 597 if (t3_st == 0) { 598 __retres1 = 1; 599 goto return_label; 600 } else { 601 if (t4_st == 0) { 602 __retres1 = 1; 603 goto return_label; 604 } else { 605 if (t5_st == 0) { 606 __retres1 = 1; 607 goto return_label; 608 } else { 609 if (t6_st == 0) { 610 __retres1 = 1; 611 goto return_label; 612 } else { 613 if (t7_st == 0) { 614 __retres1 = 1; 615 goto return_label; 616 } else { 617 618 } 619 } 620 } 621 } 622 } 623 } 624 } 625 } 626 __retres1 = 0; 627 return_label: /* CIL Label */ 628 return (__retres1); 629} 630} 631void eval(void) 632{// int __VERIFIER_nondet_int() ; 633 int tmp ; 634 635 { 636 { 637 while (1) { 638 while_8_continue: /* CIL Label */ ; 639 { 640 tmp = exists_runnable_thread(); 641 } 642 if (tmp) { 643 644 } else { 645 goto while_8_break; 646 } 647 if (m_st == 0) { 648 int tmp_ndt_1; 649 tmp_ndt_1 = __VERIFIER_nondet_int(); 650 if (tmp_ndt_1) { 651 { 652 m_st = 1; 653 master(); 654 } 655 } else { 656 657 } 658 } else { 659 660 } 661 if (t1_st == 0) { 662 int tmp_ndt_2; 663 tmp_ndt_2 = __VERIFIER_nondet_int(); 664 if (tmp_ndt_2) { 665 { 666 t1_st = 1; 667 transmit1(); 668 } 669 } else { 670 671 } 672 } else { 673 674 } 675 if (t2_st == 0) { 676 int tmp_ndt_3; 677 tmp_ndt_3 = __VERIFIER_nondet_int(); 678 if (tmp_ndt_3) { 679 { 680 t2_st = 1; 681 transmit2(); 682 } 683 } else { 684 685 } 686 } else { 687 688 } 689 if (t3_st == 0) { 690 int tmp_ndt_4; 691 tmp_ndt_4 = __VERIFIER_nondet_int(); 692 if (tmp_ndt_4) { 693 { 694 t3_st = 1; 695 transmit3(); 696 } 697 } else { 698 699 } 700 } else { 701 702 } 703 if (t4_st == 0) { 704 int tmp_ndt_5; 705 tmp_ndt_5 = __VERIFIER_nondet_int(); 706 if (tmp_ndt_5) { 707 { 708 t4_st = 1; 709 transmit4(); 710 } 711 } else { 712 713 } 714 } else { 715 716 } 717 if (t5_st == 0) { 718 int tmp_ndt_6; 719 tmp_ndt_6 = __VERIFIER_nondet_int(); 720 if (tmp_ndt_6) { 721 { 722 t5_st = 1; 723 transmit5(); 724 } 725 } else { 726 727 } 728 } else { 729 730 } 731 if (t6_st == 0) { 732 int tmp_ndt_7; 733 tmp_ndt_7 = __VERIFIER_nondet_int(); 734 if (tmp_ndt_7) { 735 { 736 t6_st = 1; 737 transmit6(); 738 } 739 } else { 740 741 } 742 } else { 743 744 } 745 if (t7_st == 0) { 746 int tmp_ndt_8; 747 tmp_ndt_8 = __VERIFIER_nondet_int(); 748 if (tmp_ndt_8) { 749 { 750 t7_st = 1; 751 transmit7(); 752 } 753 } else { 754 755 } 756 } else { 757 758 } 759 } 760 while_8_break: /* CIL Label */ ; 761 } 762 763 return; 764} 765} 766void fire_delta_events(void) 767{ 768 769 { 770 if (M_E == 0) { 771 M_E = 1; 772 } else { 773 774 } 775 if (T1_E == 0) { 776 T1_E = 1; 777 } else { 778 779 } 780 if (T2_E == 0) { 781 T2_E = 1; 782 } else { 783 784 } 785 if (T3_E == 0) { 786 T3_E = 1; 787 } else { 788 789 } 790 if (T4_E == 0) { 791 T4_E = 1; 792 } else { 793 794 } 795 if (T5_E == 0) { 796 T5_E = 1; 797 } else { 798 799 } 800 if (T6_E == 0) { 801 T6_E = 1; 802 } else { 803 804 } 805 if (T7_E == 0) { 806 T7_E = 1; 807 } else { 808 809 } 810 if (E_M == 0) { 811 E_M = 1; 812 } else { 813 814 } 815 if (E_1 == 0) { 816 E_1 = 1; 817 } else { 818 819 } 820 if (E_2 == 0) { 821 E_2 = 1; 822 } else { 823 824 } 825 if (E_3 == 0) { 826 E_3 = 1; 827 } else { 828 829 } 830 if (E_4 == 0) { 831 E_4 = 1; 832 } else { 833 834 } 835 if (E_5 == 0) { 836 E_5 = 1; 837 } else { 838 839 } 840 if (E_6 == 0) { 841 E_6 = 1; 842 } else { 843 844 } 845 if (E_7 == 0) { 846 E_7 = 1; 847 } else { 848 849 } 850 851 return; 852} 853} 854void reset_delta_events(void) 855{ 856 857 { 858 if (M_E == 1) { 859 M_E = 2; 860 } else { 861 862 } 863 if (T1_E == 1) { 864 T1_E = 2; 865 } else { 866 867 } 868 if (T2_E == 1) { 869 T2_E = 2; 870 } else { 871 872 } 873 if (T3_E == 1) { 874 T3_E = 2; 875 } else { 876 877 } 878 if (T4_E == 1) { 879 T4_E = 2; 880 } else { 881 882 } 883 if (T5_E == 1) { 884 T5_E = 2; 885 } else { 886 887 } 888 if (T6_E == 1) { 889 T6_E = 2; 890 } else { 891 892 } 893 if (T7_E == 1) { 894 T7_E = 2; 895 } else { 896 897 } 898 if (E_M == 1) { 899 E_M = 2; 900 } else { 901 902 } 903 if (E_1 == 1) { 904 E_1 = 2; 905 } else { 906 907 } 908 if (E_2 == 1) { 909 E_2 = 2; 910 } else { 911 912 } 913 if (E_3 == 1) { 914 E_3 = 2; 915 } else { 916 917 } 918 if (E_4 == 1) { 919 E_4 = 2; 920 } else { 921 922 } 923 if (E_5 == 1) { 924 E_5 = 2; 925 } else { 926 927 } 928 if (E_6 == 1) { 929 E_6 = 2; 930 } else { 931 932 } 933 if (E_7 == 1) { 934 E_7 = 2; 935 } else { 936 937 } 938 939 return; 940} 941} 942void activate_threads(void) 943{ int tmp ; 944 int tmp___0 ; 945 int tmp___1 ; 946 int tmp___2 ; 947 int tmp___3 ; 948 int tmp___4 ; 949 int tmp___5 ; 950 int tmp___6 ; 951 952 { 953 { 954 tmp = is_master_triggered(); 955 } 956 if (tmp) { 957 m_st = 0; 958 } else { 959 960 } 961 { 962 tmp___0 = is_transmit1_triggered(); 963 } 964 if (tmp___0) { 965 t1_st = 0; 966 } else { 967 968 } 969 { 970 tmp___1 = is_transmit2_triggered(); 971 } 972 if (tmp___1) { 973 t2_st = 0; 974 } else { 975 976 } 977 { 978 tmp___2 = is_transmit3_triggered(); 979 } 980 if (tmp___2) { 981 t3_st = 0; 982 } else { 983 984 } 985 { 986 tmp___3 = is_transmit4_triggered(); 987 } 988 if (tmp___3) { 989 t4_st = 0; 990 } else { 991 992 } 993 { 994 tmp___4 = is_transmit5_triggered(); 995 } 996 if (tmp___4) { 997 t5_st = 0; 998 } else { 999 1000 } 1001 { 1002 tmp___5 = is_transmit6_triggered(); 1003 } 1004 if (tmp___5) { 1005 t6_st = 0; 1006 } else { 1007 1008 } 1009 { 1010 tmp___6 = is_transmit7_triggered(); 1011 } 1012 if (tmp___6) { 1013 t7_st = 0; 1014 } else { 1015 1016 } 1017 1018 return; 1019} 1020} 1021void immediate_notify(void) 1022{ 1023 1024 { 1025 { 1026 activate_threads(); 1027 } 1028 1029 return; 1030} 1031} 1032void fire_time_events(void) 1033{ 1034 1035 { 1036 M_E = 1; 1037 1038 return; 1039} 1040} 1041void reset_time_events(void) 1042{ 1043 1044 { 1045 if (M_E == 1) { 1046 M_E = 2; 1047 } else { 1048 1049 } 1050 if (T1_E == 1) { 1051 T1_E = 2; 1052 } else { 1053 1054 } 1055 if (T2_E == 1) { 1056 T2_E = 2; 1057 } else { 1058 1059 } 1060 if (T3_E == 1) { 1061 T3_E = 2; 1062 } else { 1063 1064 } 1065 if (T4_E == 1) { 1066 T4_E = 2; 1067 } else { 1068 1069 } 1070 if (T5_E == 1) { 1071 T5_E = 2; 1072 } else { 1073 1074 } 1075 if (T6_E == 1) { 1076 T6_E = 2; 1077 } else { 1078 1079 } 1080 if (T7_E == 1) { 1081 T7_E = 2; 1082 } else { 1083 1084 } 1085 if (E_M == 1) { 1086 E_M = 2; 1087 } else { 1088 1089 } 1090 if (E_1 == 1) { 1091 E_1 = 2; 1092 } else { 1093 1094 } 1095 if (E_2 == 1) { 1096 E_2 = 2; 1097 } else { 1098 1099 } 1100 if (E_3 == 1) { 1101 E_3 = 2; 1102 } else { 1103 1104 } 1105 if (E_4 == 1) { 1106 E_4 = 2; 1107 } else { 1108 1109 } 1110 if (E_5 == 1) { 1111 E_5 = 2; 1112 } else { 1113 1114 } 1115 if (E_6 == 1) { 1116 E_6 = 2; 1117 } else { 1118 1119 } 1120 if (E_7 == 1) { 1121 E_7 = 2; 1122 } else { 1123 1124 } 1125 1126 return; 1127} 1128} 1129void init_model(void) 1130{ 1131 1132 { 1133 m_i = 1; 1134 t1_i = 1; 1135 t2_i = 1; 1136 t3_i = 1; 1137 t4_i = 1; 1138 t5_i = 1; 1139 t6_i = 1; 1140 t7_i = 1; 1141 1142 return; 1143} 1144} 1145int stop_simulation(void) 1146{ int tmp ; 1147 int __retres2 ; 1148 1149 { 1150 { 1151 tmp = exists_runnable_thread(); 1152 } 1153 if (tmp) { 1154 __retres2 = 0; 1155 goto return_label; 1156 } else { 1157 1158 } 1159 __retres2 = 1; 1160 return_label: /* CIL Label */ 1161 return (__retres2); 1162} 1163} 1164void start_simulation(void) 1165{ int kernel_st ; 1166 int tmp ; 1167 int tmp___0 ; 1168 1169 { 1170 { 1171 kernel_st = 0; 1172 update_channels(); 1173 init_threads(); 1174 fire_delta_events(); 1175 activate_threads(); 1176 reset_delta_events(); 1177 } 1178 { 1179 while (1) { 1180 while_9_continue: /* CIL Label */ ; 1181 { 1182 kernel_st = 1; 1183 eval(); 1184 } 1185 { 1186 kernel_st = 2; 1187 update_channels(); 1188 } 1189 { 1190 kernel_st = 3; 1191 fire_delta_events(); 1192 activate_threads(); 1193 reset_delta_events(); 1194 } 1195 { 1196 tmp = exists_runnable_thread(); 1197 } 1198 if (tmp == 0) { 1199 { 1200 kernel_st = 4; 1201 fire_time_events(); 1202 activate_threads(); 1203 reset_time_events(); 1204 } 1205 } else { 1206 1207 } 1208 { 1209 tmp___0 = stop_simulation(); 1210 } 1211 if (tmp___0) { 1212 goto while_9_break; 1213 } else { 1214 1215 } 1216 } 1217 while_9_break: /* CIL Label */ ; 1218 } 1219 1220 return; 1221} 1222} 1223int main(void) 1224{ int __retres1 ; 1225 1226 { 1227 { 1228 init_model(); 1229 start_simulation(); 1230 } 1231 __retres1 = 0; 1232 return (__retres1); 1233} 1234}