Showing error 2317

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