[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/pc_sfifo_2_false.cil.c [ 0:00] compiling /dios/lib/config/seqklee.bc [ 0:00] 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: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: 34772 [ 0:06] Stack: [ 0:06] #000034772 in __dios_start (l=0, argc=1, argv=93998387458568, envp=93998387535880) at /dios/libc/sys/start.cpp:87 [ 0:06] #100010791 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:06] #200043122 in klee_boot (argc=2, argv=93998360868864) 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 [ 0:06] 7 [ 0:06] 8 void error(void) [ 0:06] 9 { [ 0:06] 10 [ 0:06] 11 { [ 0:06] 12 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:06] 13 return; [ 0:06] 14 } [ 0:06] 15 } [ 0:06] 16 [ 0:06] 17 int q_buf_0 ; [ 0:06] 18 int q_free ; [ 0:06] 19 int q_read_ev ; [ 0:06] 20 int q_write_ev ; [ 0:06] 21 int q_req_up ; [ 0:06] 22 int q_ev ; [ 0:06] 23 void update_fifo_q(void) [ 0:06] 24 { [ 0:06] 25 [ 0:06] 26 { [ 0:06] 27 if ((int )q_free == 0) { [ 0:06] 28 q_write_ev = 0; [ 0:06] 29 } else { [ 0:06] 30 [ 0:06] 31 } [ 0:06] 32 if ((int )q_free == 1) { [ 0:06] 33 q_read_ev = 0; [ 0:06] 34 } else { [ 0:06] 35 [ 0:06] 36 } [ 0:06] 37 q_ev = 0; [ 0:06] 38 q_req_up = 0; [ 0:06] 39 [ 0:06] 40 return; [ 0:06] 41 } [ 0:06] 42 } [ 0:06] 43 int p_num_write ; [ 0:06] 44 int p_last_write ; [ 0:06] 45 int p_dw_st ; [ 0:06] 46 int p_dw_pc ; [ 0:06] 47 int p_dw_i ; [ 0:06] 48 int c_num_read ; [ 0:06] 49 int c_last_read ; [ 0:06] 50 int c_dr_st ; [ 0:06] 51 int c_dr_pc ; [ 0:06] 52 int c_dr_i ; [ 0:06] 53 int is_do_write_p_triggered(void) [ 0:06] 54 { int __retres1 ; [ 0:06] 55 [ 0:06] 56 { [ 0:06] 57 if ((int )p_dw_pc == 1) { [ 0:06] 58 if ((int )q_read_ev == 1) { [ 0:06] 59 __retres1 = 1; [ 0:06] 60 goto return_label; [ 0:06] 61 } else { [ 0:06] 62 [ 0:06] 63 } [ 0:06] 64 } else { [ 0:06] 65 [ 0:06] 66 } [ 0:06] 67 __retres1 = 0; [ 0:06] 68 return_label: /* CIL Label */ [ 0:06] 69 return (__retres1); [ 0:06] 70 } [ 0:06] 71 } [ 0:06] 72 int is_do_read_c_triggered(void) [ 0:06] 73 { int __retres1 ; [ 0:06] 74 [ 0:06] 75 { [ 0:06] 76 if ((int )c_dr_pc == 1) { [ 0:06] 77 if ((int )q_write_ev == 1) { [ 0:06] 78 __retres1 = 1; [ 0:06] 79 goto return_label; [ 0:06] 80 } else { [ 0:06] 81 [ 0:06] 82 } [ 0:06] 83 } else { [ 0:06] 84 [ 0:06] 85 } [ 0:06] 86 __retres1 = 0; [ 0:06] 87 return_label: /* CIL Label */ [ 0:06] 88 return (__retres1); [ 0:06] 89 } [ 0:06] 90 } [ 0:06] 91 void immediate_notify_threads(void) [ 0:06] 92 { int tmp ; [ 0:06] 93 int tmp___0 ; [ 0:06] 94 [ 0:06] 95 { [ 0:06] 96 { [ 0:06] 97 tmp = is_do_write_p_triggered(); [ 0:06] 98 } [ 0:06] 99 if (tmp) { [ 0:06] 100 p_dw_st = 0; [ 0:06] 101 } else { [ 0:06] 102 [ 0:06] 103 } [ 0:06] 104 { [ 0:06] 105 tmp___0 = is_do_read_c_triggered(); [ 0:06] 106 } [ 0:06] 107 if (tmp___0) { [ 0:06] 108 c_dr_st = 0; [ 0:06] 109 } else { [ 0:06] 110 [ 0:06] 111 } [ 0:06] 112 [ 0:06] 113 return; [ 0:06] 114 } [ 0:06] 115 } [ 0:06] 116 void do_write_p(void) [ 0:06] 117 { [ 0:06] 118 [ 0:06] 119 { [ 0:06] 120 if ((int )p_dw_pc == 0) { [ 0:06] 121 goto DW_ENTRY; [ 0:06] 122 } else { [ 0:06] 123 if ((int )p_dw_pc == 1) { [ 0:06] 124 goto DW_WAIT_READ; [ 0:06] 125 } else { [ 0:06] 126 [ 0:06] 127 } [ 0:06] 128 } [ 0:06] 129 DW_ENTRY: [ 0:06] 130 { [ 0:06] 131 while (1) { [ 0:06] 132 while_0_continue: /* CIL Label */ ; [ 0:06] 133 if ((int )q_free == 0) { [ 0:06] 134 p_dw_st = 2; [ 0:06] 135 p_dw_pc = 1; [ 0:06] 136 [ 0:06] 137 goto return_label; [ 0:06] 138 DW_WAIT_READ: ; [ 0:06] 139 } else { [ 0:06] 140 [ 0:06] 141 } [ 0:06] 142 { [ 0:06] 143 q_buf_0 = __VERIFIER_nondet_int(); [ 0:06] 144 p_last_write = q_buf_0; [ 0:06] 145 p_num_write += 1; [ 0:06] 146 q_free = 0; [ 0:06] 147 q_req_up = 1; [ 0:06] 148 } [ 0:06] 149 } [ 0:06] 150 while_0_break: /* CIL Label */ ; [ 0:06] 151 } [ 0:06] 152 return_label: /* CIL Label */ [ 0:06] 153 return; [ 0:06] 154 } [ 0:06] 155 } [ 0:06] 156 static int a_t ; [ 0:06] 157 void do_read_c(void) [ 0:06] 158 { int a ; [ 0:06] 159 [ 0:06] 160 { [ 0:06] 161 if ((int )c_dr_pc == 0) { [ 0:06] 162 goto DR_ENTRY; [ 0:06] 163 } else { [ 0:06] 164 if ((int )c_dr_pc == 1) { [ 0:06] 165 goto DR_WAIT_WRITE; [ 0:06] 166 } else { [ 0:06] 167 [ 0:06] 168 } [ 0:06] 169 } [ 0:06] 170 DR_ENTRY: [ 0:06] 171 { [ 0:06] 172 while (1) { [ 0:06] 173 while_1_continue: /* CIL Label */ ; [ 0:06] 174 if ((int )q_free == 1) { [ 0:06] 175 c_dr_st = 2; [ 0:06] 176 c_dr_pc = 1; [ 0:06] 177 a_t = a; [ 0:06] 178 [ 0:06] 179 goto return_label; [ 0:06] 180 DR_WAIT_WRITE: [ 0:06] 181 a = a_t; [ 0:06] 182 } else { [ 0:06] 183 [ 0:06] 184 } [ 0:06] 185 a = q_buf_0; [ 0:06] 186 c_last_read = a; [ 0:06] 187 c_num_read += 1; [ 0:06] 188 q_free = 1; [ 0:06] 189 q_req_up = 1; [ 0:06] 190 if (p_last_write == c_last_read) { [ 0:06] 191 if (p_num_write == c_num_read) { [ 0:06] 192 [ 0:06] 193 } else { [ 0:06] 194 { [ 0:06] 195 error(); [ 0:06] 196 } [ 0:06] 197 } [ 0:06] 198 } else { [ 0:06] 199 { [ 0:06] 200 error(); [ 0:06] 201 } [ 0:06] 202 } [ 0:06] 203 } [ 0:06] 204 while_1_break: /* CIL Label */ ; [ 0:06] 205 } [ 0:06] 206 return_label: /* CIL Label */ [ 0:06] 207 return; [ 0:06] 208 } [ 0:06] 209 } [ 0:06] 210 void update_channels(void) [ 0:06] 211 { [ 0:06] 212 [ 0:06] 213 { [ 0:06] 214 if ((int )q_req_up == 1) { [ 0:06] 215 { [ 0:06] 216 update_fifo_q(); [ 0:06] 217 } [ 0:06] 218 } else { [ 0:06] 219 [ 0:06] 220 } [ 0:06] 221 [ 0:06] 222 return; [ 0:06] 223 } [ 0:06] 224 } [ 0:06] 225 void init_threads(void) [ 0:06] 226 { [ 0:06] 227 [ 0:06] 228 { [ 0:06] 229 if ((int )p_dw_i == 1) { [ 0:06] 230 p_dw_st = 0; [ 0:06] 231 } else { [ 0:06] 232 p_dw_st = 2; [ 0:06] 233 } [ 0:06] 234 if ((int )c_dr_i == 1) { [ 0:06] 235 c_dr_st = 0; [ 0:06] 236 } else { [ 0:06] 237 c_dr_st = 2; [ 0:06] 238 } [ 0:06] 239 [ 0:06] 240 return; [ 0:06] 241 } [ 0:06] 242 } [ 0:06] 243 int exists_runnable_thread(void) [ 0:06] 244 { int __retres1 ; [ 0:06] 245 [ 0:06] 246 { [ 0:06] 247 if ((int )p_dw_st == 0) { [ 0:06] 248 __retres1 = 1; [ 0:06] 249 goto return_label; [ 0:06] 250 } else { [ 0:06] 251 if ((int )c_dr_st == 0) { [ 0:06] 252 __retres1 = 1; [ 0:06] 253 goto return_label; [ 0:06] 254 } else { [ 0:06] 255 [ 0:06] 256 } [ 0:06] 257 } [ 0:06] 258 __retres1 = 0; [ 0:06] 259 return_label: /* CIL Label */ [ 0:06] 260 return (__retres1); [ 0:06] 261 } [ 0:06] 262 } [ 0:06] 263 void fire_delta_events(void) [ 0:06] 264 { [ 0:06] 265 [ 0:06] 266 { [ 0:06] 267 if ((int )q_read_ev == 0) { [ 0:06] 268 q_read_ev = 1; [ 0:06] 269 } else { [ 0:06] 270 [ 0:06] 271 } [ 0:06] 272 if ((int )q_write_ev == 0) { [ 0:06] 273 q_write_ev = 1; [ 0:06] 274 } else { [ 0:06] 275 [ 0:06] 276 } [ 0:06] 277 [ 0:06] 278 return; [ 0:06] 279 } [ 0:06] 280 } [ 0:06] 281 void reset_delta_events(void) [ 0:06] 282 { [ 0:06] 283 [ 0:06] 284 { [ 0:06] 285 if ((int )q_read_ev == 1) { [ 0:06] 286 q_read_ev = 2; [ 0:06] 287 } else { [ 0:06] 288 [ 0:06] 289 } [ 0:06] 290 if ((int )q_write_ev == 1) { [ 0:06] 291 q_write_ev = 2; [ 0:06] 292 } else { [ 0:06] 293 [ 0:06] 294 } [ 0:06] 295 [ 0:06] 296 return; [ 0:06] 297 } [ 0:06] 298 } [ 0:06] 299 void activate_threads(void) [ 0:06] 300 { int tmp ; [ 0:06] 301 int tmp___0 ; [ 0:06] 302 [ 0:06] 303 { [ 0:06] 304 { [ 0:06] 305 tmp = is_do_write_p_triggered(); [ 0:06] 306 } [ 0:06] 307 if (tmp) { [ 0:06] 308 p_dw_st = 0; [ 0:06] 309 } else { [ 0:06] 310 [ 0:06] 311 } [ 0:06] 312 { [ 0:06] 313 tmp___0 = is_do_read_c_triggered(); [ 0:06] 314 } [ 0:06] 315 if (tmp___0) { [ 0:06] 316 c_dr_st = 0; [ 0:06] 317 } else { [ 0:06] 318 [ 0:06] 319 } [ 0:06] 320 [ 0:06] 321 return; [ 0:06] 322 } [ 0:06] 323 } [ 0:06] 324 void eval(void) [ 0:06] 325 { int tmp ; [ 0:06] 326 int tmp___0 ; [ 0:06] 327 int tmp___1 ; [ 0:06] 328 [ 0:06] 329 { [ 0:06] 330 { [ 0:06] 331 while (1) { [ 0:06] 332 while_2_continue: /* CIL Label */ ; [ 0:06] 333 { [ 0:06] 334 tmp___1 = exists_runnable_thread(); [ 0:06] 335 } [ 0:06] 336 if (tmp___1) { [ 0:06] 337 [ 0:06] 338 } else { [ 0:06] 339 goto while_2_break; [ 0:06] 340 } [ 0:06] 341 if ((int )p_dw_st == 0) { [ 0:06] 342 { [ 0:06] 343 tmp = __VERIFIER_nondet_int(); [ 0:06] 344 } [ 0:06] 345 if (tmp) { [ 0:06] 346 { [ 0:06] 347 p_dw_st = 1; [ 0:06] 348 do_write_p(); [ 0:06] 349 } [ 0:06] 350 } else { [ 0:06] 351 error(); [ 0:06] 352 } [ 0:06] 353 } else { [ 0:06] 354 [ 0:06] 355 } [ 0:06] 356 if ((int )c_dr_st == 0) { [ 0:06] 357 { [ 0:06] 358 tmp___0 = __VERIFIER_nondet_int(); [ 0:06] 359 } [ 0:06] 360 if (tmp___0) { [ 0:06] 361 { [ 0:06] 362 c_dr_st = 1; [ 0:06] 363 do_read_c(); [ 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 } [ 0:06] 372 while_2_break: /* CIL Label */ ; [ 0:06] 373 } [ 0:06] 374 [ 0:06] 375 return; [ 0:06] 376 } [ 0:06] 377 } [ 0:06] 378 int stop_simulation(void) [ 0:06] 379 { int tmp ; [ 0:06] 380 int __retres2 ; [ 0:06] 381 [ 0:06] 382 { [ 0:06] 383 { [ 0:06] 384 tmp = exists_runnable_thread(); [ 0:06] 385 } [ 0:06] 386 if (tmp) { [ 0:06] 387 __retres2 = 0; [ 0:06] 388 goto return_label; [ 0:06] 389 } else { [ 0:06] 390 [ 0:06] 391 } [ 0:06] 392 __retres2 = 1; [ 0:06] 393 return_label: /* CIL Label */ [ 0:06] 394 return (__retres2); [ 0:06] 395 } [ 0:06] 396 } [ 0:06] 397 void start_simulation(void) [ 0:06] 398 { int kernel_st ; [ 0:06] 399 int tmp ; [ 0:06] 400 [ 0:06] 401 { [ 0:06] 402 { [ 0:06] 403 kernel_st = 0; [ 0:06] 404 update_channels(); [ 0:06] 405 init_threads(); [ 0:06] 406 fire_delta_events(); [ 0:06] 407 activate_threads(); [ 0:06] 408 reset_delta_events(); [ 0:06] 409 } [ 0:06] 410 { [ 0:06] 411 while (1) { [ 0:06] 412 while_3_continue: /* CIL Label */ ; [ 0:06] 413 { [ 0:06] 414 kernel_st = 1; [ 0:06] 415 eval(); [ 0:06] 416 } [ 0:06] 417 { [ 0:06] 418 kernel_st = 2; [ 0:06] 419 update_channels(); [ 0:06] 420 } [ 0:06] 421 { [ 0:06] 422 kernel_st = 3; [ 0:06] 423 fire_delta_events(); [ 0:06] 424 activate_threads(); [ 0:06] 425 reset_delta_events(); [ 0:06] 426 tmp = stop_simulation(); [ 0:06] 427 } [ 0:06] 428 if (tmp) { [ 0:06] 429 goto while_3_break; [ 0:06] 430 } else { [ 0:06] 431 [ 0:06] 432 } [ 0:06] 433 } [ 0:06] 434 while_3_break: /* CIL Label */ ; [ 0:06] 435 } [ 0:06] 436 [ 0:06] 437 return; [ 0:06] 438 } [ 0:06] 439 } [ 0:06] 440 void init_model(void) [ 0:06] 441 { [ 0:06] 442 [ 0:06] 443 { [ 0:06] 444 q_free = 1; [ 0:06] 445 q_write_ev = 2; [ 0:06] 446 q_read_ev = q_write_ev; [ 0:06] 447 p_num_write = 0; [ 0:06] 448 p_dw_pc = 0; [ 0:06] 449 p_dw_i = 1; [ 0:06] 450 c_num_read = 0; [ 0:06] 451 c_dr_pc = 0; [ 0:06] 452 c_dr_i = 1; [ 0:06] 453 [ 0:06] 454 return; [ 0:06] 455 } [ 0:06] 456 } [ 0:06] 457 int main(void) [ 0:06] 458 { int __retres1 ; [ 0:06] 459 [ 0:06] 460 { [ 0:06] 461 { [ 0:06] 462 init_model(); [ 0:06] 463 start_simulation(); [ 0:06] 464 } [ 0:06] 465 __retres1 = 0; [ 0:06] 466 return (__retres1); [ 0:06] 467 } [ 0:06] 468 } [ 0:06] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/pc_sfifo_2_false.cil.c:12, but it was not