Showing error 232

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