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