[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/transmitter.03_false.cil.c [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:01] setting up pass: functionmeta, options = [ 0:02] setting up pass: fuse-ctors, options = [ 0:02] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.8/_klee_out" [ 0:03] KLEE: Using Z3 solver backend [ 0:03] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:03] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf' [ 0:03] [ 0:03] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:06] KLEE: WARNING: undefined reference to function: klee_free [ 0:06] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:06] i:1 [ 0:06] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:06] about to __boot:0 [ 0:06] about to run the scheduler:0 [ 0:06] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:06] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:06] KLEE: NOTE: now ignoring this error at this location [ 0:06] KLEE: ERROR: EXITING ON ERROR: [ 0:06] Error: failed external call: __dios_tainted_init [ 0:06] File: /dios/libc/sys/start.cpp [ 0:06] Line: 87 [ 0:06] assembly.ll line: 35196 [ 0:06] Stack: [ 0:06] #000035196 in __dios_start (l=0, argc=1, argv=94836672344584, envp=94836672421896) at /dios/libc/sys/start.cpp:87 [ 0:06] #100011215 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:06] #200043546 in klee_boot (argc=2, argv=94836646803456) at /dios/arch/klee/boot.c:41 [ 0:06] [ 0:06] [ 0:06] 1 /* TAGS: error c sym */ [ 0:06] 2 /* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc */ [ 0:06] 3 extern void __VERIFIER_error() __attribute__ ((__noreturn__)); [ 0:06] 4 [ 0:06] 5 extern int __VERIFIER_nondet_int(); [ 0:06] 6 /* Generated by CIL v. 1.3.6 */ [ 0:06] 7 /* print_CIL_Input is true */ [ 0:06] 8 [ 0:06] 9 void error(void) [ 0:06] 10 { [ 0:06] 11 [ 0:06] 12 { [ 0:06] 13 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:06] 14 return; [ 0:06] 15 } [ 0:06] 16 } [ 0:06] 17 int m_pc = 0; [ 0:06] 18 int t1_pc = 0; [ 0:06] 19 int t2_pc = 0; [ 0:06] 20 int t3_pc = 0; [ 0:06] 21 int m_st ; [ 0:06] 22 int t1_st ; [ 0:06] 23 int t2_st ; [ 0:06] 24 int t3_st ; [ 0:06] 25 int m_i ; [ 0:06] 26 int t1_i ; [ 0:06] 27 int t2_i ; [ 0:06] 28 int t3_i ; [ 0:06] 29 int M_E = 2; [ 0:06] 30 int T1_E = 2; [ 0:06] 31 int T2_E = 2; [ 0:06] 32 int T3_E = 2; [ 0:06] 33 int E_1 = 2; [ 0:06] 34 int E_2 = 2; [ 0:06] 35 int E_3 = 2; [ 0:06] 36 int is_master_triggered(void) ; [ 0:06] 37 int is_transmit1_triggered(void) ; [ 0:06] 38 int is_transmit2_triggered(void) ; [ 0:06] 39 int is_transmit3_triggered(void) ; [ 0:06] 40 void immediate_notify(void) ; [ 0:06] 41 void master(void) [ 0:06] 42 { [ 0:06] 43 [ 0:06] 44 { [ 0:06] 45 if (m_pc == 0) { [ 0:06] 46 goto M_ENTRY; [ 0:06] 47 } else { [ 0:06] 48 if (m_pc == 1) { [ 0:06] 49 goto M_WAIT; [ 0:06] 50 } else { [ 0:06] 51 [ 0:06] 52 } [ 0:06] 53 } [ 0:06] 54 M_ENTRY: ; [ 0:06] 55 { [ 0:06] 56 while (1) { [ 0:06] 57 while_0_continue: /* CIL Label */ ; [ 0:06] 58 { [ 0:06] 59 E_1 = 1; [ 0:06] 60 immediate_notify(); [ 0:06] 61 E_1 = 2; [ 0:06] 62 } [ 0:06] 63 { [ 0:06] 64 while (1) { [ 0:06] 65 while_1_continue: /* CIL Label */ ; [ 0:06] 66 m_pc = 1; [ 0:06] 67 m_st = 2; [ 0:06] 68 [ 0:06] 69 goto return_label; [ 0:06] 70 M_WAIT: ; [ 0:06] 71 } [ 0:06] 72 while_1_break: /* CIL Label */ ; [ 0:06] 73 } [ 0:06] 74 } [ 0:06] 75 while_0_break: /* CIL Label */ ; [ 0:06] 76 } [ 0:06] 77 [ 0:06] 78 return_label: /* CIL Label */ [ 0:06] 79 return; [ 0:06] 80 } [ 0:06] 81 } [ 0:06] 82 void transmit1(void) [ 0:06] 83 { [ 0:06] 84 [ 0:06] 85 { [ 0:06] 86 if (t1_pc == 0) { [ 0:06] 87 goto T1_ENTRY; [ 0:06] 88 } else { [ 0:06] 89 if (t1_pc == 1) { [ 0:06] 90 goto T1_WAIT; [ 0:06] 91 } else { [ 0:06] 92 [ 0:06] 93 } [ 0:06] 94 } [ 0:06] 95 T1_ENTRY: ; [ 0:06] 96 { [ 0:06] 97 while (1) { [ 0:06] 98 while_2_continue: /* CIL Label */ ; [ 0:06] 99 t1_pc = 1; [ 0:06] 100 t1_st = 2; [ 0:06] 101 [ 0:06] 102 goto return_label; [ 0:06] 103 T1_WAIT: [ 0:06] 104 { [ 0:06] 105 E_2 = 1; [ 0:06] 106 immediate_notify(); [ 0:06] 107 E_2 = 2; [ 0:06] 108 } [ 0:06] 109 } [ 0:06] 110 while_2_break: /* CIL Label */ ; [ 0:06] 111 } [ 0:06] 112 [ 0:06] 113 return_label: /* CIL Label */ [ 0:06] 114 return; [ 0:06] 115 } [ 0:06] 116 } [ 0:06] 117 void transmit2(void) [ 0:06] 118 { [ 0:06] 119 [ 0:06] 120 { [ 0:06] 121 if (t2_pc == 0) { [ 0:06] 122 goto T2_ENTRY; [ 0:06] 123 } else { [ 0:06] 124 if (t2_pc == 1) { [ 0:06] 125 goto T2_WAIT; [ 0:06] 126 } else { [ 0:06] 127 [ 0:06] 128 } [ 0:06] 129 } [ 0:06] 130 T2_ENTRY: ; [ 0:06] 131 { [ 0:06] 132 while (1) { [ 0:06] 133 while_3_continue: /* CIL Label */ ; [ 0:06] 134 t2_pc = 1; [ 0:06] 135 t2_st = 2; [ 0:06] 136 [ 0:06] 137 goto return_label; [ 0:06] 138 T2_WAIT: [ 0:06] 139 { [ 0:06] 140 E_3 = 1; [ 0:06] 141 immediate_notify(); [ 0:06] 142 E_3 = 2; [ 0:06] 143 } [ 0:06] 144 } [ 0:06] 145 while_3_break: /* CIL Label */ ; [ 0:06] 146 } [ 0:06] 147 [ 0:06] 148 return_label: /* CIL Label */ [ 0:06] 149 return; [ 0:06] 150 } [ 0:06] 151 } [ 0:06] 152 void transmit3(void) [ 0:06] 153 { [ 0:06] 154 [ 0:06] 155 { [ 0:06] 156 if (t3_pc == 0) { [ 0:06] 157 goto T3_ENTRY; [ 0:06] 158 } else { [ 0:06] 159 if (t3_pc == 1) { [ 0:06] 160 goto T3_WAIT; [ 0:06] 161 } else { [ 0:06] 162 [ 0:06] 163 } [ 0:06] 164 } [ 0:06] 165 T3_ENTRY: ; [ 0:06] 166 { [ 0:06] 167 while (1) { [ 0:06] 168 while_4_continue: /* CIL Label */ ; [ 0:06] 169 t3_pc = 1; [ 0:06] 170 t3_st = 2; [ 0:06] 171 [ 0:06] 172 goto return_label; [ 0:06] 173 T3_WAIT: [ 0:06] 174 { [ 0:06] 175 error(); [ 0:06] 176 } [ 0:06] 177 } [ 0:06] 178 while_4_break: /* CIL Label */ ; [ 0:06] 179 } [ 0:06] 180 [ 0:06] 181 return_label: /* CIL Label */ [ 0:06] 182 return; [ 0:06] 183 } [ 0:06] 184 } [ 0:06] 185 int is_master_triggered(void) [ 0:06] 186 { int __retres1 ; [ 0:06] 187 [ 0:06] 188 { [ 0:06] 189 if (m_pc == 1) { [ 0:06] 190 if (M_E == 1) { [ 0:06] 191 __retres1 = 1; [ 0:06] 192 goto return_label; [ 0:06] 193 } else { [ 0:06] 194 [ 0:06] 195 } [ 0:06] 196 } else { [ 0:06] 197 [ 0:06] 198 } [ 0:06] 199 __retres1 = 0; [ 0:06] 200 return_label: /* CIL Label */ [ 0:06] 201 return (__retres1); [ 0:06] 202 } [ 0:06] 203 } [ 0:06] 204 int is_transmit1_triggered(void) [ 0:06] 205 { int __retres1 ; [ 0:06] 206 [ 0:06] 207 { [ 0:06] 208 if (t1_pc == 1) { [ 0:06] 209 if (E_1 == 1) { [ 0:06] 210 __retres1 = 1; [ 0:06] 211 goto return_label; [ 0:06] 212 } else { [ 0:06] 213 [ 0:06] 214 } [ 0:06] 215 } else { [ 0:06] 216 [ 0:06] 217 } [ 0:06] 218 __retres1 = 0; [ 0:06] 219 return_label: /* CIL Label */ [ 0:06] 220 return (__retres1); [ 0:06] 221 } [ 0:06] 222 } [ 0:06] 223 int is_transmit2_triggered(void) [ 0:06] 224 { int __retres1 ; [ 0:06] 225 [ 0:06] 226 { [ 0:06] 227 if (t2_pc == 1) { [ 0:06] 228 if (E_2 == 1) { [ 0:06] 229 __retres1 = 1; [ 0:06] 230 goto return_label; [ 0:06] 231 } else { [ 0:06] 232 [ 0:06] 233 } [ 0:06] 234 } else { [ 0:06] 235 [ 0:06] 236 } [ 0:06] 237 __retres1 = 0; [ 0:06] 238 return_label: /* CIL Label */ [ 0:06] 239 return (__retres1); [ 0:06] 240 } [ 0:06] 241 } [ 0:06] 242 int is_transmit3_triggered(void) [ 0:06] 243 { int __retres1 ; [ 0:06] 244 [ 0:06] 245 { [ 0:06] 246 if (t3_pc == 1) { [ 0:06] 247 if (E_3 == 1) { [ 0:06] 248 __retres1 = 1; [ 0:06] 249 goto return_label; [ 0:06] 250 } else { [ 0:06] 251 [ 0:06] 252 } [ 0:06] 253 } else { [ 0:06] 254 [ 0:06] 255 } [ 0:06] 256 __retres1 = 0; [ 0:06] 257 return_label: /* CIL Label */ [ 0:06] 258 return (__retres1); [ 0:06] 259 } [ 0:06] 260 } [ 0:06] 261 void update_channels(void) [ 0:06] 262 { [ 0:06] 263 [ 0:06] 264 { [ 0:06] 265 [ 0:06] 266 return; [ 0:06] 267 } [ 0:06] 268 } [ 0:06] 269 void init_threads(void) [ 0:06] 270 { [ 0:06] 271 [ 0:06] 272 { [ 0:06] 273 if (m_i == 1) { [ 0:06] 274 m_st = 0; [ 0:06] 275 } else { [ 0:06] 276 m_st = 2; [ 0:06] 277 } [ 0:06] 278 if (t1_i == 1) { [ 0:06] 279 t1_st = 0; [ 0:06] 280 } else { [ 0:06] 281 t1_st = 2; [ 0:06] 282 } [ 0:06] 283 if (t2_i == 1) { [ 0:06] 284 t2_st = 0; [ 0:06] 285 } else { [ 0:06] 286 t2_st = 2; [ 0:06] 287 } [ 0:06] 288 if (t3_i == 1) { [ 0:06] 289 t3_st = 0; [ 0:06] 290 } else { [ 0:06] 291 t3_st = 2; [ 0:06] 292 } [ 0:06] 293 [ 0:06] 294 return; [ 0:06] 295 } [ 0:06] 296 } [ 0:06] 297 int exists_runnable_thread(void) [ 0:06] 298 { int __retres1 ; [ 0:06] 299 [ 0:06] 300 { [ 0:06] 301 if (m_st == 0) { [ 0:06] 302 __retres1 = 1; [ 0:06] 303 goto return_label; [ 0:06] 304 } else { [ 0:06] 305 if (t1_st == 0) { [ 0:06] 306 __retres1 = 1; [ 0:06] 307 goto return_label; [ 0:06] 308 } else { [ 0:06] 309 if (t2_st == 0) { [ 0:06] 310 __retres1 = 1; [ 0:06] 311 goto return_label; [ 0:06] 312 } else { [ 0:06] 313 if (t3_st == 0) { [ 0:06] 314 __retres1 = 1; [ 0:06] 315 goto return_label; [ 0:06] 316 } else { [ 0:06] 317 [ 0:06] 318 } [ 0:06] 319 } [ 0:06] 320 } [ 0:06] 321 } [ 0:06] 322 __retres1 = 0; [ 0:06] 323 return_label: /* CIL Label */ [ 0:06] 324 return (__retres1); [ 0:06] 325 } [ 0:06] 326 } [ 0:06] 327 void eval(void) [ 0:06] 328 { [ 0:06] 329 int tmp ; [ 0:06] 330 [ 0:06] 331 { [ 0:06] 332 { [ 0:06] 333 while (1) { [ 0:06] 334 while_5_continue: /* CIL Label */ ; [ 0:06] 335 { [ 0:06] 336 tmp = exists_runnable_thread(); [ 0:06] 337 } [ 0:06] 338 if (tmp) { [ 0:06] 339 [ 0:06] 340 } else { [ 0:06] 341 goto while_5_break; [ 0:06] 342 } [ 0:06] 343 if (m_st == 0) { [ 0:06] 344 int tmp_ndt_1; [ 0:06] 345 tmp_ndt_1 = __VERIFIER_nondet_int(); [ 0:06] 346 if (tmp_ndt_1) { [ 0:06] 347 { [ 0:06] 348 m_st = 1; [ 0:06] 349 master(); [ 0:06] 350 } [ 0:06] 351 } else { [ 0:06] 352 [ 0:06] 353 } [ 0:06] 354 } else { [ 0:06] 355 [ 0:06] 356 } [ 0:06] 357 if (t1_st == 0) { [ 0:06] 358 int tmp_ndt_2; [ 0:06] 359 tmp_ndt_2 = __VERIFIER_nondet_int(); [ 0:06] 360 if (tmp_ndt_2) { [ 0:06] 361 { [ 0:06] 362 t1_st = 1; [ 0:06] 363 transmit1(); [ 0:06] 364 } [ 0:06] 365 } else { [ 0:06] 366 [ 0:06] 367 } [ 0:06] 368 } else { [ 0:06] 369 [ 0:06] 370 } [ 0:06] 371 if (t2_st == 0) { [ 0:06] 372 int tmp_ndt_3; [ 0:06] 373 tmp_ndt_3 = __VERIFIER_nondet_int(); [ 0:06] 374 if (tmp_ndt_3) { [ 0:06] 375 { [ 0:06] 376 t2_st = 1; [ 0:06] 377 transmit2(); [ 0:06] 378 } [ 0:06] 379 } else { [ 0:06] 380 [ 0:06] 381 } [ 0:06] 382 } else { [ 0:06] 383 [ 0:06] 384 } [ 0:06] 385 if (t3_st == 0) { [ 0:06] 386 int tmp_ndt_4; [ 0:06] 387 tmp_ndt_4 = __VERIFIER_nondet_int(); [ 0:06] 388 if (tmp_ndt_4) { [ 0:06] 389 { [ 0:06] 390 t3_st = 1; [ 0:06] 391 transmit3(); [ 0:06] 392 } [ 0:06] 393 } else { [ 0:06] 394 [ 0:06] 395 } [ 0:06] 396 } else { [ 0:06] 397 [ 0:06] 398 } [ 0:06] 399 } [ 0:06] 400 while_5_break: /* CIL Label */ ; [ 0:06] 401 } [ 0:06] 402 [ 0:06] 403 return; [ 0:06] 404 } [ 0:06] 405 } [ 0:06] 406 void fire_delta_events(void) [ 0:06] 407 { [ 0:06] 408 [ 0:06] 409 { [ 0:06] 410 if (M_E == 0) { [ 0:06] 411 M_E = 1; [ 0:06] 412 } else { [ 0:06] 413 [ 0:06] 414 } [ 0:06] 415 if (T1_E == 0) { [ 0:06] 416 T1_E = 1; [ 0:06] 417 } else { [ 0:06] 418 [ 0:06] 419 } [ 0:06] 420 if (T2_E == 0) { [ 0:06] 421 T2_E = 1; [ 0:06] 422 } else { [ 0:06] 423 [ 0:06] 424 } [ 0:06] 425 if (T3_E == 0) { [ 0:06] 426 T3_E = 1; [ 0:06] 427 } else { [ 0:06] 428 [ 0:06] 429 } [ 0:06] 430 if (E_1 == 0) { [ 0:06] 431 E_1 = 1; [ 0:06] 432 } else { [ 0:06] 433 [ 0:06] 434 } [ 0:06] 435 if (E_2 == 0) { [ 0:06] 436 E_2 = 1; [ 0:06] 437 } else { [ 0:06] 438 [ 0:06] 439 } [ 0:06] 440 if (E_3 == 0) { [ 0:06] 441 E_3 = 1; [ 0:06] 442 } else { [ 0:06] 443 [ 0:06] 444 } [ 0:06] 445 [ 0:06] 446 return; [ 0:06] 447 } [ 0:06] 448 } [ 0:06] 449 void reset_delta_events(void) [ 0:06] 450 { [ 0:06] 451 [ 0:06] 452 { [ 0:06] 453 if (M_E == 1) { [ 0:06] 454 M_E = 2; [ 0:06] 455 } else { [ 0:06] 456 [ 0:06] 457 } [ 0:06] 458 if (T1_E == 1) { [ 0:06] 459 T1_E = 2; [ 0:06] 460 } else { [ 0:06] 461 [ 0:06] 462 } [ 0:06] 463 if (T2_E == 1) { [ 0:06] 464 T2_E = 2; [ 0:06] 465 } else { [ 0:06] 466 [ 0:06] 467 } [ 0:06] 468 if (T3_E == 1) { [ 0:06] 469 T3_E = 2; [ 0:06] 470 } else { [ 0:06] 471 [ 0:06] 472 } [ 0:06] 473 if (E_1 == 1) { [ 0:06] 474 E_1 = 2; [ 0:06] 475 } else { [ 0:06] 476 [ 0:06] 477 } [ 0:06] 478 if (E_2 == 1) { [ 0:06] 479 E_2 = 2; [ 0:06] 480 } else { [ 0:06] 481 [ 0:06] 482 } [ 0:06] 483 if (E_3 == 1) { [ 0:06] 484 E_3 = 2; [ 0:06] 485 } else { [ 0:06] 486 [ 0:06] 487 } [ 0:06] 488 [ 0:06] 489 return; [ 0:06] 490 } [ 0:06] 491 } [ 0:06] 492 void activate_threads(void) [ 0:06] 493 { int tmp ; [ 0:06] 494 int tmp___0 ; [ 0:06] 495 int tmp___1 ; [ 0:06] 496 int tmp___2 ; [ 0:06] 497 [ 0:06] 498 { [ 0:06] 499 { [ 0:06] 500 tmp = is_master_triggered(); [ 0:06] 501 } [ 0:06] 502 if (tmp) { [ 0:06] 503 m_st = 0; [ 0:06] 504 } else { [ 0:06] 505 [ 0:06] 506 } [ 0:06] 507 { [ 0:06] 508 tmp___0 = is_transmit1_triggered(); [ 0:06] 509 } [ 0:06] 510 if (tmp___0) { [ 0:06] 511 t1_st = 0; [ 0:06] 512 } else { [ 0:06] 513 [ 0:06] 514 } [ 0:06] 515 { [ 0:06] 516 tmp___1 = is_transmit2_triggered(); [ 0:06] 517 } [ 0:06] 518 if (tmp___1) { [ 0:06] 519 t2_st = 0; [ 0:06] 520 } else { [ 0:06] 521 [ 0:06] 522 } [ 0:06] 523 { [ 0:06] 524 tmp___2 = is_transmit3_triggered(); [ 0:06] 525 } [ 0:06] 526 if (tmp___2) { [ 0:06] 527 t3_st = 0; [ 0:06] 528 } else { [ 0:06] 529 [ 0:06] 530 } [ 0:06] 531 [ 0:06] 532 return; [ 0:06] 533 } [ 0:06] 534 } [ 0:06] 535 void immediate_notify(void) [ 0:06] 536 { [ 0:06] 537 [ 0:06] 538 { [ 0:06] 539 { [ 0:06] 540 activate_threads(); [ 0:06] 541 } [ 0:06] 542 [ 0:06] 543 return; [ 0:06] 544 } [ 0:06] 545 } [ 0:06] 546 void fire_time_events(void) [ 0:06] 547 { [ 0:06] 548 [ 0:06] 549 { [ 0:06] 550 M_E = 1; [ 0:06] 551 [ 0:06] 552 return; [ 0:06] 553 } [ 0:06] 554 } [ 0:06] 555 void reset_time_events(void) [ 0:06] 556 { [ 0:06] 557 [ 0:06] 558 { [ 0:06] 559 if (M_E == 1) { [ 0:06] 560 M_E = 2; [ 0:06] 561 } else { [ 0:06] 562 [ 0:06] 563 } [ 0:06] 564 if (T1_E == 1) { [ 0:06] 565 T1_E = 2; [ 0:06] 566 } else { [ 0:06] 567 [ 0:06] 568 } [ 0:06] 569 if (T2_E == 1) { [ 0:06] 570 T2_E = 2; [ 0:06] 571 } else { [ 0:06] 572 [ 0:06] 573 } [ 0:06] 574 if (T3_E == 1) { [ 0:06] 575 T3_E = 2; [ 0:06] 576 } else { [ 0:06] 577 [ 0:06] 578 } [ 0:06] 579 if (E_1 == 1) { [ 0:06] 580 E_1 = 2; [ 0:06] 581 } else { [ 0:06] 582 [ 0:06] 583 } [ 0:06] 584 if (E_2 == 1) { [ 0:06] 585 E_2 = 2; [ 0:06] 586 } else { [ 0:06] 587 [ 0:06] 588 } [ 0:06] 589 if (E_3 == 1) { [ 0:06] 590 E_3 = 2; [ 0:06] 591 } else { [ 0:06] 592 [ 0:06] 593 } [ 0:06] 594 [ 0:06] 595 return; [ 0:06] 596 } [ 0:06] 597 } [ 0:06] 598 void init_model(void) [ 0:06] 599 { [ 0:06] 600 [ 0:06] 601 { [ 0:06] 602 m_i = 1; [ 0:06] 603 t1_i = 1; [ 0:06] 604 t2_i = 1; [ 0:06] 605 t3_i = 1; [ 0:06] 606 [ 0:06] 607 return; [ 0:06] 608 } [ 0:06] 609 } [ 0:06] 610 int stop_simulation(void) [ 0:06] 611 { int tmp ; [ 0:06] 612 int __retres2 ; [ 0:06] 613 [ 0:06] 614 { [ 0:06] 615 { [ 0:06] 616 tmp = exists_runnable_thread(); [ 0:06] 617 } [ 0:06] 618 if (tmp) { [ 0:06] 619 __retres2 = 0; [ 0:06] 620 goto return_label; [ 0:06] 621 } else { [ 0:06] 622 [ 0:06] 623 } [ 0:06] 624 __retres2 = 1; [ 0:06] 625 return_label: /* CIL Label */ [ 0:06] 626 return (__retres2); [ 0:06] 627 } [ 0:06] 628 } [ 0:06] 629 void start_simulation(void) [ 0:06] 630 { int kernel_st ; [ 0:06] 631 int tmp ; [ 0:06] 632 int tmp___0 ; [ 0:06] 633 [ 0:06] 634 { [ 0:06] 635 { [ 0:06] 636 kernel_st = 0; [ 0:06] 637 update_channels(); [ 0:06] 638 init_threads(); [ 0:06] 639 fire_delta_events(); [ 0:06] 640 activate_threads(); [ 0:06] 641 reset_delta_events(); [ 0:06] 642 } [ 0:06] 643 { [ 0:06] 644 while (1) { [ 0:06] 645 while_6_continue: /* CIL Label */ ; [ 0:06] 646 { [ 0:06] 647 kernel_st = 1; [ 0:06] 648 eval(); [ 0:06] 649 } [ 0:06] 650 { [ 0:06] 651 kernel_st = 2; [ 0:06] 652 update_channels(); [ 0:06] 653 } [ 0:06] 654 { [ 0:06] 655 kernel_st = 3; [ 0:06] 656 fire_delta_events(); [ 0:06] 657 activate_threads(); [ 0:06] 658 reset_delta_events(); [ 0:06] 659 } [ 0:06] 660 { [ 0:06] 661 tmp = exists_runnable_thread(); [ 0:06] 662 } [ 0:06] 663 if (tmp == 0) { [ 0:06] 664 { [ 0:06] 665 kernel_st = 4; [ 0:06] 666 fire_time_events(); [ 0:06] 667 activate_threads(); [ 0:06] 668 reset_time_events(); [ 0:06] 669 } [ 0:06] 670 } else { [ 0:06] 671 [ 0:06] 672 } [ 0:06] 673 { [ 0:06] 674 tmp___0 = stop_simulation(); [ 0:06] 675 } [ 0:06] 676 if (tmp___0) { [ 0:06] 677 goto while_6_break; [ 0:06] 678 } else { [ 0:06] 679 [ 0:06] 680 } [ 0:06] 681 } [ 0:06] 682 while_6_break: /* CIL Label */ ; [ 0:06] 683 } [ 0:06] 684 [ 0:06] 685 return; [ 0:06] 686 } [ 0:06] 687 } [ 0:06] 688 int main(void) [ 0:06] 689 { int __retres1 ; [ 0:06] 690 [ 0:06] 691 { [ 0:06] 692 { [ 0:06] 693 init_model(); [ 0:06] 694 start_simulation(); [ 0:06] 695 } [ 0:06] 696 __retres1 = 0; [ 0:06] 697 return (__retres1); [ 0:06] 698 } [ 0:06] 699 } [ 0:06] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/transmitter.03_false.cil.c:13, but it was not