Showing error 2337

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

Source: 

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