Showing error 256

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