Showing error 279

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