Showing error 2333

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