Showing error 2319

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