Showing error 231

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