Showing error 233

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