Showing error 286

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