Showing error 230

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