Showing error 278

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