Showing error 2305

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