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