Showing error 2282

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