User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | systemc/token_ring.02_unsafe.cil.c |
Line in file: | 8 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1/* Generated by CIL v. 1.3.6 */ 2/* print_CIL_Input is true */ 3 4void error(void) 5{ 6 7 { 8 ERROR: ; 9 goto ERROR; 10 return; 11} 12} 13int m_pc = 0; 14int t1_pc = 0; 15int t2_pc = 0; 16int m_st ; 17int t1_st ; 18int t2_st ; 19int m_i ; 20int t1_i ; 21int t2_i ; 22int M_E = 2; 23int T1_E = 2; 24int T2_E = 2; 25int E_M = 2; 26int E_1 = 2; 27int E_2 = 2; 28int is_master_triggered(void) ; 29int is_transmit1_triggered(void) ; 30int is_transmit2_triggered(void) ; 31void immediate_notify(void) ; 32int token ; 33int __VERIFIER_nondet_int() ; 34int local ; 35void master(void) 36{ 37int tmp_var ; 38 { 39 if (m_pc == 0) { 40 goto M_ENTRY; 41 } else { 42 if (m_pc == 1) { 43 goto M_WAIT; 44 } else { 45 46 } 47 } 48 M_ENTRY: ; 49 { 50 while (1) { 51 while_0_continue: /* CIL Label */ ; 52 { 53 token = __VERIFIER_nondet_int(); 54 local = token; 55 E_1 = 1; 56 immediate_notify(); 57 E_1 = 2; 58 m_pc = 1; 59 m_st = 2; 60 } 61 62 goto return_label; 63 M_WAIT: ; 64 if (token != local + 2) { 65 { 66 error(); 67 } 68 } else { 69 if(tmp_var <= 5){ 70 if(tmp_var >= 5){ 71 72 } 73 } 74 75 if(tmp_var <= 5){ 76 if(tmp_var >= 5){ 77 if(tmp_var == 5){ 78 error(); 79 } 80 } 81 } 82 } 83 } 84 while_0_break: /* CIL Label */ ; 85 } 86 87 return_label: /* CIL Label */ 88 return; 89} 90} 91void transmit1(void) 92{ 93 94 { 95 if (t1_pc == 0) { 96 goto T1_ENTRY; 97 } else { 98 if (t1_pc == 1) { 99 goto T1_WAIT; 100 } else { 101 102 } 103 } 104 T1_ENTRY: ; 105 { 106 while (1) { 107 while_1_continue: /* CIL Label */ ; 108 t1_pc = 1; 109 t1_st = 2; 110 111 goto return_label; 112 T1_WAIT: 113 { 114 token += 1; 115 E_2 = 1; 116 immediate_notify(); 117 E_2 = 2; 118 } 119 } 120 while_1_break: /* CIL Label */ ; 121 } 122 123 return_label: /* CIL Label */ 124 return; 125} 126} 127void transmit2(void) 128{ 129 130 { 131 if (t2_pc == 0) { 132 goto T2_ENTRY; 133 } else { 134 if (t2_pc == 1) { 135 goto T2_WAIT; 136 } else { 137 138 } 139 } 140 T2_ENTRY: ; 141 { 142 while (1) { 143 while_2_continue: /* CIL Label */ ; 144 t2_pc = 1; 145 t2_st = 2; 146 147 goto return_label; 148 T2_WAIT: 149 { 150 token += 1; 151 E_M = 1; 152 immediate_notify(); 153 E_M = 2; 154 } 155 } 156 while_2_break: /* CIL Label */ ; 157 } 158 159 return_label: /* CIL Label */ 160 return; 161} 162} 163int is_master_triggered(void) 164{ int __retres1 ; 165 166 { 167 if (m_pc == 1) { 168 if (E_M == 1) { 169 __retres1 = 1; 170 goto return_label; 171 } else { 172 173 } 174 } else { 175 176 } 177 __retres1 = 0; 178 return_label: /* CIL Label */ 179 return (__retres1); 180} 181} 182int is_transmit1_triggered(void) 183{ int __retres1 ; 184 185 { 186 if (t1_pc == 1) { 187 if (E_1 == 1) { 188 __retres1 = 1; 189 goto return_label; 190 } else { 191 192 } 193 } else { 194 195 } 196 __retres1 = 0; 197 return_label: /* CIL Label */ 198 return (__retres1); 199} 200} 201int is_transmit2_triggered(void) 202{ int __retres1 ; 203 204 { 205 if (t2_pc == 1) { 206 if (E_2 == 1) { 207 __retres1 = 1; 208 goto return_label; 209 } else { 210 211 } 212 } else { 213 214 } 215 __retres1 = 0; 216 return_label: /* CIL Label */ 217 return (__retres1); 218} 219} 220void update_channels(void) 221{ 222 223 { 224 225 return; 226} 227} 228void init_threads(void) 229{ 230 231 { 232 if (m_i == 1) { 233 m_st = 0; 234 } else { 235 m_st = 2; 236 } 237 if (t1_i == 1) { 238 t1_st = 0; 239 } else { 240 t1_st = 2; 241 } 242 if (t2_i == 1) { 243 t2_st = 0; 244 } else { 245 t2_st = 2; 246 } 247 248 return; 249} 250} 251int exists_runnable_thread(void) 252{ int __retres1 ; 253 254 { 255 if (m_st == 0) { 256 __retres1 = 1; 257 goto return_label; 258 } else { 259 if (t1_st == 0) { 260 __retres1 = 1; 261 goto return_label; 262 } else { 263 if (t2_st == 0) { 264 __retres1 = 1; 265 goto return_label; 266 } else { 267 268 } 269 } 270 } 271 __retres1 = 0; 272 return_label: /* CIL Label */ 273 return (__retres1); 274} 275} 276void eval(void) 277{ 278 int tmp ; 279 280 { 281 { 282 while (1) { 283 while_3_continue: /* CIL Label */ ; 284 { 285 tmp = exists_runnable_thread(); 286 } 287 if (tmp) { 288 289 } else { 290 goto while_3_break; 291 } 292 if (m_st == 0) { 293 int tmp_ndt_1; 294 tmp_ndt_1 = __VERIFIER_nondet_int(); 295 if (tmp_ndt_1) { 296 { 297 m_st = 1; 298 master(); 299 } 300 } else { 301 302 } 303 } else { 304 305 } 306 if (t1_st == 0) { 307 int tmp_ndt_2; 308 tmp_ndt_2 = __VERIFIER_nondet_int(); 309 if (tmp_ndt_2) { 310 { 311 t1_st = 1; 312 transmit1(); 313 } 314 } else { 315 316 } 317 } else { 318 319 } 320 if (t2_st == 0) { 321 int tmp_ndt_3; 322 tmp_ndt_3 = __VERIFIER_nondet_int(); 323 if (tmp_ndt_3) { 324 { 325 t2_st = 1; 326 transmit2(); 327 } 328 } else { 329 330 } 331 } else { 332 333 } 334 } 335 while_3_break: /* CIL Label */ ; 336 } 337 338 return; 339} 340} 341void fire_delta_events(void) 342{ 343 344 { 345 if (M_E == 0) { 346 M_E = 1; 347 } else { 348 349 } 350 if (T1_E == 0) { 351 T1_E = 1; 352 } else { 353 354 } 355 if (T2_E == 0) { 356 T2_E = 1; 357 } else { 358 359 } 360 if (E_M == 0) { 361 E_M = 1; 362 } else { 363 364 } 365 if (E_1 == 0) { 366 E_1 = 1; 367 } else { 368 369 } 370 if (E_2 == 0) { 371 E_2 = 1; 372 } else { 373 374 } 375 376 return; 377} 378} 379void reset_delta_events(void) 380{ 381 382 { 383 if (M_E == 1) { 384 M_E = 2; 385 } else { 386 387 } 388 if (T1_E == 1) { 389 T1_E = 2; 390 } else { 391 392 } 393 if (T2_E == 1) { 394 T2_E = 2; 395 } else { 396 397 } 398 if (E_M == 1) { 399 E_M = 2; 400 } else { 401 402 } 403 if (E_1 == 1) { 404 E_1 = 2; 405 } else { 406 407 } 408 if (E_2 == 1) { 409 E_2 = 2; 410 } else { 411 412 } 413 414 return; 415} 416} 417void activate_threads(void) 418{ int tmp ; 419 int tmp___0 ; 420 int tmp___1 ; 421 422 { 423 { 424 tmp = is_master_triggered(); 425 } 426 if (tmp) { 427 m_st = 0; 428 } else { 429 430 } 431 { 432 tmp___0 = is_transmit1_triggered(); 433 } 434 if (tmp___0) { 435 t1_st = 0; 436 } else { 437 438 } 439 { 440 tmp___1 = is_transmit2_triggered(); 441 } 442 if (tmp___1) { 443 t2_st = 0; 444 } else { 445 446 } 447 448 return; 449} 450} 451void immediate_notify(void) 452{ 453 454 { 455 { 456 activate_threads(); 457 } 458 459 return; 460} 461} 462void fire_time_events(void) 463{ 464 465 { 466 M_E = 1; 467 468 return; 469} 470} 471void reset_time_events(void) 472{ 473 474 { 475 if (M_E == 1) { 476 M_E = 2; 477 } else { 478 479 } 480 if (T1_E == 1) { 481 T1_E = 2; 482 } else { 483 484 } 485 if (T2_E == 1) { 486 T2_E = 2; 487 } else { 488 489 } 490 if (E_M == 1) { 491 E_M = 2; 492 } else { 493 494 } 495 if (E_1 == 1) { 496 E_1 = 2; 497 } else { 498 499 } 500 if (E_2 == 1) { 501 E_2 = 2; 502 } else { 503 504 } 505 506 return; 507} 508} 509void init_model(void) 510{ 511 512 { 513 m_i = 1; 514 t1_i = 1; 515 t2_i = 1; 516 517 return; 518} 519} 520int stop_simulation(void) 521{ int tmp ; 522 int __retres2 ; 523 524 { 525 { 526 tmp = exists_runnable_thread(); 527 } 528 if (tmp) { 529 __retres2 = 0; 530 goto return_label; 531 } else { 532 533 } 534 __retres2 = 1; 535 return_label: /* CIL Label */ 536 return (__retres2); 537} 538} 539void start_simulation(void) 540{ int kernel_st ; 541 int tmp ; 542 int tmp___0 ; 543 544 { 545 { 546 kernel_st = 0; 547 update_channels(); 548 init_threads(); 549 fire_delta_events(); 550 activate_threads(); 551 reset_delta_events(); 552 } 553 { 554 while (1) { 555 while_4_continue: /* CIL Label */ ; 556 { 557 kernel_st = 1; 558 eval(); 559 } 560 { 561 kernel_st = 2; 562 update_channels(); 563 } 564 { 565 kernel_st = 3; 566 fire_delta_events(); 567 activate_threads(); 568 reset_delta_events(); 569 } 570 { 571 tmp = exists_runnable_thread(); 572 } 573 if (tmp == 0) { 574 { 575 kernel_st = 4; 576 fire_time_events(); 577 activate_threads(); 578 reset_time_events(); 579 } 580 } else { 581 582 } 583 { 584 tmp___0 = stop_simulation(); 585 } 586 if (tmp___0) { 587 goto while_4_break; 588 } else { 589 590 } 591 } 592 while_4_break: /* CIL Label */ ; 593 } 594 595 return; 596} 597} 598int main(void) 599{ int __retres1 ; 600 601 { 602 { 603 init_model(); 604 start_simulation(); 605 } 606 __retres1 = 0; 607 return (__retres1); 608} 609}