Showing error 2329

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_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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