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