Showing error 259

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