Showing error 2330

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/transmitter.08_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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