Showing error 2283

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