Showing error 2280

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/mem_slave_tlm.1_safe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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