Showing error 2309

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.09_unsafe.cil.c
Line in file: 8
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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