Showing error 280

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