Showing error 2284

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