Showing error 254

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