[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu1_false.cil.c [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu1_false.cil.c:500:3: warning: expression result unused [ 0:01] e ; [ 0:01] ^ [ 0:01] 1 warning generated. [ 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.2/_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: 34830 [ 0:07] Stack: [ 0:07] #000034830 in __dios_start (l=0, argc=1, argv=94198667039240, envp=94198667132936) at /dios/libc/sys/start.cpp:87 [ 0:07] #100010849 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200043180 in klee_boot (argc=2, argv=94198640416768) 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 [ 0:07] 7 void error(void) [ 0:07] 8 { [ 0:07] 9 [ 0:07] 10 { [ 0:07] 11 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:07] 12 return; [ 0:07] 13 } [ 0:07] 14 } [ 0:07] 15 [ 0:07] 16 void immediate_notify(void) ; [ 0:07] 17 int max_loop ; [ 0:07] 18 int num ; [ 0:07] 19 int i ; [ 0:07] 20 int e ; [ 0:07] 21 int timer ; [ 0:07] 22 char data_0 ; [ 0:07] 23 char data_1 ; [ 0:07] 24 char read_data(int i___0 ) [ 0:07] 25 { char c ; [ 0:07] 26 char __retres3 ; [ 0:07] 27 [ 0:07] 28 { [ 0:07] 29 if (i___0 == 0) { [ 0:07] 30 __retres3 = data_0; [ 0:07] 31 goto return_label; [ 0:07] 32 } else { [ 0:07] 33 if (i___0 == 1) { [ 0:07] 34 __retres3 = data_1; [ 0:07] 35 goto return_label; [ 0:07] 36 } else { [ 0:07] 37 { [ 0:07] 38 error(); [ 0:07] 39 } [ 0:07] 40 } [ 0:07] 41 } [ 0:07] 42 __retres3 = c; [ 0:07] 43 return_label: /* CIL Label */ [ 0:07] 44 return (__retres3); [ 0:07] 45 } [ 0:07] 46 } [ 0:07] 47 void write_data(int i___0 , char c ) [ 0:07] 48 { [ 0:07] 49 [ 0:07] 50 { [ 0:07] 51 if (i___0 == 0) { [ 0:07] 52 data_0 = c; [ 0:07] 53 } else { [ 0:07] 54 if (i___0 == 1) { [ 0:07] 55 data_1 = c; [ 0:07] 56 } else { [ 0:07] 57 { [ 0:07] 58 error(); [ 0:07] 59 } [ 0:07] 60 } [ 0:07] 61 } [ 0:07] 62 [ 0:07] 63 return; [ 0:07] 64 } [ 0:07] 65 } [ 0:07] 66 int P_1_pc; [ 0:07] 67 int P_1_st ; [ 0:07] 68 int P_1_i ; [ 0:07] 69 int P_1_ev ; [ 0:07] 70 void P_1(void) [ 0:07] 71 { [ 0:07] 72 [ 0:07] 73 { [ 0:07] 74 if ((int )P_1_pc == 0) { [ 0:07] 75 goto P_1_ENTRY_LOC; [ 0:07] 76 } else { [ 0:07] 77 if ((int )P_1_pc == 1) { [ 0:07] 78 goto P_1_WAIT_LOC; [ 0:07] 79 } else { [ 0:07] 80 [ 0:07] 81 } [ 0:07] 82 } [ 0:07] 83 P_1_ENTRY_LOC: [ 0:07] 84 { [ 0:07] 85 while (i < max_loop) { [ 0:07] 86 while_0_continue: /* CIL Label */ ; [ 0:07] 87 { [ 0:07] 88 write_data(num, 'A'); [ 0:07] 89 num += 1; [ 0:07] 90 P_1_pc = 1; [ 0:07] 91 P_1_st = 2; [ 0:07] 92 } [ 0:07] 93 [ 0:07] 94 goto return_label; [ 0:07] 95 P_1_WAIT_LOC: ; [ 0:07] 96 } [ 0:07] 97 while_0_break: /* CIL Label */ ; [ 0:07] 98 } [ 0:07] 99 P_1_st = 2; [ 0:07] 100 [ 0:07] 101 return_label: /* CIL Label */ [ 0:07] 102 return; [ 0:07] 103 } [ 0:07] 104 } [ 0:07] 105 int is_P_1_triggered(void) [ 0:07] 106 { int __retres1 ; [ 0:07] 107 [ 0:07] 108 { [ 0:07] 109 if ((int )P_1_pc == 1) { [ 0:07] 110 if ((int )P_1_ev == 1) { [ 0:07] 111 __retres1 = 1; [ 0:07] 112 goto return_label; [ 0:07] 113 } else { [ 0:07] 114 [ 0:07] 115 } [ 0:07] 116 } else { [ 0:07] 117 [ 0:07] 118 } [ 0:07] 119 __retres1 = 0; [ 0:07] 120 return_label: /* CIL Label */ [ 0:07] 121 return (__retres1); [ 0:07] 122 } [ 0:07] 123 } [ 0:07] 124 int C_1_pc ; [ 0:07] 125 int C_1_st ; [ 0:07] 126 int C_1_i ; [ 0:07] 127 int C_1_ev ; [ 0:07] 128 int C_1_pr ; [ 0:07] 129 void C_1(void) [ 0:07] 130 { char c ; [ 0:07] 131 [ 0:07] 132 { [ 0:07] 133 if ((int )C_1_pc == 0) { [ 0:07] 134 goto C_1_ENTRY_LOC; [ 0:07] 135 } else { [ 0:07] 136 if ((int )C_1_pc == 1) { [ 0:07] 137 goto C_1_WAIT_1_LOC; [ 0:07] 138 } else { [ 0:07] 139 if ((int )C_1_pc == 2) { [ 0:07] 140 goto C_1_WAIT_2_LOC; [ 0:07] 141 } else { [ 0:07] 142 [ 0:07] 143 } [ 0:07] 144 } [ 0:07] 145 } [ 0:07] 146 C_1_ENTRY_LOC: [ 0:07] 147 { [ 0:07] 148 while (i < max_loop) { [ 0:07] 149 while_2_continue: /* CIL Label */ ; [ 0:07] 150 if (num == 0) { [ 0:07] 151 timer = 1; [ 0:07] 152 i += 1; [ 0:07] 153 C_1_pc = 1; [ 0:07] 154 C_1_st = 2; [ 0:07] 155 [ 0:07] 156 goto return_label; [ 0:07] 157 C_1_WAIT_1_LOC: ; [ 0:07] 158 } else { [ 0:07] 159 [ 0:07] 160 } [ 0:07] 161 num -= 1; [ 0:07] 162 if (! (num >= 0)) { [ 0:07] 163 { [ 0:07] 164 error(); [ 0:07] 165 } [ 0:07] 166 } else { [ 0:07] 167 [ 0:07] 168 } [ 0:07] 169 { [ 0:07] 170 c = read_data(num); [ 0:07] 171 i += 1; [ 0:07] 172 C_1_pc = 2; [ 0:07] 173 C_1_st = 2; [ 0:07] 174 } [ 0:07] 175 [ 0:07] 176 goto return_label; [ 0:07] 177 C_1_WAIT_2_LOC: ; [ 0:07] 178 } [ 0:07] 179 while_2_break: /* CIL Label */ ; [ 0:07] 180 } [ 0:07] 181 C_1_st = 2; [ 0:07] 182 [ 0:07] 183 return_label: /* CIL Label */ [ 0:07] 184 return; [ 0:07] 185 } [ 0:07] 186 } [ 0:07] 187 int is_C_1_triggered(void) [ 0:07] 188 { int __retres1 ; [ 0:07] 189 [ 0:07] 190 { [ 0:07] 191 if ((int )C_1_pc == 1) { [ 0:07] 192 if ((int )e == 1) { [ 0:07] 193 __retres1 = 1; [ 0:07] 194 goto return_label; [ 0:07] 195 } else { [ 0:07] 196 [ 0:07] 197 } [ 0:07] 198 } else { [ 0:07] 199 [ 0:07] 200 } [ 0:07] 201 if ((int )C_1_pc == 2) { [ 0:07] 202 if ((int )C_1_ev == 1) { [ 0:07] 203 __retres1 = 1; [ 0:07] 204 goto return_label; [ 0:07] 205 } else { [ 0:07] 206 [ 0:07] 207 } [ 0:07] 208 } else { [ 0:07] 209 [ 0:07] 210 } [ 0:07] 211 __retres1 = 0; [ 0:07] 212 return_label: /* CIL Label */ [ 0:07] 213 return (__retres1); [ 0:07] 214 } [ 0:07] 215 } [ 0:07] 216 void update_channels(void) [ 0:07] 217 { [ 0:07] 218 [ 0:07] 219 { [ 0:07] 220 [ 0:07] 221 return; [ 0:07] 222 } [ 0:07] 223 } [ 0:07] 224 void init_threads(void) [ 0:07] 225 { [ 0:07] 226 [ 0:07] 227 { [ 0:07] 228 if ((int )P_1_i == 1) { [ 0:07] 229 P_1_st = 0; [ 0:07] 230 } else { [ 0:07] 231 P_1_st = 2; [ 0:07] 232 } [ 0:07] 233 if ((int )C_1_i == 1) { [ 0:07] 234 C_1_st = 0; [ 0:07] 235 } else { [ 0:07] 236 C_1_st = 2; [ 0:07] 237 } [ 0:07] 238 [ 0:07] 239 return; [ 0:07] 240 } [ 0:07] 241 } [ 0:07] 242 int exists_runnable_thread(void) [ 0:07] 243 { int __retres1 ; [ 0:07] 244 [ 0:07] 245 { [ 0:07] 246 if ((int )P_1_st == 0) { [ 0:07] 247 __retres1 = 1; [ 0:07] 248 goto return_label; [ 0:07] 249 } else { [ 0:07] 250 if ((int )C_1_st == 0) { [ 0:07] 251 __retres1 = 1; [ 0:07] 252 goto return_label; [ 0:07] 253 } else { [ 0:07] 254 [ 0:07] 255 } [ 0:07] 256 } [ 0:07] 257 } [ 0:07] 258 __retres1 = 0; [ 0:07] 259 return_label: /* CIL Label */ [ 0:07] 260 return (__retres1); [ 0:07] 261 } [ 0:07] 262 [ 0:07] 263 void eval(void) [ 0:07] 264 { int tmp ; [ 0:07] 265 int tmp___0 ; [ 0:07] 266 int tmp___1 ; [ 0:07] 267 int tmp___2 ; [ 0:07] 268 [ 0:07] 269 { [ 0:07] 270 { [ 0:07] 271 while (1) { [ 0:07] 272 while_3_continue: /* CIL Label */ ; [ 0:07] 273 { [ 0:07] 274 tmp___2 = exists_runnable_thread(); [ 0:07] 275 } [ 0:07] 276 if (tmp___2) { [ 0:07] 277 [ 0:07] 278 } else { [ 0:07] 279 goto while_3_break; [ 0:07] 280 } [ 0:07] 281 if ((int )P_1_st == 0) { [ 0:07] 282 { [ 0:07] 283 tmp = __VERIFIER_nondet_int(); [ 0:07] 284 } [ 0:07] 285 if (tmp) { [ 0:07] 286 { [ 0:07] 287 P_1_st = 1; [ 0:07] 288 P_1(); [ 0:07] 289 } [ 0:07] 290 } else { [ 0:07] 291 [ 0:07] 292 } [ 0:07] 293 } else { [ 0:07] 294 [ 0:07] 295 } [ 0:07] 296 if ((int )C_1_st == 0) { [ 0:07] 297 { [ 0:07] 298 tmp___1 = __VERIFIER_nondet_int(); [ 0:07] 299 } [ 0:07] 300 if (tmp___1) { [ 0:07] 301 { [ 0:07] 302 C_1_st = 1; [ 0:07] 303 C_1(); [ 0:07] 304 } [ 0:07] 305 } else { [ 0:07] 306 [ 0:07] 307 } [ 0:07] 308 } else { [ 0:07] 309 [ 0:07] 310 } [ 0:07] 311 } [ 0:07] 312 while_3_break: /* CIL Label */ ; [ 0:07] 313 } [ 0:07] 314 [ 0:07] 315 return; [ 0:07] 316 } [ 0:07] 317 } [ 0:07] 318 void fire_delta_events(void) [ 0:07] 319 { [ 0:07] 320 [ 0:07] 321 { [ 0:07] 322 [ 0:07] 323 return; [ 0:07] 324 } [ 0:07] 325 } [ 0:07] 326 void reset_delta_events(void) [ 0:07] 327 { [ 0:07] 328 [ 0:07] 329 { [ 0:07] 330 [ 0:07] 331 return; [ 0:07] 332 } [ 0:07] 333 } [ 0:07] 334 void fire_time_events(void) [ 0:07] 335 { [ 0:07] 336 [ 0:07] 337 { [ 0:07] 338 C_1_ev = 1; [ 0:07] 339 [ 0:07] 340 P_1_ev = 1; [ 0:07] 341 [ 0:07] 342 [ 0:07] 343 [ 0:07] 344 [ 0:07] 345 return; [ 0:07] 346 } [ 0:07] 347 } [ 0:07] 348 void reset_time_events(void) [ 0:07] 349 { [ 0:07] 350 [ 0:07] 351 { [ 0:07] 352 if ((int )P_1_ev == 1) { [ 0:07] 353 P_1_ev = 2; [ 0:07] 354 } else { [ 0:07] 355 [ 0:07] 356 } [ 0:07] 357 if ((int )C_1_ev == 1) { [ 0:07] 358 C_1_ev = 2; [ 0:07] 359 } else { [ 0:07] 360 [ 0:07] 361 } [ 0:07] 362 [ 0:07] 363 return; [ 0:07] 364 } [ 0:07] 365 } [ 0:07] 366 void activate_threads(void) [ 0:07] 367 { int tmp ; [ 0:07] 368 int tmp___0 ; [ 0:07] 369 int tmp___1 ; [ 0:07] 370 [ 0:07] 371 { [ 0:07] 372 { [ 0:07] 373 tmp = is_P_1_triggered(); [ 0:07] 374 } [ 0:07] 375 if (tmp) { [ 0:07] 376 P_1_st = 0; [ 0:07] 377 } else { [ 0:07] 378 [ 0:07] 379 } [ 0:07] 380 { [ 0:07] 381 tmp___1 = is_C_1_triggered(); [ 0:07] 382 } [ 0:07] 383 if (tmp___1) { [ 0:07] 384 C_1_st = 0; [ 0:07] 385 } else { [ 0:07] 386 [ 0:07] 387 } [ 0:07] 388 [ 0:07] 389 return; [ 0:07] 390 } [ 0:07] 391 } [ 0:07] 392 void immediate_notify(void) [ 0:07] 393 { [ 0:07] 394 [ 0:07] 395 { [ 0:07] 396 { [ 0:07] 397 activate_threads(); [ 0:07] 398 } [ 0:07] 399 [ 0:07] 400 return; [ 0:07] 401 } [ 0:07] 402 } [ 0:07] 403 int stop_simulation(void) [ 0:07] 404 { int tmp ; [ 0:07] 405 int __retres2 ; [ 0:07] 406 [ 0:07] 407 { [ 0:07] 408 { [ 0:07] 409 tmp = exists_runnable_thread(); [ 0:07] 410 } [ 0:07] 411 if (tmp) { [ 0:07] 412 __retres2 = 0; [ 0:07] 413 goto return_label; [ 0:07] 414 } else { [ 0:07] 415 [ 0:07] 416 } [ 0:07] 417 __retres2 = 1; [ 0:07] 418 return_label: /* CIL Label */ [ 0:07] 419 return (__retres2); [ 0:07] 420 } [ 0:07] 421 } [ 0:07] 422 void start_simulation(void) [ 0:07] 423 { int kernel_st ; [ 0:07] 424 int tmp ; [ 0:07] 425 int tmp___0 ; [ 0:07] 426 [ 0:07] 427 { [ 0:07] 428 { [ 0:07] 429 kernel_st = 0; [ 0:07] 430 update_channels(); [ 0:07] 431 init_threads(); [ 0:07] 432 fire_delta_events(); [ 0:07] 433 activate_threads(); [ 0:07] 434 reset_delta_events(); [ 0:07] 435 } [ 0:07] 436 { [ 0:07] 437 while (1) { [ 0:07] 438 while_4_continue: /* CIL Label */ ; [ 0:07] 439 { [ 0:07] 440 kernel_st = 1; [ 0:07] 441 eval(); [ 0:07] 442 } [ 0:07] 443 { [ 0:07] 444 kernel_st = 2; [ 0:07] 445 update_channels(); [ 0:07] 446 } [ 0:07] 447 { [ 0:07] 448 kernel_st = 3; [ 0:07] 449 fire_delta_events(); [ 0:07] 450 activate_threads(); [ 0:07] 451 reset_delta_events(); [ 0:07] 452 } [ 0:07] 453 { [ 0:07] 454 tmp = exists_runnable_thread(); [ 0:07] 455 } [ 0:07] 456 if (tmp == 0) { [ 0:07] 457 { [ 0:07] 458 kernel_st = 4; [ 0:07] 459 fire_time_events(); [ 0:07] 460 activate_threads(); [ 0:07] 461 reset_time_events(); [ 0:07] 462 } [ 0:07] 463 } else { [ 0:07] 464 [ 0:07] 465 } [ 0:07] 466 { [ 0:07] 467 tmp___0 = stop_simulation(); [ 0:07] 468 } [ 0:07] 469 if (tmp___0) { [ 0:07] 470 goto while_4_break; [ 0:07] 471 } else { [ 0:07] 472 [ 0:07] 473 } [ 0:07] 474 } [ 0:07] 475 while_4_break: /* CIL Label */ ; [ 0:07] 476 } [ 0:07] 477 [ 0:07] 478 return; [ 0:07] 479 } [ 0:07] 480 } [ 0:07] 481 void init_model(void) [ 0:07] 482 { [ 0:07] 483 [ 0:07] 484 { [ 0:07] 485 P_1_i = 1; [ 0:07] 486 C_1_i = 1; [ 0:07] 487 [ 0:07] 488 return; [ 0:07] 489 } [ 0:07] 490 } [ 0:07] 491 int main(void) [ 0:07] 492 { int count ; [ 0:07] 493 int __retres2 ; [ 0:07] 494 [ 0:07] 495 { [ 0:07] 496 { [ 0:07] 497 num = 0; [ 0:07] 498 i = 0; [ 0:07] 499 max_loop = 2; [ 0:07] 500 e ; [ 0:07] 501 timer = 0; [ 0:07] 502 P_1_pc = 0; [ 0:07] 503 C_1_pc = 0; [ 0:07] 504 [ 0:07] 505 count = 0; [ 0:07] 506 init_model(); [ 0:07] 507 start_simulation(); [ 0:07] 508 } [ 0:07] 509 __retres2 = 0; [ 0:07] 510 return (__retres2); [ 0:07] 511 } [ 0:07] 512 } [ 0:07] 513 [ 0:07] 514 [ 0:07] 515 [ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu1_false.cil.c:11, but it was not