Showing error 229

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.1.cil.c
Line in file: 15
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

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