[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/toy1_false.cil.c [ 0:00] compiling /dios/lib/config/seqklee.bc [ 0:00] setting up pass: functionmeta, options = [ 0:01] setting up pass: fuse-ctors, options = [ 0:01] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.20/_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:03] [ 0:03] 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: 35456 [ 0:06] Stack: [ 0:06] #000035456 in __dios_start (l=0, argc=1, argv=93848321790472, envp=93848321859592) at /dios/libc/sys/start.cpp:87 [ 0:06] #100011475 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:06] #200043806 in klee_boot (argc=2, argv=93848296249344) at /dios/arch/klee/boot.c:41 [ 0:06] [ 0:06] [ 0:06] 1 /* TAGS: error c sym z3skip */ [ 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 /* Generated by CIL v. 1.3.6 */ [ 0:06] 7 /* print_CIL_Input is true */ [ 0:06] 8 [ 0:06] 9 [ 0:06] 10 [ 0:06] 11 void error(void) [ 0:06] 12 { [ 0:06] 13 [ 0:06] 14 { [ 0:06] 15 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:06] 16 return; [ 0:06] 17 } [ 0:06] 18 } [ 0:06] 19 [ 0:06] 20 int c ; [ 0:06] 21 int c_t ; [ 0:06] 22 int c_req_up ; [ 0:06] 23 int p_in ; [ 0:06] 24 int p_out ; [ 0:06] 25 int wl_st ; [ 0:06] 26 int c1_st ; [ 0:06] 27 int c2_st ; [ 0:06] 28 int wb_st ; [ 0:06] 29 int r_st ; [ 0:06] 30 int wl_i ; [ 0:06] 31 int c1_i ; [ 0:06] 32 int c2_i ; [ 0:06] 33 int wb_i ; [ 0:06] 34 int r_i ; [ 0:06] 35 int wl_pc ; [ 0:06] 36 int c1_pc ; [ 0:06] 37 int c2_pc ; [ 0:06] 38 int wb_pc ; [ 0:06] 39 int e_e ; [ 0:06] 40 int e_f ; [ 0:06] 41 int e_g ; [ 0:06] 42 int e_c ; [ 0:06] 43 int e_p_in ; [ 0:06] 44 int e_wl ; [ 0:06] 45 void write_loop(void) ; [ 0:06] 46 void compute1(void) ; [ 0:06] 47 void compute2(void) ; [ 0:06] 48 void write_back(void) ; [ 0:06] 49 void read(void) ; [ 0:06] 50 int d ; [ 0:06] 51 int data ; [ 0:06] 52 int processed ; [ 0:06] 53 static int t_b ; [ 0:06] 54 void write_loop(void) [ 0:06] 55 { int t ; [ 0:06] 56 [ 0:06] 57 { [ 0:06] 58 if ((int )wl_pc == 0) { [ 0:06] 59 goto WL_ENTRY_LOC; [ 0:06] 60 } else { [ 0:06] 61 if ((int )wl_pc == 2) { [ 0:06] 62 goto WL_WAIT_2_LOC; [ 0:06] 63 } else { [ 0:06] 64 if ((int )wl_pc == 1) { [ 0:06] 65 goto WL_WAIT_1_LOC; [ 0:06] 66 } else { [ 0:06] 67 [ 0:06] 68 } [ 0:06] 69 } [ 0:06] 70 } [ 0:06] 71 WL_ENTRY_LOC: [ 0:06] 72 wl_st = 2; [ 0:06] 73 wl_pc = 1; [ 0:06] 74 e_wl = 0; [ 0:06] 75 [ 0:06] 76 goto return_label; [ 0:06] 77 WL_WAIT_1_LOC: [ 0:06] 78 { [ 0:06] 79 while (1) { [ 0:06] 80 while_0_continue: /* CIL Label */ ; [ 0:06] 81 t = d; [ 0:06] 82 data = d; [ 0:06] 83 processed = 0; [ 0:06] 84 e_f = 1; [ 0:06] 85 if ((int )c1_pc == 1) { [ 0:06] 86 if ((int )e_f == 1) { [ 0:06] 87 c1_st = 0; [ 0:06] 88 } else { [ 0:06] 89 [ 0:06] 90 } [ 0:06] 91 } else { [ 0:06] 92 [ 0:06] 93 } [ 0:06] 94 if ((int )c2_pc == 1) { [ 0:06] 95 if ((int )e_f == 1) { [ 0:06] 96 c2_st = 0; [ 0:06] 97 } else { [ 0:06] 98 [ 0:06] 99 } [ 0:06] 100 } else { [ 0:06] 101 [ 0:06] 102 } [ 0:06] 103 e_f = 2; [ 0:06] 104 wl_st = 2; [ 0:06] 105 wl_pc = 2; [ 0:06] 106 t_b = t; [ 0:06] 107 [ 0:06] 108 goto return_label; [ 0:06] 109 WL_WAIT_2_LOC: [ 0:06] 110 t = t_b; [ 0:06] 111 if (d == t + 1) { [ 0:06] 112 [ 0:06] 113 } else { [ 0:06] 114 if (d == t + 2) { [ 0:06] 115 [ 0:06] 116 } else { [ 0:06] 117 { [ 0:06] 118 error(); [ 0:06] 119 } [ 0:06] 120 } [ 0:06] 121 } [ 0:06] 122 if (d == t + 1) { [ 0:06] 123 [ 0:06] 124 } else { [ 0:06] 125 { [ 0:06] 126 error(); [ 0:06] 127 } [ 0:06] 128 [ 0:06] 129 } [ 0:06] 130 } [ 0:06] 131 while_0_break: /* CIL Label */ ; [ 0:06] 132 } [ 0:06] 133 return_label: /* CIL Label */ [ 0:06] 134 return; [ 0:06] 135 } [ 0:06] 136 } [ 0:06] 137 void compute1(void) [ 0:06] 138 { [ 0:06] 139 [ 0:06] 140 { [ 0:06] 141 if ((int )c1_pc == 0) { [ 0:06] 142 goto C1_ENTRY_LOC; [ 0:06] 143 } else { [ 0:06] 144 if ((int )c1_pc == 1) { [ 0:06] 145 goto C1_WAIT_LOC; [ 0:06] 146 } else { [ 0:06] 147 [ 0:06] 148 } [ 0:06] 149 } [ 0:06] 150 C1_ENTRY_LOC: [ 0:06] 151 { [ 0:06] 152 while (1) { [ 0:06] 153 while_1_continue: /* CIL Label */ ; [ 0:06] 154 c1_st = 2; [ 0:06] 155 c1_pc = 1; [ 0:06] 156 [ 0:06] 157 goto return_label; [ 0:06] 158 C1_WAIT_LOC: [ 0:06] 159 if (! processed) { [ 0:06] 160 data += 1; [ 0:06] 161 e_g = 1; [ 0:06] 162 if ((int )wb_pc == 1) { [ 0:06] 163 if ((int )e_g == 1) { [ 0:06] 164 wb_st = 0; [ 0:06] 165 } else { [ 0:06] 166 [ 0:06] 167 } [ 0:06] 168 } else { [ 0:06] 169 [ 0:06] 170 } [ 0:06] 171 e_g = 2; [ 0:06] 172 } else { [ 0:06] 173 [ 0:06] 174 } [ 0:06] 175 } [ 0:06] 176 while_1_break: /* CIL Label */ ; [ 0:06] 177 } [ 0:06] 178 return_label: /* CIL Label */ [ 0:06] 179 return; [ 0:06] 180 } [ 0:06] 181 } [ 0:06] 182 void compute2(void) [ 0:06] 183 { [ 0:06] 184 [ 0:06] 185 { [ 0:06] 186 if ((int )c2_pc == 0) { [ 0:06] 187 goto C2_ENTRY_LOC; [ 0:06] 188 } else { [ 0:06] 189 if ((int )c2_pc == 1) { [ 0:06] 190 goto C2_WAIT_LOC; [ 0:06] 191 } else { [ 0:06] 192 [ 0:06] 193 } [ 0:06] 194 } [ 0:06] 195 C2_ENTRY_LOC: [ 0:06] 196 { [ 0:06] 197 while (1) { [ 0:06] 198 while_2_continue: /* CIL Label */ ; [ 0:06] 199 c2_st = 2; [ 0:06] 200 c2_pc = 1; [ 0:06] 201 [ 0:06] 202 goto return_label; [ 0:06] 203 C2_WAIT_LOC: [ 0:06] 204 if (! processed) { [ 0:06] 205 data += 1; [ 0:06] 206 e_g = 1; [ 0:06] 207 if ((int )wb_pc == 1) { [ 0:06] 208 if ((int )e_g == 1) { [ 0:06] 209 wb_st = 0; [ 0:06] 210 } else { [ 0:06] 211 [ 0:06] 212 } [ 0:06] 213 } else { [ 0:06] 214 [ 0:06] 215 } [ 0:06] 216 e_g = 2; [ 0:06] 217 } else { [ 0:06] 218 [ 0:06] 219 } [ 0:06] 220 } [ 0:06] 221 while_2_break: /* CIL Label */ ; [ 0:06] 222 } [ 0:06] 223 return_label: /* CIL Label */ [ 0:06] 224 return; [ 0:06] 225 } [ 0:06] 226 } [ 0:06] 227 void write_back(void) [ 0:06] 228 { [ 0:06] 229 [ 0:06] 230 { [ 0:06] 231 if ((int )wb_pc == 0) { [ 0:06] 232 goto WB_ENTRY_LOC; [ 0:06] 233 } else { [ 0:06] 234 if ((int )wb_pc == 1) { [ 0:06] 235 goto WB_WAIT_LOC; [ 0:06] 236 } else { [ 0:06] 237 [ 0:06] 238 } [ 0:06] 239 } [ 0:06] 240 WB_ENTRY_LOC: [ 0:06] 241 { [ 0:06] 242 while (1) { [ 0:06] 243 while_3_continue: /* CIL Label */ ; [ 0:06] 244 wb_st = 2; [ 0:06] 245 wb_pc = 1; [ 0:06] 246 [ 0:06] 247 goto return_label; [ 0:06] 248 WB_WAIT_LOC: [ 0:06] 249 c_t = data; [ 0:06] 250 c_req_up = 1; [ 0:06] 251 processed = 1; [ 0:06] 252 } [ 0:06] 253 while_3_break: /* CIL Label */ ; [ 0:06] 254 } [ 0:06] 255 return_label: /* CIL Label */ [ 0:06] 256 return; [ 0:06] 257 } [ 0:06] 258 } [ 0:06] 259 void read(void) [ 0:06] 260 { [ 0:06] 261 [ 0:06] 262 { [ 0:06] 263 d = c; [ 0:06] 264 e_e = 1; [ 0:06] 265 if ((int )wl_pc == 1) { [ 0:06] 266 if ((int )e_wl == 1) { [ 0:06] 267 wl_st = 0; [ 0:06] 268 } else { [ 0:06] 269 goto _L; [ 0:06] 270 } [ 0:06] 271 } else { [ 0:06] 272 _L: /* CIL Label */ [ 0:06] 273 if ((int )wl_pc == 2) { [ 0:06] 274 if ((int )e_e == 1) { [ 0:06] 275 wl_st = 0; [ 0:06] 276 } else { [ 0:06] 277 [ 0:06] 278 } [ 0:06] 279 } else { [ 0:06] 280 [ 0:06] 281 } [ 0:06] 282 } [ 0:06] 283 e_e = 2; [ 0:06] 284 r_st = 2; [ 0:06] 285 [ 0:06] 286 return; [ 0:06] 287 } [ 0:06] 288 } [ 0:06] 289 void eval(void) [ 0:06] 290 { int tmp ; [ 0:06] 291 int tmp___0 ; [ 0:06] 292 int tmp___1 ; [ 0:06] 293 int tmp___2 ; [ 0:06] 294 int tmp___3 ; [ 0:06] 295 [ 0:06] 296 { [ 0:06] 297 { [ 0:06] 298 while (1) { [ 0:06] 299 while_4_continue: /* CIL Label */ ; [ 0:06] 300 if ((int )wl_st == 0) { [ 0:06] 301 [ 0:06] 302 } else { [ 0:06] 303 if ((int )c1_st == 0) { [ 0:06] 304 [ 0:06] 305 } else { [ 0:06] 306 if ((int )c2_st == 0) { [ 0:06] 307 [ 0:06] 308 } else { [ 0:06] 309 if ((int )wb_st == 0) { [ 0:06] 310 [ 0:06] 311 } else { [ 0:06] 312 if ((int )r_st == 0) { [ 0:06] 313 [ 0:06] 314 } else { [ 0:06] 315 goto while_4_break; [ 0:06] 316 } [ 0:06] 317 } [ 0:06] 318 } [ 0:06] 319 } [ 0:06] 320 } [ 0:06] 321 if ((int )wl_st == 0) { [ 0:06] 322 { [ 0:06] 323 tmp = __VERIFIER_nondet_int(); [ 0:06] 324 } [ 0:06] 325 if (tmp) { [ 0:06] 326 { [ 0:06] 327 wl_st = 1; [ 0:06] 328 write_loop(); [ 0:06] 329 } [ 0:06] 330 } else { [ 0:06] 331 [ 0:06] 332 } [ 0:06] 333 } else { [ 0:06] 334 [ 0:06] 335 } [ 0:06] 336 if ((int )c1_st == 0) { [ 0:06] 337 { [ 0:06] 338 tmp___0 = __VERIFIER_nondet_int(); [ 0:06] 339 } [ 0:06] 340 if (tmp___0) { [ 0:06] 341 { [ 0:06] 342 c1_st = 1; [ 0:06] 343 compute1(); [ 0:06] 344 } [ 0:06] 345 } else { [ 0:06] 346 [ 0:06] 347 } [ 0:06] 348 } else { [ 0:06] 349 [ 0:06] 350 } [ 0:06] 351 if ((int )c2_st == 0) { [ 0:06] 352 { [ 0:06] 353 tmp___1 = __VERIFIER_nondet_int(); [ 0:06] 354 } [ 0:06] 355 if (tmp___1) { [ 0:06] 356 { [ 0:06] 357 c2_st = 1; [ 0:06] 358 compute2(); [ 0:06] 359 } [ 0:06] 360 } else { [ 0:06] 361 [ 0:06] 362 } [ 0:06] 363 } else { [ 0:06] 364 [ 0:06] 365 } [ 0:06] 366 if ((int )wb_st == 0) { [ 0:06] 367 { [ 0:06] 368 tmp___2 = __VERIFIER_nondet_int(); [ 0:06] 369 } [ 0:06] 370 if (tmp___2) { [ 0:06] 371 { [ 0:06] 372 wb_st = 1; [ 0:06] 373 write_back(); [ 0:06] 374 } [ 0:06] 375 } else { [ 0:06] 376 [ 0:06] 377 } [ 0:06] 378 } else { [ 0:06] 379 [ 0:06] 380 } [ 0:06] 381 if ((int )r_st == 0) { [ 0:06] 382 { [ 0:06] 383 tmp___3 = __VERIFIER_nondet_int(); [ 0:06] 384 } [ 0:06] 385 if (tmp___3) { [ 0:06] 386 { [ 0:06] 387 r_st = 1; [ 0:06] 388 read(); [ 0:06] 389 } [ 0:06] 390 } else { [ 0:06] 391 [ 0:06] 392 } [ 0:06] 393 } else { [ 0:06] 394 [ 0:06] 395 } [ 0:06] 396 } [ 0:06] 397 while_4_break: /* CIL Label */ ; [ 0:06] 398 } [ 0:06] 399 [ 0:06] 400 return; [ 0:06] 401 } [ 0:06] 402 } [ 0:06] 403 void start_simulation(void) [ 0:06] 404 { int kernel_st ; [ 0:06] 405 [ 0:06] 406 { [ 0:06] 407 kernel_st = 0; [ 0:06] 408 if ((int )c_req_up == 1) { [ 0:06] 409 if (c != c_t) { [ 0:06] 410 c = c_t; [ 0:06] 411 e_c = 0; [ 0:06] 412 } else { [ 0:06] 413 [ 0:06] 414 } [ 0:06] 415 c_req_up = 0; [ 0:06] 416 } else { [ 0:06] 417 [ 0:06] 418 } [ 0:06] 419 if ((int )wl_i == 1) { [ 0:06] 420 wl_st = 0; [ 0:06] 421 } else { [ 0:06] 422 wl_st = 2; [ 0:06] 423 } [ 0:06] 424 if ((int )c1_i == 1) { [ 0:06] 425 c1_st = 0; [ 0:06] 426 } else { [ 0:06] 427 c1_st = 2; [ 0:06] 428 } [ 0:06] 429 if ((int )c2_i == 1) { [ 0:06] 430 c2_st = 0; [ 0:06] 431 } else { [ 0:06] 432 c2_st = 2; [ 0:06] 433 } [ 0:06] 434 if ((int )wb_i == 1) { [ 0:06] 435 wb_st = 0; [ 0:06] 436 } else { [ 0:06] 437 wb_st = 2; [ 0:06] 438 } [ 0:06] 439 if ((int )r_i == 1) { [ 0:06] 440 r_st = 0; [ 0:06] 441 } else { [ 0:06] 442 r_st = 2; [ 0:06] 443 } [ 0:06] 444 if ((int )e_f == 0) { [ 0:06] 445 e_f = 1; [ 0:06] 446 } else { [ 0:06] 447 [ 0:06] 448 } [ 0:06] 449 if ((int )e_g == 0) { [ 0:06] 450 e_g = 1; [ 0:06] 451 } else { [ 0:06] 452 [ 0:06] 453 } [ 0:06] 454 if ((int )e_e == 0) { [ 0:06] 455 e_e = 1; [ 0:06] 456 } else { [ 0:06] 457 [ 0:06] 458 } [ 0:06] 459 if ((int )e_c == 0) { [ 0:06] 460 e_c = 1; [ 0:06] 461 } else { [ 0:06] 462 [ 0:06] 463 } [ 0:06] 464 if ((int )e_wl == 0) { [ 0:06] 465 e_wl = 1; [ 0:06] 466 } else { [ 0:06] 467 [ 0:06] 468 } [ 0:06] 469 if ((int )wl_pc == 1) { [ 0:06] 470 if ((int )e_wl == 1) { [ 0:06] 471 wl_st = 0; [ 0:06] 472 } else { [ 0:06] 473 goto _L; [ 0:06] 474 } [ 0:06] 475 } else { [ 0:06] 476 _L: /* CIL Label */ [ 0:06] 477 if ((int )wl_pc == 2) { [ 0:06] 478 if ((int )e_e == 1) { [ 0:06] 479 wl_st = 0; [ 0:06] 480 } else { [ 0:06] 481 [ 0:06] 482 } [ 0:06] 483 } else { [ 0:06] 484 [ 0:06] 485 } [ 0:06] 486 } [ 0:06] 487 if ((int )c1_pc == 1) { [ 0:06] 488 if ((int )e_f == 1) { [ 0:06] 489 c1_st = 0; [ 0:06] 490 } else { [ 0:06] 491 [ 0:06] 492 } [ 0:06] 493 } else { [ 0:06] 494 [ 0:06] 495 } [ 0:06] 496 if ((int )c2_pc == 1) { [ 0:06] 497 if ((int )e_f == 1) { [ 0:06] 498 c2_st = 0; [ 0:06] 499 } else { [ 0:06] 500 [ 0:06] 501 } [ 0:06] 502 } else { [ 0:06] 503 [ 0:06] 504 } [ 0:06] 505 if ((int )wb_pc == 1) { [ 0:06] 506 if ((int )e_g == 1) { [ 0:06] 507 wb_st = 0; [ 0:06] 508 } else { [ 0:06] 509 [ 0:06] 510 } [ 0:06] 511 } else { [ 0:06] 512 [ 0:06] 513 } [ 0:06] 514 if ((int )e_c == 1) { [ 0:06] 515 r_st = 0; [ 0:06] 516 } else { [ 0:06] 517 [ 0:06] 518 } [ 0:06] 519 if ((int )e_e == 1) { [ 0:06] 520 e_e = 2; [ 0:06] 521 } else { [ 0:06] 522 [ 0:06] 523 } [ 0:06] 524 if ((int )e_f == 1) { [ 0:06] 525 e_f = 2; [ 0:06] 526 } else { [ 0:06] 527 [ 0:06] 528 } [ 0:06] 529 if ((int )e_g == 1) { [ 0:06] 530 e_g = 2; [ 0:06] 531 } else { [ 0:06] 532 [ 0:06] 533 } [ 0:06] 534 if ((int )e_c == 1) { [ 0:06] 535 e_c = 2; [ 0:06] 536 } else { [ 0:06] 537 [ 0:06] 538 } [ 0:06] 539 if ((int )e_wl == 1) { [ 0:06] 540 e_wl = 2; [ 0:06] 541 } else { [ 0:06] 542 [ 0:06] 543 } [ 0:06] 544 { [ 0:06] 545 while (1) { [ 0:06] 546 while_5_continue: /* CIL Label */ ; [ 0:06] 547 { [ 0:06] 548 kernel_st = 1; [ 0:06] 549 eval(); [ 0:06] 550 } [ 0:06] 551 kernel_st = 2; [ 0:06] 552 if ((int )c_req_up == 1) { [ 0:06] 553 if (c != c_t) { [ 0:06] 554 c = c_t; [ 0:06] 555 e_c = 0; [ 0:06] 556 } else { [ 0:06] 557 [ 0:06] 558 } [ 0:06] 559 c_req_up = 0; [ 0:06] 560 } else { [ 0:06] 561 [ 0:06] 562 } [ 0:06] 563 kernel_st = 3; [ 0:06] 564 if ((int )e_f == 0) { [ 0:06] 565 e_f = 1; [ 0:06] 566 } else { [ 0:06] 567 [ 0:06] 568 } [ 0:06] 569 if ((int )e_g == 0) { [ 0:06] 570 e_g = 1; [ 0:06] 571 } else { [ 0:06] 572 [ 0:06] 573 } [ 0:06] 574 if ((int )e_e == 0) { [ 0:06] 575 e_e = 1; [ 0:06] 576 } else { [ 0:06] 577 [ 0:06] 578 } [ 0:06] 579 if ((int )e_c == 0) { [ 0:06] 580 e_c = 1; [ 0:06] 581 } else { [ 0:06] 582 [ 0:06] 583 } [ 0:06] 584 if ((int )e_wl == 0) { [ 0:06] 585 e_wl = 1; [ 0:06] 586 } else { [ 0:06] 587 [ 0:06] 588 } [ 0:06] 589 if ((int )wl_pc == 1) { [ 0:06] 590 if ((int )e_wl == 1) { [ 0:06] 591 wl_st = 0; [ 0:06] 592 } else { [ 0:06] 593 goto _L___0; [ 0:06] 594 } [ 0:06] 595 } else { [ 0:06] 596 _L___0: /* CIL Label */ [ 0:06] 597 if ((int )wl_pc == 2) { [ 0:06] 598 if ((int )e_e == 1) { [ 0:06] 599 wl_st = 0; [ 0:06] 600 } else { [ 0:06] 601 [ 0:06] 602 } [ 0:06] 603 } else { [ 0:06] 604 [ 0:06] 605 } [ 0:06] 606 } [ 0:06] 607 if ((int )c1_pc == 1) { [ 0:06] 608 if ((int )e_f == 1) { [ 0:06] 609 c1_st = 0; [ 0:06] 610 } else { [ 0:06] 611 [ 0:06] 612 } [ 0:06] 613 } else { [ 0:06] 614 [ 0:06] 615 } [ 0:06] 616 if ((int )c2_pc == 1) { [ 0:06] 617 if ((int )e_f == 1) { [ 0:06] 618 c2_st = 0; [ 0:06] 619 } else { [ 0:06] 620 [ 0:06] 621 } [ 0:06] 622 } else { [ 0:06] 623 [ 0:06] 624 } [ 0:06] 625 if ((int )wb_pc == 1) { [ 0:06] 626 if ((int )e_g == 1) { [ 0:06] 627 wb_st = 0; [ 0:06] 628 } else { [ 0:06] 629 [ 0:06] 630 } [ 0:06] 631 } else { [ 0:06] 632 [ 0:06] 633 } [ 0:06] 634 if ((int )e_c == 1) { [ 0:06] 635 r_st = 0; [ 0:06] 636 } else { [ 0:06] 637 [ 0:06] 638 } [ 0:06] 639 if ((int )e_e == 1) { [ 0:06] 640 e_e = 2; [ 0:06] 641 } else { [ 0:06] 642 [ 0:06] 643 } [ 0:06] 644 if ((int )e_f == 1) { [ 0:06] 645 e_f = 2; [ 0:06] 646 } else { [ 0:06] 647 [ 0:06] 648 } [ 0:06] 649 if ((int )e_g == 1) { [ 0:06] 650 e_g = 2; [ 0:06] 651 } else { [ 0:06] 652 [ 0:06] 653 } [ 0:06] 654 if ((int )e_c == 1) { [ 0:06] 655 e_c = 2; [ 0:06] 656 } else { [ 0:06] 657 [ 0:06] 658 } [ 0:06] 659 if ((int )e_wl == 1) { [ 0:06] 660 e_wl = 2; [ 0:06] 661 } else { [ 0:06] 662 [ 0:06] 663 } [ 0:06] 664 if ((int )wl_st == 0) { [ 0:06] 665 [ 0:06] 666 } else { [ 0:06] 667 if ((int )c1_st == 0) { [ 0:06] 668 [ 0:06] 669 } else { [ 0:06] 670 if ((int )c2_st == 0) { [ 0:06] 671 [ 0:06] 672 } else { [ 0:06] 673 if ((int )wb_st == 0) { [ 0:06] 674 [ 0:06] 675 } else { [ 0:06] 676 if ((int )r_st == 0) { [ 0:06] 677 [ 0:06] 678 } else { [ 0:06] 679 goto while_5_break; [ 0:06] 680 } [ 0:06] 681 } [ 0:06] 682 } [ 0:06] 683 } [ 0:06] 684 } [ 0:06] 685 } [ 0:06] 686 while_5_break: /* CIL Label */ ; [ 0:06] 687 } [ 0:06] 688 [ 0:06] 689 return; [ 0:06] 690 } [ 0:06] 691 } [ 0:06] 692 int main(void) [ 0:06] 693 { int __retres1 ; [ 0:06] 694 [ 0:06] 695 { [ 0:06] 696 { [ 0:06] 697 e_wl = 2; [ 0:06] 698 e_c = e_wl; [ 0:06] 699 e_g = e_c; [ 0:06] 700 e_f = e_g; [ 0:06] 701 e_e = e_f; [ 0:06] 702 wl_pc = 0; [ 0:06] 703 c1_pc = 0; [ 0:06] 704 c2_pc = 0; [ 0:06] 705 wb_pc = 0; [ 0:06] 706 wb_i = 1; [ 0:06] 707 c2_i = wb_i; [ 0:06] 708 c1_i = c2_i; [ 0:06] 709 wl_i = c1_i; [ 0:06] 710 r_i = 0; [ 0:06] 711 c_req_up = 0; [ 0:06] 712 d = 0; [ 0:06] 713 c = 0; [ 0:06] 714 start_simulation(); [ 0:06] 715 } [ 0:06] 716 __retres1 = 0; [ 0:06] 717 return (__retres1); [ 0:06] 718 } [ 0:06] 719 } [ 0:06] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/toy1_false.cil.c:15, but it was not