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