Showing error 2281

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/mem_slave_tlm.2_safe.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
   3
   4void error(void) 
   5{ 
   6
   7  {
   8  goto ERROR;
   9  ERROR: ;
  10  return;
  11}
  12}
  13
  14int m_run_st  ;
  15int m_run_i  ;
  16int m_run_pc  ;
  17int s_memory0  ;
  18int s_memory1  ;
  19
  20int s_run_st  ;
  21int s_run_i  ;
  22int s_run_pc  ;
  23int c_m_lock  ;
  24int c_m_ev  ;
  25int c_req_type  ;
  26int c_req_a  ;
  27int c_req_d  ;
  28int c_rsp_type  ;
  29int c_rsp_status  ;
  30int c_rsp_d  ;
  31int c_empty_req  ;
  32int c_empty_rsp  ;
  33int c_read_req_ev  ;
  34int c_write_req_ev  ;
  35int c_read_rsp_ev  ;
  36int c_write_rsp_ev  ;
  37static int d_t  ;
  38static int a_t  ;
  39static int req_t_type  ;
  40static int req_t_a  ;
  41static int req_t_d  ;
  42static int rsp_t_type  ;
  43static int rsp_t_status  ;
  44static int rsp_t_d  ;
  45static int req_tt_type  ;
  46static int req_tt_a  ;
  47static int req_tt_d  ;
  48static int rsp_tt_type  ;
  49static int rsp_tt_status  ;
  50static int rsp_tt_d  ;
  51
  52int s_memory_read(int i)
  53{
  54  int x;
  55
  56  if (i==0)
  57    x = s_memory0;
  58  else if (i==1)
  59    x = s_memory1;
  60  else
  61    error();
  62
  63  return (x);
  64}
  65
  66void s_memory_write(int i, int v)
  67{
  68  if (i==0)
  69    s_memory0 = v;
  70  else if (i==1)
  71    s_memory1 = v;
  72  else
  73    error();
  74
  75  return;
  76}
  77
  78
  79void m_run(void) 
  80{ int d ;
  81  int a ;
  82  int req_type ;
  83  int req_a ;
  84  int req_d ;
  85  int rsp_type ;
  86  int rsp_status ;
  87  int rsp_d ;
  88  int req_type___0 ;
  89  int req_a___0 ;
  90  int req_d___0 ;
  91  int rsp_type___0 ;
  92  int rsp_status___0 ;
  93  int rsp_d___0 ;
  94
  95  {
  96  if ((int )m_run_pc == 0) {
  97    goto L_MASTER_RUN_ENTRY;
  98  } else {
  99    if ((int )m_run_pc == 1) {
 100      goto L_MASTER_RUN_MUTEX;
 101    } else {
 102      if ((int )m_run_pc == 2) {
 103        goto L_MASTER_RUN_PUT;
 104      } else {
 105        if ((int )m_run_pc == 3) {
 106          goto L_MASTER_RUN_GET;
 107        } else {
 108          if ((int )m_run_pc == 4) {
 109            goto L_MASTER_RUN_MUTEX2;
 110          } else {
 111            if ((int )m_run_pc == 5) {
 112              goto L_MASTER_RUN_PUT2;
 113            } else {
 114              if ((int )m_run_pc == 6) {
 115                goto L_MASTER_RUN_GET2;
 116              } else {
 117
 118              }
 119            }
 120          }
 121        }
 122      }
 123    }
 124  }
 125  L_MASTER_RUN_ENTRY: 
 126  a = 0;
 127  {
 128  while (1) {
 129    while_0_continue: /* CIL Label */ ;
 130    if (a < 2) {
 131
 132    } else {
 133      goto while_0_break;
 134    }
 135    req_type = 1;
 136    req_a = a;
 137    req_d = a + 50;
 138    {
 139    while (1) {
 140      while_1_continue: /* CIL Label */ ;
 141      if (c_m_lock == 1) {
 142
 143      } else {
 144        goto while_1_break;
 145      }
 146      m_run_st = 2;
 147      m_run_pc = 1;
 148      req_t_type = req_type;
 149      req_t_a = req_a;
 150      req_t_d = req_d;
 151      rsp_t_type = rsp_type;
 152      rsp_t_status = rsp_status;
 153      rsp_t_d = rsp_d;
 154      d_t = d;
 155      a_t = a;
 156
 157      goto return_label;
 158      L_MASTER_RUN_MUTEX: 
 159      req_type = req_t_type;
 160      req_a = req_t_a;
 161      req_d = req_t_d;
 162      rsp_type = rsp_t_type;
 163      rsp_status = rsp_t_status;
 164      rsp_d = rsp_t_d;
 165      d = d_t;
 166      a = a_t;
 167    }
 168    while_1_break: /* CIL Label */ ;
 169    }
 170    c_m_lock = 1;
 171    {
 172    while (1) {
 173      while_2_continue: /* CIL Label */ ;
 174      if ((int )c_empty_req == 0) {
 175
 176      } else {
 177        goto while_2_break;
 178      }
 179      m_run_st = 2;
 180      m_run_pc = 2;
 181      req_t_type = req_type;
 182      req_t_a = req_a;
 183      req_t_d = req_d;
 184      rsp_t_type = rsp_type;
 185      rsp_t_status = rsp_status;
 186      rsp_t_d = rsp_d;
 187      d_t = d;
 188      a_t = a;
 189
 190      goto return_label;
 191      L_MASTER_RUN_PUT: 
 192      req_type = req_t_type;
 193      req_a = req_t_a;
 194      req_d = req_t_d;
 195      rsp_type = rsp_t_type;
 196      rsp_status = rsp_t_status;
 197      rsp_d = rsp_t_d;
 198      a = a_t;
 199      d = d_t;
 200    }
 201    while_2_break: /* CIL Label */ ;
 202    }
 203    c_req_type = req_type;
 204    c_req_a = req_a;
 205    c_req_d = req_d;
 206    c_empty_req = 0;
 207    c_write_req_ev = 1;
 208    if ((int )m_run_pc == 1) {
 209      if ((int )c_m_ev == 1) {
 210        m_run_st = 0;
 211      } else {
 212        goto _L___3;
 213      }
 214    } else {
 215      _L___3: /* CIL Label */ 
 216      if ((int )m_run_pc == 2) {
 217        if ((int )c_read_req_ev == 1) {
 218          m_run_st = 0;
 219        } else {
 220          goto _L___2;
 221        }
 222      } else {
 223        _L___2: /* CIL Label */ 
 224        if ((int )m_run_pc == 3) {
 225          if ((int )c_write_rsp_ev == 1) {
 226            m_run_st = 0;
 227          } else {
 228            goto _L___1;
 229          }
 230        } else {
 231          _L___1: /* CIL Label */ 
 232          if ((int )m_run_pc == 4) {
 233            if ((int )c_m_ev == 1) {
 234              m_run_st = 0;
 235            } else {
 236              goto _L___0;
 237            }
 238          } else {
 239            _L___0: /* CIL Label */ 
 240            if ((int )m_run_pc == 5) {
 241              if ((int )c_read_req_ev == 1) {
 242                m_run_st = 0;
 243              } else {
 244                goto _L;
 245              }
 246            } else {
 247              _L: /* CIL Label */ 
 248              if ((int )m_run_pc == 6) {
 249                if ((int )c_write_rsp_ev == 1) {
 250                  m_run_st = 0;
 251                } else {
 252
 253                }
 254              } else {
 255
 256              }
 257            }
 258          }
 259        }
 260      }
 261    }
 262    if ((int )s_run_pc == 2) {
 263      if ((int )c_write_req_ev == 1) {
 264        s_run_st = 0;
 265      } else {
 266        goto _L___4;
 267      }
 268    } else {
 269      _L___4: /* CIL Label */ 
 270      if ((int )s_run_pc == 1) {
 271        if ((int )c_read_rsp_ev == 1) {
 272          s_run_st = 0;
 273        } else {
 274
 275        }
 276      } else {
 277
 278      }
 279    }
 280    c_write_req_ev = 2;
 281    {
 282    while (1) {
 283      while_3_continue: /* CIL Label */ ;
 284      if ((int )c_empty_rsp == 1) {
 285
 286      } else {
 287        goto while_3_break;
 288      }
 289      m_run_st = 2;
 290      m_run_pc = 3;
 291      req_t_type = req_type;
 292      req_t_a = req_a;
 293      req_t_d = req_d;
 294      rsp_t_type = rsp_type;
 295      rsp_t_status = rsp_status;
 296      rsp_t_d = rsp_d;
 297      d_t = d;
 298      a_t = a;
 299
 300      goto return_label;
 301      L_MASTER_RUN_GET: 
 302      req_type = req_t_type;
 303      req_a = req_t_a;
 304      req_d = req_t_d;
 305      rsp_type = rsp_t_type;
 306      rsp_status = rsp_t_status;
 307      rsp_d = rsp_t_d;
 308      d = d_t;
 309      a = a_t;
 310    }
 311    while_3_break: /* CIL Label */ ;
 312    }
 313    rsp_type = c_rsp_type;
 314    rsp_status = c_rsp_status;
 315    rsp_d = c_rsp_d;
 316    c_empty_rsp = 1;
 317    c_read_rsp_ev = 1;
 318    if ((int )m_run_pc == 1) {
 319      if ((int )c_m_ev == 1) {
 320        m_run_st = 0;
 321      } else {
 322        goto _L___9;
 323      }
 324    } else {
 325      _L___9: /* CIL Label */ 
 326      if ((int )m_run_pc == 2) {
 327        if ((int )c_read_req_ev == 1) {
 328          m_run_st = 0;
 329        } else {
 330          goto _L___8;
 331        }
 332      } else {
 333        _L___8: /* CIL Label */ 
 334        if ((int )m_run_pc == 3) {
 335          if ((int )c_write_rsp_ev == 1) {
 336            m_run_st = 0;
 337          } else {
 338            goto _L___7;
 339          }
 340        } else {
 341          _L___7: /* CIL Label */ 
 342          if ((int )m_run_pc == 4) {
 343            if ((int )c_m_ev == 1) {
 344              m_run_st = 0;
 345            } else {
 346              goto _L___6;
 347            }
 348          } else {
 349            _L___6: /* CIL Label */ 
 350            if ((int )m_run_pc == 5) {
 351              if ((int )c_read_req_ev == 1) {
 352                m_run_st = 0;
 353              } else {
 354                goto _L___5;
 355              }
 356            } else {
 357              _L___5: /* CIL Label */ 
 358              if ((int )m_run_pc == 6) {
 359                if ((int )c_write_rsp_ev == 1) {
 360                  m_run_st = 0;
 361                } else {
 362
 363                }
 364              } else {
 365
 366              }
 367            }
 368          }
 369        }
 370      }
 371    }
 372    if ((int )s_run_pc == 2) {
 373      if ((int )c_write_req_ev == 1) {
 374        s_run_st = 0;
 375      } else {
 376        goto _L___10;
 377      }
 378    } else {
 379      _L___10: /* CIL Label */ 
 380      if ((int )s_run_pc == 1) {
 381        if ((int )c_read_rsp_ev == 1) {
 382          s_run_st = 0;
 383        } else {
 384
 385        }
 386      } else {
 387
 388      }
 389    }
 390    c_read_rsp_ev = 2;
 391    if (c_m_lock == 0) {
 392      {
 393      error();
 394      }
 395    } else {
 396
 397    }
 398    c_m_lock = 0;
 399    c_m_ev = 1;
 400    if ((int )m_run_pc == 1) {
 401      if ((int )c_m_ev == 1) {
 402        m_run_st = 0;
 403      } else {
 404        goto _L___15;
 405      }
 406    } else {
 407      _L___15: /* CIL Label */ 
 408      if ((int )m_run_pc == 2) {
 409        if ((int )c_read_req_ev == 1) {
 410          m_run_st = 0;
 411        } else {
 412          goto _L___14;
 413        }
 414      } else {
 415        _L___14: /* CIL Label */ 
 416        if ((int )m_run_pc == 3) {
 417          if ((int )c_write_rsp_ev == 1) {
 418            m_run_st = 0;
 419          } else {
 420            goto _L___13;
 421          }
 422        } else {
 423          _L___13: /* CIL Label */ 
 424          if ((int )m_run_pc == 4) {
 425            if ((int )c_m_ev == 1) {
 426              m_run_st = 0;
 427            } else {
 428              goto _L___12;
 429            }
 430          } else {
 431            _L___12: /* CIL Label */ 
 432            if ((int )m_run_pc == 5) {
 433              if ((int )c_read_req_ev == 1) {
 434                m_run_st = 0;
 435              } else {
 436                goto _L___11;
 437              }
 438            } else {
 439              _L___11: /* CIL Label */ 
 440              if ((int )m_run_pc == 6) {
 441                if ((int )c_write_rsp_ev == 1) {
 442                  m_run_st = 0;
 443                } else {
 444
 445                }
 446              } else {
 447
 448              }
 449            }
 450          }
 451        }
 452      }
 453    }
 454    if ((int )s_run_pc == 2) {
 455      if ((int )c_write_req_ev == 1) {
 456        s_run_st = 0;
 457      } else {
 458        goto _L___16;
 459      }
 460    } else {
 461      _L___16: /* CIL Label */ 
 462      if ((int )s_run_pc == 1) {
 463        if ((int )c_read_rsp_ev == 1) {
 464          s_run_st = 0;
 465        } else {
 466
 467        }
 468      } else {
 469
 470      }
 471    }
 472    c_m_ev = 2;
 473    a += 1;
 474  }
 475  while_0_break: /* CIL Label */ ;
 476  }
 477  a = 0;
 478  {
 479  while (1) {
 480    while_4_continue: /* CIL Label */ ;
 481    if (a < 2) {
 482
 483    } else {
 484      goto while_4_break;
 485    }
 486    req_type___0 = 0;
 487    req_a___0 = a;
 488    {
 489    while (1) {
 490      while_5_continue: /* CIL Label */ ;
 491      if (c_m_lock == 1) {
 492
 493      } else {
 494        goto while_5_break;
 495      }
 496      m_run_st = 2;
 497      m_run_pc = 4;
 498      req_tt_type = req_type___0;
 499      req_tt_a = req_a___0;
 500      req_tt_d = req_d___0;
 501      rsp_tt_type = rsp_type___0;
 502      rsp_tt_status = rsp_status___0;
 503      rsp_tt_d = rsp_d___0;
 504      d_t = d;
 505      a_t = a;
 506
 507      goto return_label;
 508      L_MASTER_RUN_MUTEX2: 
 509      req_type___0 = req_tt_type;
 510      req_a___0 = req_tt_a;
 511      req_d___0 = req_tt_d;
 512      rsp_type___0 = rsp_tt_type;
 513      rsp_status___0 = rsp_tt_status;
 514      rsp_d___0 = rsp_tt_d;
 515      d = d_t;
 516      a = a_t;
 517    }
 518    while_5_break: /* CIL Label */ ;
 519    }
 520    c_m_lock = 1;
 521    {
 522    while (1) {
 523      while_6_continue: /* CIL Label */ ;
 524      if ((int )c_empty_req == 0) {
 525
 526      } else {
 527        goto while_6_break;
 528      }
 529      m_run_st = 2;
 530      m_run_pc = 5;
 531      req_tt_type = req_type___0;
 532      req_tt_a = req_a___0;
 533      req_tt_d = req_d___0;
 534      rsp_tt_type = rsp_type___0;
 535      rsp_tt_status = rsp_status___0;
 536      rsp_tt_d = rsp_d___0;
 537      d_t = d;
 538      a_t = a;
 539
 540      goto return_label;
 541      L_MASTER_RUN_PUT2: 
 542      req_type___0 = req_tt_type;
 543      req_a___0 = req_tt_a;
 544      req_d___0 = req_tt_d;
 545      rsp_type___0 = rsp_tt_type;
 546      rsp_status___0 = rsp_tt_status;
 547      rsp_d___0 = rsp_tt_d;
 548      d = d_t;
 549      a = a_t;
 550    }
 551    while_6_break: /* CIL Label */ ;
 552    }
 553    c_req_type = req_type___0;
 554    c_req_a = req_a___0;
 555    c_req_d = req_d___0;
 556    c_empty_req = 0;
 557    c_write_req_ev = 1;
 558    if ((int )m_run_pc == 1) {
 559      if ((int )c_m_ev == 1) {
 560        m_run_st = 0;
 561      } else {
 562        goto _L___21;
 563      }
 564    } else {
 565      _L___21: /* CIL Label */ 
 566      if ((int )m_run_pc == 2) {
 567        if ((int )c_read_req_ev == 1) {
 568          m_run_st = 0;
 569        } else {
 570          goto _L___20;
 571        }
 572      } else {
 573        _L___20: /* CIL Label */ 
 574        if ((int )m_run_pc == 3) {
 575          if ((int )c_write_rsp_ev == 1) {
 576            m_run_st = 0;
 577          } else {
 578            goto _L___19;
 579          }
 580        } else {
 581          _L___19: /* CIL Label */ 
 582          if ((int )m_run_pc == 4) {
 583            if ((int )c_m_ev == 1) {
 584              m_run_st = 0;
 585            } else {
 586              goto _L___18;
 587            }
 588          } else {
 589            _L___18: /* CIL Label */ 
 590            if ((int )m_run_pc == 5) {
 591              if ((int )c_read_req_ev == 1) {
 592                m_run_st = 0;
 593              } else {
 594                goto _L___17;
 595              }
 596            } else {
 597              _L___17: /* CIL Label */ 
 598              if ((int )m_run_pc == 6) {
 599                if ((int )c_write_rsp_ev == 1) {
 600                  m_run_st = 0;
 601                } else {
 602
 603                }
 604              } else {
 605
 606              }
 607            }
 608          }
 609        }
 610      }
 611    }
 612    if ((int )s_run_pc == 2) {
 613      if ((int )c_write_req_ev == 1) {
 614        s_run_st = 0;
 615      } else {
 616        goto _L___22;
 617      }
 618    } else {
 619      _L___22: /* CIL Label */ 
 620      if ((int )s_run_pc == 1) {
 621        if ((int )c_read_rsp_ev == 1) {
 622          s_run_st = 0;
 623        } else {
 624
 625        }
 626      } else {
 627
 628      }
 629    }
 630    c_write_req_ev = 2;
 631    {
 632    while (1) {
 633      while_7_continue: /* CIL Label */ ;
 634      if ((int )c_empty_rsp == 1) {
 635
 636      } else {
 637        goto while_7_break;
 638      }
 639      m_run_st = 2;
 640      m_run_pc = 6;
 641      req_tt_type = req_type___0;
 642      req_tt_a = req_a___0;
 643      req_tt_d = req_d___0;
 644      rsp_tt_type = rsp_type___0;
 645      rsp_tt_status = rsp_status___0;
 646      rsp_tt_d = rsp_d___0;
 647      d_t = d;
 648      a_t = a;
 649
 650      goto return_label;
 651      L_MASTER_RUN_GET2: 
 652      req_type___0 = req_tt_type;
 653      req_a___0 = req_tt_a;
 654      req_d___0 = req_tt_d;
 655      rsp_type___0 = rsp_tt_type;
 656      rsp_status___0 = rsp_tt_status;
 657      rsp_d___0 = rsp_tt_d;
 658      d = d_t;
 659      a = a_t;
 660    }
 661    while_7_break: /* CIL Label */ ;
 662    }
 663    rsp_type___0 = c_rsp_type;
 664    rsp_status___0 = c_rsp_status;
 665    rsp_d___0 = c_rsp_d;
 666    c_empty_rsp = 1;
 667    c_read_rsp_ev = 1;
 668    if ((int )m_run_pc == 1) {
 669      if ((int )c_m_ev == 1) {
 670        m_run_st = 0;
 671      } else {
 672        goto _L___27;
 673      }
 674    } else {
 675      _L___27: /* CIL Label */ 
 676      if ((int )m_run_pc == 2) {
 677        if ((int )c_read_req_ev == 1) {
 678          m_run_st = 0;
 679        } else {
 680          goto _L___26;
 681        }
 682      } else {
 683        _L___26: /* CIL Label */ 
 684        if ((int )m_run_pc == 3) {
 685          if ((int )c_write_rsp_ev == 1) {
 686            m_run_st = 0;
 687          } else {
 688            goto _L___25;
 689          }
 690        } else {
 691          _L___25: /* CIL Label */ 
 692          if ((int )m_run_pc == 4) {
 693            if ((int )c_m_ev == 1) {
 694              m_run_st = 0;
 695            } else {
 696              goto _L___24;
 697            }
 698          } else {
 699            _L___24: /* CIL Label */ 
 700            if ((int )m_run_pc == 5) {
 701              if ((int )c_read_req_ev == 1) {
 702                m_run_st = 0;
 703              } else {
 704                goto _L___23;
 705              }
 706            } else {
 707              _L___23: /* CIL Label */ 
 708              if ((int )m_run_pc == 6) {
 709                if ((int )c_write_rsp_ev == 1) {
 710                  m_run_st = 0;
 711                } else {
 712
 713                }
 714              } else {
 715
 716              }
 717            }
 718          }
 719        }
 720      }
 721    }
 722    if ((int )s_run_pc == 2) {
 723      if ((int )c_write_req_ev == 1) {
 724        s_run_st = 0;
 725      } else {
 726        goto _L___28;
 727      }
 728    } else {
 729      _L___28: /* CIL Label */ 
 730      if ((int )s_run_pc == 1) {
 731        if ((int )c_read_rsp_ev == 1) {
 732          s_run_st = 0;
 733        } else {
 734
 735        }
 736      } else {
 737
 738      }
 739    }
 740    c_read_rsp_ev = 2;
 741    if (c_m_lock == 0) {
 742      {
 743      error();
 744      }
 745    } else {
 746
 747    }
 748    c_m_lock = 0;
 749    c_m_ev = 1;
 750    if ((int )m_run_pc == 1) {
 751      if ((int )c_m_ev == 1) {
 752        m_run_st = 0;
 753      } else {
 754        goto _L___33;
 755      }
 756    } else {
 757      _L___33: /* CIL Label */ 
 758      if ((int )m_run_pc == 2) {
 759        if ((int )c_read_req_ev == 1) {
 760          m_run_st = 0;
 761        } else {
 762          goto _L___32;
 763        }
 764      } else {
 765        _L___32: /* CIL Label */ 
 766        if ((int )m_run_pc == 3) {
 767          if ((int )c_write_rsp_ev == 1) {
 768            m_run_st = 0;
 769          } else {
 770            goto _L___31;
 771          }
 772        } else {
 773          _L___31: /* CIL Label */ 
 774          if ((int )m_run_pc == 4) {
 775            if ((int )c_m_ev == 1) {
 776              m_run_st = 0;
 777            } else {
 778              goto _L___30;
 779            }
 780          } else {
 781            _L___30: /* CIL Label */ 
 782            if ((int )m_run_pc == 5) {
 783              if ((int )c_read_req_ev == 1) {
 784                m_run_st = 0;
 785              } else {
 786                goto _L___29;
 787              }
 788            } else {
 789              _L___29: /* CIL Label */ 
 790              if ((int )m_run_pc == 6) {
 791                if ((int )c_write_rsp_ev == 1) {
 792                  m_run_st = 0;
 793                } else {
 794
 795                }
 796              } else {
 797
 798              }
 799            }
 800          }
 801        }
 802      }
 803    }
 804    if ((int )s_run_pc == 2) {
 805      if ((int )c_write_req_ev == 1) {
 806        s_run_st = 0;
 807      } else {
 808        goto _L___34;
 809      }
 810    } else {
 811      _L___34: /* CIL Label */ 
 812      if ((int )s_run_pc == 1) {
 813        if ((int )c_read_rsp_ev == 1) {
 814          s_run_st = 0;
 815        } else {
 816
 817        }
 818      } else {
 819
 820      }
 821    }
 822    c_m_ev = 2;
 823    if (! (req_a___0 + 50 == rsp_d___0)) {
 824      {
 825      error();
 826      }
 827    } else {
 828
 829    }
 830    a += 1;
 831  }
 832  while_4_break: /* CIL Label */ ;
 833  }
 834
 835  return_label: /* CIL Label */ 
 836  return;
 837}
 838}
 839static int req_t_type___0  ;
 840static int req_t_a___0  ;
 841static int req_t_d___0  ;
 842static int rsp_t_type___0  ;
 843static int rsp_t_status___0  ;
 844static int rsp_t_d___0  ;
 845void s_run(void) 
 846{ int req_type ;
 847  int req_a ;
 848  int req_d ;
 849  int rsp_type ;
 850  int rsp_status ;
 851  int rsp_d ;
 852  int dummy ;
 853
 854  {
 855  if ((int )s_run_pc == 0) {
 856    goto L_SLAVE_RUN_ENTRY;
 857  } else {
 858    if ((int )s_run_pc == 1) {
 859      goto L_SLAVE_RUN_PUT;
 860    } else {
 861      if ((int )s_run_pc == 2) {
 862        goto L_SLAVE_RUN_GET;
 863      } else {
 864
 865      }
 866    }
 867  }
 868  L_SLAVE_RUN_ENTRY: 
 869  {
 870  while (1) {
 871    while_8_continue: /* CIL Label */ ;
 872    {
 873    while (1) {
 874      while_9_continue: /* CIL Label */ ;
 875      if ((int )c_empty_req == 1) {
 876
 877      } else {
 878        goto while_9_break;
 879      }
 880      s_run_st = 2;
 881      s_run_pc = 2;
 882      req_t_type___0 = req_type;
 883      req_t_a___0 = req_a;
 884      req_t_d___0 = req_d;
 885      rsp_t_type___0 = rsp_type;
 886      rsp_t_status___0 = rsp_status;
 887      rsp_t_d___0 = rsp_d;
 888
 889      goto return_label;
 890      L_SLAVE_RUN_GET: 
 891      req_type = req_t_type___0;
 892      req_a = req_t_a___0;
 893      req_d = req_t_d___0;
 894      rsp_type = rsp_t_type___0;
 895      rsp_status = rsp_t_status___0;
 896      rsp_d = rsp_t_d___0;
 897    }
 898    while_9_break: /* CIL Label */ ;
 899    }
 900    req_type = c_req_type;
 901    req_a = c_req_a;
 902    req_d = c_req_d;
 903    c_empty_req = 1;
 904    c_read_req_ev = 1;
 905    if ((int )m_run_pc == 1) {
 906      if ((int )c_m_ev == 1) {
 907        m_run_st = 0;
 908      } else {
 909        goto _L___3;
 910      }
 911    } else {
 912      _L___3: /* CIL Label */ 
 913      if ((int )m_run_pc == 2) {
 914        if ((int )c_read_req_ev == 1) {
 915          m_run_st = 0;
 916        } else {
 917          goto _L___2;
 918        }
 919      } else {
 920        _L___2: /* CIL Label */ 
 921        if ((int )m_run_pc == 3) {
 922          if ((int )c_write_rsp_ev == 1) {
 923            m_run_st = 0;
 924          } else {
 925            goto _L___1;
 926          }
 927        } else {
 928          _L___1: /* CIL Label */ 
 929          if ((int )m_run_pc == 4) {
 930            if ((int )c_m_ev == 1) {
 931              m_run_st = 0;
 932            } else {
 933              goto _L___0;
 934            }
 935          } else {
 936            _L___0: /* CIL Label */ 
 937            if ((int )m_run_pc == 5) {
 938              if ((int )c_read_req_ev == 1) {
 939                m_run_st = 0;
 940              } else {
 941                goto _L;
 942              }
 943            } else {
 944              _L: /* CIL Label */ 
 945              if ((int )m_run_pc == 6) {
 946                if ((int )c_write_rsp_ev == 1) {
 947                  m_run_st = 0;
 948                } else {
 949
 950                }
 951              } else {
 952
 953              }
 954            }
 955          }
 956        }
 957      }
 958    }
 959    if ((int )s_run_pc == 2) {
 960      if ((int )c_write_req_ev == 1) {
 961        s_run_st = 0;
 962      } else {
 963        goto _L___4;
 964      }
 965    } else {
 966      _L___4: /* CIL Label */ 
 967      if ((int )s_run_pc == 1) {
 968        if ((int )c_read_rsp_ev == 1) {
 969          s_run_st = 0;
 970        } else {
 971
 972        }
 973      } else {
 974
 975      }
 976    }
 977    c_read_req_ev = 2;
 978    rsp_type = req_type;
 979    if ((int )req_type == 0) {
 980
 981      rsp_d = s_memory_read(req_a);
 982
 983      rsp_status = 1;
 984    } else {
 985      if ((int )req_type == 1) {
 986
 987        s_memory_write(req_a,req_d);
 988
 989        rsp_status = 1;
 990      } else {
 991        rsp_status = 0;
 992      }
 993    }
 994    {
 995    while (1) {
 996      while_10_continue: /* CIL Label */ ;
 997      if ((int )c_empty_rsp == 0) {
 998
 999      } else {
1000        goto while_10_break;
1001      }
1002      s_run_st = 2;
1003      s_run_pc = 1;
1004      req_t_type___0 = req_type;
1005      req_t_a___0 = req_a;
1006      req_t_d___0 = req_d;
1007      rsp_t_type___0 = rsp_type;
1008      rsp_t_status___0 = rsp_status;
1009      rsp_t_d___0 = rsp_d;
1010
1011      goto return_label;
1012      L_SLAVE_RUN_PUT: 
1013      req_type = req_t_type___0;
1014      req_a = req_t_a___0;
1015      req_d = req_t_d___0;
1016      rsp_type = rsp_t_type___0;
1017      rsp_status = rsp_t_status___0;
1018      rsp_d = rsp_t_d___0;
1019    }
1020    while_10_break: /* CIL Label */ ;
1021    }
1022    c_rsp_type = rsp_type;
1023    c_rsp_status = rsp_status;
1024    c_rsp_d = rsp_d;
1025    c_empty_rsp = 0;
1026    c_write_rsp_ev = 1;
1027    if ((int )m_run_pc == 1) {
1028      if ((int )c_m_ev == 1) {
1029        m_run_st = 0;
1030      } else {
1031        goto _L___9;
1032      }
1033    } else {
1034      _L___9: /* CIL Label */ 
1035      if ((int )m_run_pc == 2) {
1036        if ((int )c_read_req_ev == 1) {
1037          m_run_st = 0;
1038        } else {
1039          goto _L___8;
1040        }
1041      } else {
1042        _L___8: /* CIL Label */ 
1043        if ((int )m_run_pc == 3) {
1044          if ((int )c_write_rsp_ev == 1) {
1045            m_run_st = 0;
1046          } else {
1047            goto _L___7;
1048          }
1049        } else {
1050          _L___7: /* CIL Label */ 
1051          if ((int )m_run_pc == 4) {
1052            if ((int )c_m_ev == 1) {
1053              m_run_st = 0;
1054            } else {
1055              goto _L___6;
1056            }
1057          } else {
1058            _L___6: /* CIL Label */ 
1059            if ((int )m_run_pc == 5) {
1060              if ((int )c_read_req_ev == 1) {
1061                m_run_st = 0;
1062              } else {
1063                goto _L___5;
1064              }
1065            } else {
1066              _L___5: /* CIL Label */ 
1067              if ((int )m_run_pc == 6) {
1068                if ((int )c_write_rsp_ev == 1) {
1069                  m_run_st = 0;
1070                } else {
1071
1072                }
1073              } else {
1074
1075              }
1076            }
1077          }
1078        }
1079      }
1080    }
1081    if ((int )s_run_pc == 2) {
1082      if ((int )c_write_req_ev == 1) {
1083        s_run_st = 0;
1084      } else {
1085        goto _L___10;
1086      }
1087    } else {
1088      _L___10: /* CIL Label */ 
1089      if ((int )s_run_pc == 1) {
1090        if ((int )c_read_rsp_ev == 1) {
1091          s_run_st = 0;
1092        } else {
1093
1094        }
1095      } else {
1096
1097      }
1098    }
1099    c_write_rsp_ev = 2;
1100  }
1101  while_8_break: /* CIL Label */ ;
1102  }
1103  return_label: /* CIL Label */ 
1104  return;
1105}
1106}
1107void eval(void) 
1108{ int tmp ;
1109  int tmp___0 ;
1110
1111  {
1112  {
1113  while (1) {
1114    while_11_continue: /* CIL Label */ ;
1115    if ((int )m_run_st == 0) {
1116
1117    } else {
1118      if ((int )s_run_st == 0) {
1119
1120      } else {
1121        goto while_11_break;
1122      }
1123    }
1124    if ((int )m_run_st == 0) {
1125      {
1126        tmp = __VERIFIER_nondet_int();
1127      }
1128      if (tmp) {
1129        {
1130        m_run_st = 1;
1131        m_run();
1132        }
1133      } else {
1134
1135      }
1136    } else {
1137
1138    }
1139    if ((int )s_run_st == 0) {
1140      {
1141        tmp___0 = __VERIFIER_nondet_int();
1142      }
1143      if (tmp___0) {
1144        {
1145        s_run_st = 1;
1146        s_run();
1147        }
1148      } else {
1149
1150      }
1151    } else {
1152
1153    }
1154  }
1155  while_11_break: /* CIL Label */ ;
1156  }
1157
1158  return;
1159}
1160}
1161void start_simulation(void) 
1162{ int kernel_st ;
1163
1164  {
1165  kernel_st = 0;
1166  if ((int )m_run_i == 1) {
1167    m_run_st = 0;
1168  } else {
1169    m_run_st = 2;
1170  }
1171  if ((int )s_run_i == 1) {
1172    s_run_st = 0;
1173  } else {
1174    s_run_st = 2;
1175  }
1176  if ((int )m_run_pc == 1) {
1177    if ((int )c_m_ev == 1) {
1178      m_run_st = 0;
1179    } else {
1180      goto _L___3;
1181    }
1182  } else {
1183    _L___3: /* CIL Label */ 
1184    if ((int )m_run_pc == 2) {
1185      if ((int )c_read_req_ev == 1) {
1186        m_run_st = 0;
1187      } else {
1188        goto _L___2;
1189      }
1190    } else {
1191      _L___2: /* CIL Label */ 
1192      if ((int )m_run_pc == 3) {
1193        if ((int )c_write_rsp_ev == 1) {
1194          m_run_st = 0;
1195        } else {
1196          goto _L___1;
1197        }
1198      } else {
1199        _L___1: /* CIL Label */ 
1200        if ((int )m_run_pc == 4) {
1201          if ((int )c_m_ev == 1) {
1202            m_run_st = 0;
1203          } else {
1204            goto _L___0;
1205          }
1206        } else {
1207          _L___0: /* CIL Label */ 
1208          if ((int )m_run_pc == 5) {
1209            if ((int )c_read_req_ev == 1) {
1210              m_run_st = 0;
1211            } else {
1212              goto _L;
1213            }
1214          } else {
1215            _L: /* CIL Label */ 
1216            if ((int )m_run_pc == 6) {
1217              if ((int )c_write_rsp_ev == 1) {
1218                m_run_st = 0;
1219              } else {
1220
1221              }
1222            } else {
1223
1224            }
1225          }
1226        }
1227      }
1228    }
1229  }
1230  if ((int )s_run_pc == 2) {
1231    if ((int )c_write_req_ev == 1) {
1232      s_run_st = 0;
1233    } else {
1234      goto _L___4;
1235    }
1236  } else {
1237    _L___4: /* CIL Label */ 
1238    if ((int )s_run_pc == 1) {
1239      if ((int )c_read_rsp_ev == 1) {
1240        s_run_st = 0;
1241      } else {
1242
1243      }
1244    } else {
1245
1246    }
1247  }
1248  {
1249  while (1) {
1250    while_12_continue: /* CIL Label */ ;
1251    {
1252    kernel_st = 1;
1253    eval();
1254    }
1255    kernel_st = 2;
1256    kernel_st = 3;
1257    if ((int )m_run_pc == 1) {
1258      if ((int )c_m_ev == 1) {
1259        m_run_st = 0;
1260      } else {
1261        goto _L___9;
1262      }
1263    } else {
1264      _L___9: /* CIL Label */ 
1265      if ((int )m_run_pc == 2) {
1266        if ((int )c_read_req_ev == 1) {
1267          m_run_st = 0;
1268        } else {
1269          goto _L___8;
1270        }
1271      } else {
1272        _L___8: /* CIL Label */ 
1273        if ((int )m_run_pc == 3) {
1274          if ((int )c_write_rsp_ev == 1) {
1275            m_run_st = 0;
1276          } else {
1277            goto _L___7;
1278          }
1279        } else {
1280          _L___7: /* CIL Label */ 
1281          if ((int )m_run_pc == 4) {
1282            if ((int )c_m_ev == 1) {
1283              m_run_st = 0;
1284            } else {
1285              goto _L___6;
1286            }
1287          } else {
1288            _L___6: /* CIL Label */ 
1289            if ((int )m_run_pc == 5) {
1290              if ((int )c_read_req_ev == 1) {
1291                m_run_st = 0;
1292              } else {
1293                goto _L___5;
1294              }
1295            } else {
1296              _L___5: /* CIL Label */ 
1297              if ((int )m_run_pc == 6) {
1298                if ((int )c_write_rsp_ev == 1) {
1299                  m_run_st = 0;
1300                } else {
1301
1302                }
1303              } else {
1304
1305              }
1306            }
1307          }
1308        }
1309      }
1310    }
1311    if ((int )s_run_pc == 2) {
1312      if ((int )c_write_req_ev == 1) {
1313        s_run_st = 0;
1314      } else {
1315        goto _L___10;
1316      }
1317    } else {
1318      _L___10: /* CIL Label */ 
1319      if ((int )s_run_pc == 1) {
1320        if ((int )c_read_rsp_ev == 1) {
1321          s_run_st = 0;
1322        } else {
1323
1324        }
1325      } else {
1326
1327      }
1328    }
1329    if ((int )m_run_st == 0) {
1330
1331    } else {
1332      if ((int )s_run_st == 0) {
1333
1334      } else {
1335        goto while_12_break;
1336      }
1337    }
1338  }
1339  while_12_break: /* CIL Label */ ;
1340  }
1341
1342  return;
1343}
1344}
1345int main(void) 
1346{ int __retres1 ;
1347
1348  {
1349  {
1350 c_m_lock  =    0;
1351 c_m_ev  =    2;
1352
1353  m_run_i = 1;
1354  m_run_pc = 0;
1355  s_run_i = 1;
1356  s_run_pc = 0;
1357  c_empty_req = 1;
1358  c_empty_rsp = 1;
1359  c_read_req_ev = 2;
1360  c_write_req_ev = 2;
1361  c_read_rsp_ev = 2;
1362  c_write_rsp_ev = 2;
1363  c_m_lock = 0;
1364  c_m_ev = 2;
1365  start_simulation();
1366  }
1367  __retres1 = 0;
1368  return (__retres1);
1369}
1370}
↑